Ben*_*esh 9 haskell type-theory hindley-milner
Haskell类型系统(*)的一个有趣特性是,有时你可以根据它的类型签名确定函数的确切功能(假设没有unsafe IO黑暗魔法被激活).
例如,具有类型签名的任何函数a -> a必须是标识函数,并且任何类型的函数(a,b) -> a都等效于fst.在某些情况下,您无法完全确定函数:类型中存在无数个不同的可能函数a -> Int,但它们都是常量 - 它们都忽略第一个参数.
我发现这个属性很吸引人,但我怀疑它只适用于"琐碎"的功能,如id和const.我对么？
此外,我在这里的推理仅基于直觉 - 例如,在a -> a我们中"不知道" a(与受约束的函数相反Num a => a -> a),因此除了不变地返回之外,"不能做任何事情".有没有正式的方法来处理这种扣除？
*我知道Haskell的类型系统是基于Hindley-Milner类型的系统,但我不熟悉它,不能假设任何关于它的东西
Rei*_*chs 10
您所指的概念称为参数化.以上类型的通用定量给出了参数的多态性和"统一性"的属性,是直觉这个概念,"我们不知道什么" a的forall a. a -> a,因此它比其他原样返回"不能做什么".什么均匀物业说是一种f :: [a] -> [a]不依赖于的类型a,或者更准确地说,取决于均匀就可以了:一切皆有一个"不"的[a]必须是"可行的" 所有的选择a.Wadler使用它来显示映射列表中的值然后置换列表等同于先置换和后置映射.
处理这些直觉的正式方法在例如Philip Wadler的自由定理中给出,涉及类型和关系之间的同构(实际上是部分等价关系的类别PER(per)),这表明这种一致性是一种普遍的属性.在类别中.
参数化的一个有趣结果是你可以"双向":从类型到关于那种类型的定理,从类型到那种类型的居民.Wadler的自由定理是前者和Djinn的一个例子,Djinn是一个定理证明者(一种类型的居民是"定理"类型的"证明"),是后者的一个例子.