gra*_*ero 1 haskell clojure hindley-milner
我试图通过在我经常使用的语言Clojure中实现算法W来自学Hindley-Milner类型推断.我遇到了let推理的问题,我不确定我做错了什么,或者我期望的结果是否需要算法以外的东西.
基本上,使用Haskell表示法,如果我尝试推断它的类型:
\a -> let b = a in b + 1
我明白了:
Num a => t -> a
但我应该得到这个:
Num a => a -> a
同样,我实际上是在Clojure中这样做,但我不相信问题是Clojure特有的,所以我使用Haskell表示法使它更清晰.当我在Haskell中尝试它时,我得到了预期的结果.
无论如何,我可以通过将每个let转换为函数应用程序来解决该特定问题,例如:
\a -> (\b -> b + 1) a
但后来我失去了let多态性.由于我对HM没有任何先验知识,我的问题是我是否在这里遗漏了一些东西,或者这只是算法的工作方式.
编辑
如果有人有类似的问题,并想知道我是如何解决它的,那我就是按照Algorith W Step by Step进行操作.在第2页的底部,它说"将Types方法扩展到列表有时会很有用".因为它对我来说听起来不是强制性的,所以我决定跳过那部分并稍后重新审视.
然后我将ftv函数TypeEnv直接翻译成Clojure,如下所示:(ftv (vals env)).由于我已经实现ftv了一个cond表单并且没有seqs 的子句,所以它只是返回nil了(vals env).这当然正是静态类型系统设计要捕获的那种错误!无论如何,我刚刚重新定义了ftv与env地图有关的条款,(reduce set/union #{} (map ftv (vals env)))并且它有效.
很难说出什么是错的,但我猜你的概括是错误的.
我们手动输入术语.
\a -> let b = a in b + 1
首先,我们a将一个新的类型变量与之相关联a :: t0.
然后我们输入b = a.我们也得到b :: t0了.
然而,这是关键的一点,我们应该不能一概而论的类型b来b :: forall t0. t0.这是因为我们只能概括在环境中不会发生的tyvar:相反,我们确实存在t0于环境中a :: t0.
如果你对它进行概括,你会得到一种太普通的方式b.然后b+1变成b+1 :: forall t0. Num t0 => t0,并且整个术语forall t0 t1. Num t1 => t0 -> t1从因为类型for a和b不相关(t0一旦被推广,可以被alpha转换为t1).