输入Haskell和ML之间的系统差异

Question

我想知道Haskell和ML的Type系统之间的完全不同.我不需要一般的差异,但只需要他们的类型系统的差异.

任何人都可以解释为什么在Haskell中引入这些差异？(为简单起见的任何优点)

提前致谢!

Answer 1

在这个答案中,我将讨论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 + Type系列+ 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的核心类型系统中是不可表达的,但是对于仿函数,人们可以解决这个问题.