Type system differences between Haskell and ML

Question

I wanted to know complete differences between Type systems of Haskell and ML. I don't need general differences, but only differences in their Type systems.

And also can anyone please explain why these differences are introduced in Haskell?(For any advantage of simplicity)

Thanks in Advance!

Answer 1

Throughout this answer I'm going to talk about Haskell 98 and SML.

Both type systems have the same foundations really, System F. This means you have basic parametric polymorphism

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

SML provides functors and modules and Haskell type classes, but both of these are really built on top of a core calculus.

The most interesting difference is that Haskell is System Fw, which is a souped up version of System F. In particular, it provides a richer notion of kinds (the types of types) allowing for things like

data Foo f a = Foo (f a)

Notice here that f is a function from a type onto another type, it's kind in other words is * -> *. In fact, Haskell 98 + Type families + PolyKinds + DataKinds extends this further by allowing arbitrary type functions. This gives you something like simply typed lambda calculus with types. For example, here's a church encoding of type level lists

{-# 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

This isn't expressible in SML's core type system, however with functors, one can hack around this.