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

Justin Carrey 发表于 Dev

贾斯汀·凯瑞（Justin Carrey）

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

还有谁能解释为什么Haskell引入了这些差异？（出于简单性的考虑）

提前致谢！

丹尼尔·格拉泽（Daniel Gratzer）

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

这两种类型的系统都具有相同的基础实在，系统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 +类型家族+ 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