Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

发现了一只大佬 #1

Closed
duangsuse opened this issue Dec 28, 2017 · 144 comments
Closed

发现了一只大佬 #1

duangsuse opened this issue Dec 28, 2017 · 144 comments

Comments

@duangsuse
Copy link
Collaborator

🌚 在看 gh 更新时发现之前因为 "中文 C#" 事件 #csharplang/993 关注的 @Glavo
Star 了一个 JVM 程序设计语言的 repo https://github.com/lice-lang/lice

看看居然是函数式 Lisp 方言! 后来还发现是中国人开发的??? (虽然之前那个 lemon-lang 也中国人
后来发现居然... 是高中大佬??? 于是找到个人博客发现是 真·大佬_ ... 而且还是 死宅 🌝

@ice1000

看看 Github 主页的... 怕不是 5 岁就??? wtf 虽然最近两年才有真正的项目

忍不住想到了我寒假时的 https://coding.net/u/duangsuse/p/MonkeyVM , 虽然现在无法看那时候的代码
而且 🐒 语言 又是低级语言

(ps. 我真的惊讶了,虽然现在还没有一年吧,没想到他的博客名 "IR" 我居然在看到谜底前能猜到是 "中间表示 Intermid Repr, 虽然当时大概最先想大概是 MS IL (当然我现在还不会写... 虽然我英语很能记单词)"

总算找到一个同为低龄研究 "高级" 食物的dalao了 (因为有别人那 @drakeet 之前说的一些大概觉得我应该先 好好学习 那些书你看不懂... 这样的话就影响少一些了) ,
虽然之前也交到不少前/后端

(以及 @losfair , 不过可怕的是这个... 居然还研究过地图生成 (之前计划的有个类似生存战争的游戏用到,死想不到怎么做 (当然是空想因为想碰电脑不容易)),总之学得很杂和我差不多 🌚

中午没有时间就没注重排版了... 希望能交上 py XD( 可惜他应该不在 telegram.me 吧... 而且我现在也不能上了

@duangsuse
Copy link
Collaborator Author

@duangsuse
Copy link
Collaborator Author

@duangsuse
Copy link
Collaborator Author

你好,欢迎来到我的博客 「中间表示 (IR) 」 ,我是千里冰封。
我此时还不知道是什么时候知道这词的...( 大概是 repr + IL 自己组合来的吧 🌚

@duangsuse
Copy link
Collaborator Author

duangsuse commented Dec 28, 2017

在我看来,网上那些自称会编程的初中/高中生大部分都是

没有命名规范
函数名用拼音
代码没有设计
自称熟悉 C++然而却不知道 C++有 class 这个保留字
把没有对象的编程称为函数式编程,比如纯 C 风格
语言工具论

(ANSI 标准)C 是过程式 🌝

很多我三次元认识的人也不例外,尤其是刚入坑的 OIer。

🌚 有时候批判 NOIP 和一些... (
https://t.me/dsuse 上可以看到一些

补充:

😳反正 没有命名规范 指的是

void boynextdoor
void Boynextdoor
void BoyNextDoor
void boy_next_door
void lingjiananhai
void ling_jia_nan_hai
void Ling_jia_Nan_hai
void Nan_hai_nextDoor

从来没写过这样的命名?(
https://coding.net/u/duangsuse/p/MonkeyVM/git/blob/master/src/main.rs

@duangsuse
Copy link
Collaborator Author

我是初三毕业开始学编程的【

同 🌝
其实我小学四年级开始,不过后面到初三都是泡 Linux 吧里面...
后来通过 https://coolapk.com 认识一堆dalao 开始学习程序设计
第一个是今年2月的 MinBase64, 那代码我不想看,可惜那么 🐔 的项目我居然上了几个 CI 服务... 黑历史
现在在设计 coolapk 的替代品 GeekAPK (相关 repo 还在我这里)

人吗... 还是向以前一样爱折腾
我的 Telegram 是 @duangsuse , (其实年龄真的还不算太重要,但中国能有程序员一生能尝试到你尝试的东西都太少了) (当然最近由于 GeekApk 的事情强迫自己退了一段时间

过几个月搞 {male sign} 完 GeekApk 第一个平台版本 就回来 😄

@duangsuse
Copy link
Collaborator Author

另外你看的都是些啥啊,不来看看 https://github.com/ice1000/resume

看过了 😃 虽然我也没研究 TeX ... 迟早会的
和 wangyin 有得一拼?(

@duangsuse
Copy link
Collaborator Author

地图生成那个其实只糊了一晚上,然后再修修补补了一星期,23333 😆

唉,现在时间真的是硬伤啊 😢
中午 1小时 晚上 2小时
虽然之前我最多也连着搞了一个月... 虽然有帮助还是不大(最后又上学去了
具体可以看我的 channel https://t.me/dsuset
没时间... 现在还有 GeekApk
之前的 Tree 和 MinVM(后面还有 MinASM EMMC 等...) 直接拖掉了 😢

@duangsuse
Copy link
Collaborator Author

另外我相当不喜欢Linux【

我 Windows/ GNU/Linux 通吃 😄
有时候研究点其他操作系统和内核 Bootloader 什么的

         _,met$$$$$gg.           dse@susepc
      ,g$$$$$$$$$$$$$$$P.        OS: Debian testing buster
    ,g$$P""       """Y$$.".      Kernel: x86_64 Linux 4.13.0-1-amd64
   ,$$P'              `$$$.      Uptime: 10d 10h 45m
  ',$$P       ,ggs.     `$$b:    Packages: 2793
  `d$$'     ,$P"'   .    $$$     Shell: bash
   $$P      d$'     ,    $$P     Resolution: 1920x1080
   $$:      $$.   -    ,d$$'     DE: XFCE
   $$\;      Y$b._   _,d$P'      WM: Xfwm4
   Y$$.    `.`"Y$$$$P"'          WM Theme: Default
   `$$b      "-.__               GTK Theme: Xfce [GTK2]
    `Y$$                         Icon Theme: Tango
     `Y$$.                       Font: Sans 10
       `$$b.                     CPU: Intel Celeron 847 @ 2x 1.1GHz [48.0°C]
         `Y$$b.                  GPU: intel
            `"Y$b._              RAM: 947MiB / 1852MiB
                `""""           

@ice1000
Copy link

ice1000 commented Dec 28, 2017

你那个channel为啥我没法说话啊

@duangsuse
Copy link
Collaborator Author

👆 10d 我这几天睡眠 ( systemctl suspend ) 到的 XD

@duangsuse
Copy link
Collaborator Author

你那个channel为啥我没法说话啊

🌚 WTF( channel 你不是发布者当然不能说话(

@duangsuse
Copy link
Collaborator Author

duangsuse commented Dec 28, 2017

我在给Lice做IntelliJ IDEA的插件【

dalao(

@duangsuse
Copy link
Collaborator Author

duangsuse commented Dec 28, 2017

钦点了flex和bnf真麻烦,我原本的Parser是手写的魔法。。。

我差不多死了的 Min (现在还是设计阶段) 也计划手写 LALR ...

Jay 估计也不错,但 Min 的主要目标是体积...
用于 替换 BeanShell 和 AndroLua (XD

@duangsuse
Copy link
Collaborator Author

我不是很熟悉Telegram那一套理论,平时也没什么需要在tg讨论的东西,都是QQ。。。

我更喜欢 tg 的良心

@duangsuse
Copy link
Collaborator Author

另外LALR什么的都是邪教,Haskell/Parserc大法好【

怕不是体积要报表(

@duangsuse
Copy link
Collaborator Author

Min 之所以要分开 Compiler/Assembler/VM 就是为了减小体积

@duangsuse
Copy link
Collaborator Author

用什么社交软件全取决于我想联系啥样的人

一般我觉得 tg 上 nc 少很多

@duangsuse
Copy link
Collaborator Author

我用Haskell写的完整的Kotlin Parser编译出来也不到5mb

你知道 BeanShell core 多大吗...(*
你会吓死,因为比你小 10x 🌚 (

@duangsuse
Copy link
Collaborator Author

duangsuse commented Dec 28, 2017

哇你手写汇编CodeGen啊

别胡说,是 Min 汇编( 我不做这种事

@duangsuse
Copy link
Collaborator Author

duangsuse commented Dec 28, 2017

比较像 Ruby

按我的话说是 Ruby/BeanShell/Lua(LuaJava) 杂交

@duangsuse
Copy link
Collaborator Author

还有你应该学习一个markdown语法【

Fixed(

@duangsuse
Copy link
Collaborator Author

duangsuse commented Dec 28, 2017

Ruby语法复杂度比Kotlin小多了。。

简单优雅
Min 就像它的名字一样小... 计划最多带 EMMC 200k

@duangsuse
Copy link
Collaborator Author

哦,语法啥样的?

xiaq/halang#1 (comment)

这虽然不是 Min ... ( 结构可以参考

@duangsuse
Copy link
Collaborator Author

是是是,限制太少了【
连CH同构都证不了,Haskell都能证加法交换律【

(一般情况能胜任就好,我不要求绝对的表现力(

@duangsuse
Copy link
Collaborator Author

好讨厌,竟然翻我黑历史【

反正没人(
你也可以翻我的

@ice1000
Copy link

ice1000 commented Dec 28, 2017

这虽然不是 Min ... ( 结构可以参考

真敷衍,bnf和type system都没说【

@duangsuse
Copy link
Collaborator Author

我不是很熟悉Telegram那一套理论,平时也没什么需要在tg讨论的东西,都是QQ。。。

🙈 你没找对地方(

@duangsuse
Copy link
Collaborator Author

duangsuse commented Dec 28, 2017

真敷衍,bnf和type system都没说【

所以才来找大佬 py 学习一个 🌚
而且也真的是没时间了...

@duangsuse
Copy link
Collaborator Author

2017-12-22 13-28-54

@duangsuse
Copy link
Collaborator Author

rainoftime/marisakirisame/terrojack/belleve都在QQ,为什么我需要其他的IM,难道TG你能找到Odersky/SPJ?

我目前没在 QQ 上找到真正的技术 py ( 而且 QQ 对我来说比较不方便,尤其是现在 Debian 使用起来

@nukc
Copy link

nukc commented Nov 4, 2018

py 吗

@duangsuse
Copy link
Collaborator Author

duangsuse commented Nov 9, 2018

话说 @ice1000 到底是男是女,没有看到答案啊

... 这方面你就别纠结了,我真的不相信 (她 | 他) 一出生就写了 ice1000/Dekoder
... 我倒是没有虚化自己实际身份的癖好,我十七岁男湖北襄阳最烂高中八中高二在读 2002 年生 😶 学渣人间之屑长得很像先辈 Instagram @duangsuse Telegram QQ 也是这垃圾绿色头像号,连 Agda 即得易见平凡都看不出来也认不出扭来扭去的 ∧ LOGICAL AND ∨ LOGICAL OR 逻辑符号并且不知道 XeTeX MathJax 是啥,也不知道啥是 lambda (λ)演算啥是集合论也没学过定理证明在学 Haskell 并且连 Currying 和模式匹配都不会用并且作为垃圾 Jawa 厨更是一周前连子类对象为何能 safely cast to base type 和 Rust 的 subtyping 都不知道 Rustonomicon 都没看过并且泛型除了 Java 和 Kotlin 外 Haskell 里的也只是会用不知其所以然并且 Haskell ADT(抽象数据类型)只入门了个大写 Type 和小写 Type Variable,至于并发编程 ES6 async 函数咋和 coroutine 有关的我都不知道,根本看不懂你们 declarative 声明式 Hindley-Milner 的稀奇古怪的类型定义并且算法方面超级菜的,只认识比较线性(不是指时间复杂度)的数据结构并且刚刚学会 Dijkstra 和 Bellman-Ford 两种图算法甚至可能连伪代码都不知道怎么写并且动态规划是啥都不会,网络流真的是不知道是啥(这句真话),反正就是那种菜到爆炸的垃圾人+巨婴+en_* 系语言都看不懂,经常被一些连选择排序都不会而且熟悉 jadx 命令行工具使用并且非常擅长逆向工程而且连 WebAssembly 都不知道是啥而且连 ARM 系列有哪几种常用微控制器平台的并且连大端小端是啥都不知道的 Android 前端吊打也面不改色并且还想乘着人家结婚大喜之际给人家道歉重新修好我就是这种人渣,动漫也不看游戏也不玩文化科也不学留学别想 DSP 不会数学渣渣连地图生成该拿那种函数负责都不知道,啥 nn 神经网络啥导数最大公约数啥质数、三角函数都不会各种密码学算法诸如 RSA、md5 都不会求不喷(或者说欢迎喷啊,欢迎啥都不知道知识图狭窄的不要不要并且连 Function.prototype.bind 都不知道的前端们和用别人框架开发游戏的大佬(大嘘)们来喷,用你们之前写过所有比王垠还厉害的那些前端代码喷我啊,咱们比写 lexer(lexical analyzer)(绝望)别比写什么「降维打击解决魅族状态栏 UI bug(其实就是 Rx 定时任务...)」什么「类型池」什么「Android 高级混淆代码保护」什么「Android 里最优雅的 TextEdit 行间距算法」什么「Android layout XML 优雅格式化 IDEA 插件(居然连 javax 的内建 XML 序列化支持都不知道还上正则匹配)」什么 Flappy Bird 了(话说 U2D 写这种东西业务代码不会超过三百行啊...))

突然间发现又在这破烂黑历史上写了这么多字... 挖粪啊
然后想去萌百找点材料往里面加点幽默感来着... 算了还要帮老师写 Qt 点名器,绝对要吊打某些国内的辣鸡易语言点名器,不管是设计还是代码质量... 算了

上面这些我自己说的东西有些是真的有些是假的,求大佬别打回原型(才刚刚膨胀一点就被戳破是很难受的,绝望

上面有些假的信息,说的反话都是为了各种工业界的 dalao 啊!
虽然被连 bfs 这种 naive 到爆炸的 蠢萌 算法都不会甚至只会个 bubble sort 冒泡排序然后不会选择排序也根本没听说过快速排序也不知道啥是时间复杂度啥是空间复杂度啥是 AC 啥是 RE 啥是 CE 啥是伪共享啥是 virtual 方法 mmap() 是啥消息队列是啥乐观锁是啥自旋锁是啥 Java 的 synchronized Kotlin 的 @Volatile CLR 的 Volatile.Read() Volatile.Write() 都不知道的的这种明显知其然(咋用 how)不知其所以然(咋实现 why)的前端开发兼(迫真)逆向工程(但实际上 QEMU 是咋工作、JIT 是啥内联汇编 GDB 反汇编、内存读写断点咋用、JDWP 是啥、的 int 指令是啥都不知道,或许还会被当成在 .data 里定义分配 int32 长度数据的伪指令呢呵呵) dalao 喷也死性不改继续打印资料买各种辣鸡根本用不到的书然后成天不认真听讲看书的 duangsuse 如是说

最后欢迎关注辣鸡人学习不辣鸡科目( <unnamed subject : (CS ^ IT)> 的记录频道(指 Telegram) duangsuse::Echo 我保证尽可能易读并且不(不带注释的)引入各种高大上但你们看得一脸蒙蔽的技术名词,不然就... 你退出呗(滑稽)(实话,因为目前里面还啥都没有)(好渴望有时间工程然后自己写个 web 应用不止在 Telegram 上发了)(一年后毕业了才能吧 hhhh)(要是有某些知乎 dalao 一半水平我早上 JB 做静态分析去了谁还在这里教你们 LinkedList<*> 是咋实现的这种弱智问题 233333)

顺带问问 ice1000.org 怎么了... 域名过期了? 🚶🏿 ❓

@ice1000
Copy link

ice1000 commented Nov 9, 2018

是开通https了。

@duangsuse
Copy link
Collaborator Author

是开通https了。

噢,我还以为是没有备案被限制了... 才发现是限制了 HSTS

btw. 好久没看 web 运维连 TLS 严格模式都忘了是啥了

@duangsuse
Copy link
Collaborator Author

... 这方面你就别纠结了,我真的不相信 (她 | 他) 一出生就写了 ice1000/Dekoder

^

ice1000/Dekoder@1c25871#commitcomment-25648208

据说是 commit 时间倒转导致 GitHub 误判... 对我的年龄来说的确是刚出生就会写 Kotlin 代码了 2333(话说那时候有我还没 Kotlin...

@duangsuse
Copy link
Collaborator Author

duangsuse commented Nov 9, 2018

强烈推荐 https://ice1000.org/lagda

好啊,可惜我打印机没墨了,而且 Haskell 都没入门你的 Agda 教程我还没看懂...

UPDATE:

刚才以为是 Agda 教程书... 才发现是静态博客系统啊

@ice1000
Copy link

ice1000 commented Nov 9, 2018

那个commit是在机房提交的,机房电脑的时间是2002年。

@duangsuse
Copy link
Collaborator Author

duangsuse commented Nov 24, 2018

强烈推荐 https://ice1000.org/lagda

你搞的这个东西还怪 excited 的,不知道为什么那些 JavaScript 系的前端就没有想出来,可能是平时 imperative 的东西用多了都想不到博客还可以一半用代码一半用自然语言写吧(:P

刚才找了找发现 Haskell 几乎可以说没有专门的中文社区,估计中国能在网上找到的 FP 爱好者还不是很多?

不过我目前也就个 Haskell 入门水平,刚会 multi-branch function 和 pattern matching 之类的 naive 模型

以前在本子上写 imperative 的 Java、Rust 的时候怪无聊的,感觉空间利用率低了一点或者说不是那么自然,现在给还没有被形式化定义的 InScript 弄了个模式识别扩展以后各种递归算法可以说写疯了... 真的是非常好看,没有一点余赘,真香。

Agda 教程打印了现在只是稍微看懂一些铪,可能是命名太不对新手友好了,含义都太隐式所以模式识别搞得我还要猜其意思,with 表达式还半会不会的水平,简单如逻辑基础、充要命题和类型架构器都模式识别得出来,而且既然 Haskell ADT 都还没做到知其所以然目前估计暂时还没法看,况且恳求学校放假不现实,一周一晚上... 每次本来可以讲点笔记的,然后到这周,笔记队列都要溢出了(最开始放进去的助记内容我都快忘记是说啥了),只好暂时放弃讲笔记,但还是经常熬夜到凌晨... 浑身难受

考虑到怕被喷(大嘘)就不 @ mention 了

顺推 InScript 新加入的模式识别多分支函数,当然正确性是非常不能保证的(非常符合 InScript 「自然第一,简洁正确第二」的哲学),而且我也没时间实现这破语言... 而且或许语法歧义很多吧(比 Julia 都多可能),或许很难实现?
(尤其是 polymorphism 纠缠不清... A[] 和 JVM 集合类型之间有啥关系呢... 依然等待学习,不能让类型都由程序员手动检查吧,那那群刚从网校毕业的菜鸡们就会写出一大堆一解释到就爆炸的代码,而且不知道自己是怎么死的)(好吧,即使有了正式执行前的类型检查报错我看他们也不知道自己在做什么)

{- Toy progream: FizzBuzz judger-}

type scannerIter : Iterator<out Int>
type judge : Int => String
type main : String[] => Nil

scannerIter = object : Iterator<out Int>
  new def next = gets.parseInt
  new def hasNext = IN.open?

judge(x) = when x
  % 3 zero  -> 'Buzz'
  % 5 zero  -> 'Fizz'
  both 1, 2 -> 'FizzBuzz'
  otherwise -> x as String

main(args) = puts << judge <$> scannerIter

{- Toy program: Guessing game -}
using randInt from std.math

main(String[] args): Nil = |>
  scope let answer = randInt(1..100)
    where while input = gets.parseInt
      puts when input where
        > answer -> 'Too big'
        < answer -> 'Too small'
        answer   -> "$answer, Just right!"; break 

{- Toy program: Selection sort -}

type <A : Comparable<? super A>> selectionSort : (A[]) -> A[]
# equiv
type <A : Comparable<? :< A>> selectionSort : (A[]) -> A[]

scope let opt = |orig@(v, i), b, j| v > b ? orig : b, j)
      where findSmallest(xs) = let (_, res) =
        foldWithIndex(opt, (Int::MIN, 0), xs) in res 

selectionSort [] = []
selectionSort [findSmallest x in xs] = x >> tailrec 

main(args) = puts selectionSort [2, 4, 1, 5, 3] 

{- Toy program: binarySearch -}

type <A : Comparable<in A>> binarySearch : |A[]| |A| |Range| Int

binarySearch xs o <srch = xs.indexRange> = |>
  let index = srch.mid, guess = xs[index] in when
    | srch.len zero -> nil
    | guess is o -> index
    | guess > o  -> tailrec(srch.a..srch.mid.sub1)
    | guess < o  -> tailrec(srch.mid.add1..srch.b)

noinline pure def <T> List<T>.binarySearch(T obj) = binarySearch(self, obj)

{- Toy program: dfs 在盒子堆里找指定物品,并且获得其路径 -}
data Box     = BoxItem[] items, String name
data Item    = String name
data BoxItem = Box box ^ Item item

findItemInBox(Box box, String target_name, String[] path = "")
  box.items.each |>[:findItemInBox, "$box.name/$path"]

findItemInBox(Item item, String target_name, String[] path) = puts path if item.name is target_name


{- Toy program: Coroutine Fibonacci 序列 -}

using std.sequence

def fibonacciSequence: Sequence
  let suspend fib(a, b) = tailrec(suspend b, a + b) in
    return new Sequence(fib(1, 2))


def main(args) = puts fibonacciSequence().take(args.first.parseInt ?: 100)

最后还顺便写了个 Haskell 的盒子堆,可惜不知道有没有更好的实践... 感觉有点奇怪

module BoxDfs where

data Item = Box (String, [Item]) | Atom String
  deriving (Eq, Show) 

findItem :: String -> [String] -> [Item] -> [String]

findItem m v [] = []

findItem m v ((Box (n, xs)):bs) = findItem m (n:v) xs
findItem m v ((Atom n):bs) = if n == m then v else []

@duangsuse
Copy link
Collaborator Author

最后还顺便写了个 Haskell 的盒子堆,可惜不知道有没有更好的实践... 感觉有点奇怪

最后分析结果是这解决方案无效,测试时使用了只有一条路径的,正在找其他解决方案

*BoxDfs> findItem "a" [] [Box("a", [Box("n", [Atom "a"])])]
["n","a"]

嗯,这样倒是蛮正确的 dfs

但是,但是!

*BoxDfs> findItem "a" [] [Box("a", [Box("n", [Atom "a"]), Box("bs", [Atom "a"])]), Box("xs", [Atom "x"])]
["n","a"]
*BoxDfs> findItem "a" [] [Box("a", [Box("n", [Atom ""]), Box("bs", [Atom "a"])]), Box("xs", [Atom "x"])]
[]
*BoxDfs> findItem "a" [] [Box("a", [Box("n", [Atom ""]), Box("bs", [Atom "a"])]), Box("xs", [Atom "x"])]

假若在第一个 Cons 能找到 Atom,就能正常返回正确的结果,反之,即使下一项有嵌套此 Atom 也不行... 晕

当然,我很好奇为啥 Haskell 不让我这么写... 歧义?

findItem m v [] = []
           | ((Box (n, xs)):bs) = findItem m (n:v) xs
           | ((Atom n):bs) = if n == m then v else []

@ice1000
Copy link

ice1000 commented Nov 24, 2018

你对guard的语法理解有问题

@duangsuse
Copy link
Collaborator Author

duangsuse commented Nov 24, 2018

你对guard的语法理解有问题

我不是对 guard,是想(对于这种情况)弄这样的语法糖

a b c d
  | x y
  | z w

等于

a b c d
a b x y
a b z w

因为重复看起来有点烦了...

所以我甚至(在 InScript 里)把 Kotlin 里只作为方法标记的 tailrec 搞成了递归简写,即使使用 tailrec 不代表定义真的能做尾递归优化...

fold op v [] = v
        | [x, ...xs] = op(x, tailrec)
fold op v [] = v
        | [x, ...xs] = op(x, tailrec(xs))
fold op v [] = v
        | [x, ...xs] = op(x, fold(op)(v)(xs))

UPDATE:我去确认了一下 Gurad 的定义 here

其实我本来不管这个叫 guard,之前学 Rust 的时候勉强记得有这个名词

不过后来是为了方便看了很多代码并简化产生的 InScript 语法,其实更类似伪代码因为没有形式定义,虽然预备好进行或许不 CFG 的形式化定义

Haskell 值得学习一下,不过 Haskell guard 的附加特性感觉可以看情况抄一点,就怕找不到时间实现了

@ice1000
Copy link

ice1000 commented Nov 24, 2018

你是想抄Idris的with abstraction的语法?这可能需要你弄下Layout。
Haskell本来就没这么设计,明明有case of语法。

{-# LANGUAGE LambdaCase #-}

bla : Int -> Int -> [Int] -> ()
bla a b = \case
  [] -> rua
  (a : as) -> ora

@duangsuse
Copy link
Collaborator Author

duangsuse commented Nov 24, 2018

你是想抄Idris的with abstraction的语法?

不敢,Idris 我几乎还没见过

上面说了 InScript 本来是基于那个垃圾 Lite 扩展一点语法和特性(诸如 block crossinlining, infix notation, extension function)等设计的,我设计时就是民科看哪块代码不爽就简化一下再添加一个对应文法,顺带从别的语言里抄点东西过来,很多模式之前根本不知道,啥时候准备规范化一下... :(

另. 上面的 {-# LANGUAGE LambdaCase #-} 勉强能识别出来

但 上上面的 when (InScript) 其实只是 when 自己的语法糖而已,和 guards、with abstraction 啥的没关系,大概等于

binarySearch xs o <srch = xs.indexRange> = |>
  let index = srch.mid, guess = xs[index] in when
    srch.len zero -> nil
    guess is o -> index
    guess > o  -> tailrec(srch.a..srch.mid.sub1)
    guess < o  -> tailrec(srch.mid.add1..srch.b)

因为 when | branch 也是有效的,而设计 InScript 时又打算在缩进上做一些文章

@ice1000
Copy link

ice1000 commented Nov 24, 2018

@ice1000
Copy link

ice1000 commented Nov 24, 2018

你这个语法好垃圾啊,不喜欢

@duangsuse
Copy link
Collaborator Author

duangsuse commented Nov 24, 2018

推荐阅读 https://ice1000.org/2018/11/18/SomeProspectsAboutOwO/

Thanks

你这个语法好垃圾啊,不喜欢

毕竟我现在比较菜,人的审美都是随姿势程度变化的

最后一个可能看不到的 btw

https://ice1000.org/gist/rina-spider-zhihu-stu/ md

  } catch(e) { process.stdout.write('\x1b[31m FAILED\x1b[0m\n'); continue; }

貌似编码有问题(弄错了,看到 escape 字符和红框框就以为是错了,其实是故意的(ANSI 色彩控制))

@nukc
Copy link

nukc commented Nov 24, 2018

所以你们是在玩自己设计的一套语言?

@ice1000
Copy link

ice1000 commented Nov 24, 2018

毕竟我现在比较菜,人的审美都是随姿势程度变化的

去学习些好点的语言啊。别整天抱着拖人类后腿的语言看了。

@duangsuse
Copy link
Collaborator Author

duangsuse commented Nov 24, 2018

去学习些好点的语言啊。别整天抱着拖人类后腿的语言看了。

当然啊,我现在就在学 Haskell 嘛,不过没有时间碰电脑所以学得慢罢了,但并行编程、底层二进制编译原理递归算法逆向工程和稍微不那么弱智一点的 OO 类型系统都有书有本子所以可以一起学

等学到理解「知其所以然」 Haskell 的程度就会再学 Agda 系语言的,可惜我现在连 Functor 为啥长得像是 Functor 都不知道 ,现在是 Haskell 语法定义都没看的那种

所以你们是在玩自己设计的一套语言?

嗯,准确的说是我在玩,而且我都不知道这语言的文法到底能不能做出解析器来,因为 indentation matters 太鬼畜了,而且 |> 这玩意我都不知道到底是和缩进换行语义有关还是和块转换(Ruby 的 to_proc)相关了...

@ice1000
Copy link

ice1000 commented Nov 24, 2018

当然啊,我现在就在学 Haskell 嘛

https://www.zhihu.com/question/303042890/answer/536022243

@duangsuse
Copy link
Collaborator Author

duangsuse commented Nov 29, 2018

你搞的这个东西还怪 excited 的,不知道为什么那些 JavaScript 系的前端就没有想出来,可能是平时 imperative 的东西用多了都想不到博客还可以一半用代码一半用自然语言写吧(:P ...

我也是现在才知道有 Literate Haskell 这玩意 所以这不是原创啊

这... 不是 TeX 么 -- 打住,是 TeX,不过的确是 Literate Haskell... (ghci --make *.lhs

顺便问问(请,如果有概念上的错误就是我太菜了,求轻喷),

  • Idris 和 Agda 是所谓的逻辑式语言吗?还是只是所谓的 Proof Assistance 呢,他们的主要功能可以认为是提供一个更高等的类型检查系统吗?

然后如果是,它们能不能“倒着”逆向运行呢?(没错,从王某的博客上看的

dependent type 是什么(ps. 这个有点伸手了

USTC CS 系一 type safe printf (当然作者明显没有编译过此代码示例,因为我使用 C++17 都 CE...)代码示例上提到了几种 PLT(类型理论)的概念

value -> valuefunction
type -> typegeneric
value -> typedependent type
type -> valueparametric polymorphism

然而,某 Kotlin 教程里说 generic(Kotlin 里的泛型)就是 parametric polymorphism (画上等号地 )(参形多态)
还是说他们有包含关系么

  • 『Lice 的动态作用域实现』(老文了,当然)里

所谓动态作用域知道了是时序的作用域(貌似),但静态作用域最后好像没有讲

@duangsuse
Copy link
Collaborator Author

duangsuse commented Nov 29, 2018

https://www.zhihu.com/question/303042890/answer/536022243

目前唯一有关的回答... 其他的估计都一脸蒙蔽

我类型理论现在是儿童都不及的状态,函数式理论和 Haskell 还没怎么理解... 定理证明在学就是了,昨天上午看了一个上午写了十多面草稿也才是到勉强猜出 ∧-assoc 结合律证明一部分的命题的程度

(主要还是没有啥时间去理解一大堆数学性的东西,干货多难消化要时间,然而还在国内上高二的我一周里只有半天可以碰到电脑,而且甚至因为要处理 Telegram 的输入消息以及在 Telegram 频道里讲点笔记都没时间看这些玩意,只能慢慢学)

至于 Agda 看你那点示例代码看了很久算是大概认出类型签名啥意思了,可惜还是不知道 {P Q : Set}(P Q : Set) 有什么区别(我打印你教程里你 implicit 的东西太多了... 还好《Kotlin 极简教程》这本一看就知道是工业系的书里讲 FP 讲得比较多,核心理念和历史组合态射半群含弘半群 lambda 演算集合论封闭律 Y 组合子(包括 Clojure 里那个特别难看的 Y 组合子) Functor 范畴态射都讲了), 之前见过后来忘了,记得看某个代码示例的时候 forall 和 ∀ 一起出现弄得我都不敢叫它 forall 了(每次总是这样...)

(这时候一大堆闲杂书籍一起学的优势就体现出来了,虽然看过不一定就会但至少能知道内容大致在哪,这样遇到没详细讲的玩意总是能在别的书里找到讲解和类似的内容,比较容易做到建立关系学起来也不容易忘)

btw. 什么是 Refinement Type? - 兴趣使然千里冰封的回答 - 知乎
https://www.zhihu.com/question/303886130/answer/540534316

div : (a b : Nat) -> b !== 0 -> Nat

我之前一直以为 Nat 是类似 Foo Bar Bazx y zp q r 的东西(一个类型名称的例子),直到我知道后续数和前驱数,然后又闲的没事(也就是两节课的时间原型)设计了一个(更严谨的,可以总结出形式化定义的)(我是指目前的语法上可以弄出 flex 代码、tokenize 模式、BNF 模式什么的,不是指 β-归约、W 算法之类的... 用来发 papper 并且最好是写在 papper 上的那种)高甜 静态强类型 C-like 语言 Marisa 顺便看了看 LLVM Cookbook 以便准备以后能实现它...,现在看来巧合真是越来越多了...

在区分 unsigned 和 signed 数的时候我考虑了 u8 unsigned UInt8 什么的,但最后选择了类似 C# Rational R (可能词法层面没有) Java Nature N 的方式弄了个 Nat$len 这种类型名称来,现在看来和 Idris 上面的自然数类型名称貌似相似...

Types :: Primitives

  - Numeric
    = signed =
    Int8 Int16 Int32 Int64
    = unsigned =
    Nat8 Nat16 Nat32 Nat64
    = floating point numbers =
    Num32 Num64
  - Frequently Used
  Boolean String Symbol Any Nil
  - Special
  Fn Box Nilable Never Extern

  = Marks =
  [], [size], +/*(nullable double pointer), ?(nullable)

@duangsuse
Copy link
Collaborator Author

duangsuse commented Nov 29, 2018

顺便推荐终于放假的今天在 Telegram 上看到的一张图,因为觉得很有意义就自己又画了一份,自己 Inkscape 画的那张不是多严谨,大概看起来像而已

https://t.me/Ralphonograph/425

dunningkruger

和一 beizer 曲线博文

OpenGL 中 Bézier 曲线及其 deCasteljau 剖分算法

@duangsuse
Copy link
Collaborator Author

duangsuse commented Nov 29, 2018

你是想抄 Idris 的 with abstraction 的语法?这可能需要你弄下 Layout。

... 我也是你发文讲这个了之后才知道 Layout 是代码缩进 Layout,或者说代码逻辑布局的... 看来这个的确是很需要经验和直觉,要不然各种没给定义也难找定义/定义容易混淆的东西就像英文句子里不知道其意思的词一样会影响到句子的理解

... 我们数学课里都已经学会用到这种能锻炼人类脑力的机制 implicit definition 教学方案了,这个 ∑ summation 符号 TMD 从来没给我们模式识别定义过就到处在用,Well, good. Have a nice day.

你那个新发的二维文法的文章是讲这个的...

InScript 虽然是在我基本不会 Haskell 的情况下设计的(虽然基本都是伪代码),但其实二维语法很像 Haskell...

starPlatinum = \case
  a -> \case
    e -> f
    _ -> __IMPOSSIBLE__
  c -> d

starPlatinum = \case 就是类似 InScript 里的 = |>
不过因为 when 文法上和 case of 有区别所以没有可比性只是作为例子

当然也有可选缩进

if 1 == 1.succ { never } else { println }

Layout 的部分概念以前我在写垃圾 Lite(最后因为我太菜了不会写 recursive descent method 的 parser 而报废)的时候就考虑过,不过 Lite 就垃圾多了,它没有『可选』这一说(就是 Python 式的必须换行,缩进)并且把二空格而不是一空格视为一个 Level(内部名称 indent,不过我当时好像误写为 ident 了)

不过 Lite 当时的实现思路是「CFG 转化」,因为 Lite 导致词条解释依赖额外上下文的只有缩进文法一个而已,所以我选择在内部增加 end 关键字(词法里不存在)来进行转化,

最后我花了一天多没能设计出那个算法来(我当时称之为「Deflator」),因为此算法会把

def nope()
  if true
    if false
      print 1
    elif true
      print 2
  else
    print 3

展开为

def nope()
  if true
    if false
      print 1
    end
    elif true
      print 2
    end
  else
  end
    print 3
  end
end

最后最好的结果,直到今天我发现了是因为我没有问『这行后面会不会跟一个 block』之类的简单问题...
因为原算法是根据『本行缩进 level 是否小于上一行』来加 end 的(不管考不考虑嵌套层次),诸如 else 这种就会翻车

@ice1000
Copy link

ice1000 commented Nov 29, 2018

什么辣鸡

@ice1000
Copy link

ice1000 commented Nov 29, 2018

Idris 和 Agda 是所谓的逻辑式语言吗?还是只是所谓的 Proof Assistance 呢,他们的主要功能可以认为是提供一个更高等的类型检查系统吗?

https://agda.readthedocs.io/en/latest/getting-started/tutorial-list.html#introduction-to-agda
https://www.idris-lang.org/

@nukc
Copy link

nukc commented Mar 3, 2021

考古现场

@ice1000
Copy link

ice1000 commented Mar 3, 2021

考古现场

麻了,你把这翻出来,我简直想自杀了

我竟然和这种人讨论了这么久技术 我自裁

@nukc
Copy link

nukc commented Mar 3, 2021

@ice1000 不知道你们啊,我是今天又看你的博客,一看,emmm,在想是不是之前看的啊,所以就来考古了(狗头保命,溜了溜了)

@mesondzh
Copy link

mesondzh commented May 7, 2021

考古😂

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

No branches or pull requests

8 participants