为什么最初的Lisp是基于untyped lambda calculus而不是typed lambda calculus


#21

只要是 strong normalizing,不管是否 typed or untyped 都可以避免停机。也就是说,如果我把 Lisp 的定义修改一下,全改成 total function,另外只允许能证明 terminate 的递归调用,整个系统就是 strong normalizing 的,没什么了不起的。


#22

读 “请注意” 那一段


#23

沒有 Flash, Could someone help copy that to here


#24


#25

这个Y组合子其实还是用了trick

newtype Mu a = Roll { unroll :: Mu a -> a }

注意:这里的Mu是具名的,它引用自身了,这是因为Haskell支持递归类型,而STLC不支持。


#26

不仅STLC不支持,Haskell对应的typed LC是STLC的扩展System F(不看rank-N types的话),System F也不支持recursive bindings所以写不出不动点组合子。但是Haskell本身是有不动点组合子的,原因的确就是Haskell支持任意递归。这也是从实用的角度出发才加上去的,对于一门不是针对定理证明的语言来说turing completeness还是很重要的


#27

Martin-Löf,System F 的 inconsistent extension。


#28

我现在比较困惑的是,函数式编程范式固然是很好的,比如golang和rust里都加入了这个范式,js写这种范式也很简便。但当发现很多人研究type lambda之类的,我又迷茫了。我们的目的不是开发吗?搞太多技巧,对生产性有什么提高吗?

另外,我虽然也经常在golang,rust,js中写lambda,在Ruby中写block。但并不清楚untyped与typed的区别。有人科普一下吗?


#29

他们是数学家,不是工程师


#30

如果想知道为什么会有LC的话,可以去看希尔伯特的23个问题。当初只是为了设计出一个完备,一致的公理化系统而已。跟计算机没太大的关系。


#31

计算机也有搞逻辑的