Haskell 和 ML 之间的类型系统差异答案

【问题标题】：Type system differences between Haskell and MLHaskell 和 ML 之间的类型系统差异
【发布时间】：2013-12-16 03:01:23
【问题描述】：

我想知道 Haskell 和 ML 的类型系统之间的完全区别。我不需要一般差异，只需要它们的类型系统的差异。

还有谁能解释一下为什么在 Haskell 中引入了这些差异？（为了简单起见）

提前致谢！

【问题讨论】：

“我只是好奇这两种语言中哪一种更好”。这对于 stackoverflow 来说是题外话，因为它是一个“[问题] 要求我们推荐或查找工具、库或最喜欢的非现场资源对于 Stack Overflow 来说是题外话，因为它们往往会吸引固执己见的答案和垃圾邮件。相反，描述问题以及迄今为止为解决问题所做的工作。”

标签： haskell type-conversion ml

【解决方案1】：

在整个答案中，我将讨论 Haskell 98 和 SML。

这两种类型系统确实具有相同的基础，System F。这意味着你有基本的参数多态性

foo :: a -> b -> a
foo : 'a -> 'b -> 'c

SML 提供函子和模块以及 Haskell 类型的类，但这两者实际上都是建立在核心演算之上的。

最有趣的区别是 Haskell 是 System Fw，它是 System F 的升级版。特别是，它提供了更丰富的种类（类型的类型）概念，允许诸如

data Foo f a = Foo (f a)

注意这里f 是一个从一个类型到另一个类型的函数，它的类型是* -> *。事实上，Haskell 98 + Type family + PolyKinds + DataKinds 通过允许任意类型函数进一步扩展了这一点。这为您提供了类似于带有类型的简单类型的 lambda 演算。例如，这是类型级别列表的教堂编码

{-# LANGUAGE TypeFamilies,  EmptyDataDecls #-}

-- So we can box things up to partially apply them
type family Eval e
type instance Eval (Car a b) = a
type instance Eval (Cdr a b) = b
type instance Eval (Cons a b f) = Eval (f a b)

data Car a b
data Cdr a b
data Cons a b (f :: * -> * -> *)

type First p  = Eval (p Car)
type Second p = Eval (p Cdr)

foo :: First (Cons (First (Cons Int Bool)) String)
foo = 1

这在 SML 的核心类型系统中是无法表达的，但是使用函子，可以解决这个问题。

【讨论】：