Rank N

Type signatures

Types can be specified explicitly, with rank N, quantifiers are allowed at all places.

f :: (forall a . a -> a) -> (Int,Char)
f i = (i 5,i 'x')

g :: ((forall a . a -> a) -> (Int,Char)) -> Int
g ic = fst (ic id)

h :: (((forall a . a -> a) -> (Int,Char)) -> Int) -> Int
h iii = iii f

x = h g

Partial type signatures

Types can be partially specified, denoted by '...' (equivalent to type variable which is not implicitly quantified, and filled in by type inferencing):

f x = let g :: (forall a. a -> a) -> (Char,...)
          g h = (h 'a', h x)
      in  g id

x1 = f 3   -- :: (Char,Int)
x2 = f 'x' -- :: (Char,Char)

Impredicativity

Depending on context and/or help from the programmer, types are (or are not) propagated impredicatively. Haskell's default behavior is to instantiate arguments before binding to type variables. This default is followed, except when specified otherwise, using '~':

f :: a -> a -> a
f x y = y

x1 = f id   -- :: forall a . (a -> a) -> a -> a
x2 = f ~id  -- :: (forall a . a -> a) -> forall b . b -> b

During subsumption (asymmetric unification with coercions) quantified types are propagated when occurring at higher ranked positions, predicates may be in different order (requiring context reduction during subsumption):

data T  = C1 Int (forall a. (Eq a, Show a) => a -> a)
        | C2     (forall a. (Show a, Eq a) => a -> a)

h      :: a -> a -> Int
h _ _   = 1

test1    = h (C1 1) C2  -- :: Int
test2    = h (C1 1)     -- :: ((forall a . (Eq a,Show a) => a -> a) -> T) -> Int

Currying example:

f :: (forall a. a -> a) -> Int -> Char  
g :: (forall a. a -> a, Int) -> Char

f' = uncurry f   -- :: (forall a . a -> a,Int) -> Char
g' = curry   g   -- :: (forall a . a -> a) -> Int -> Char

Polymorphic fields

Polymorphic functions can be stored in structures, matched upon by a variable, and used polymorphically:

data T = C [forall a.a->a]

f (C (f:fs)) = (f 5,f 'x')

g x = case x of
        C y -> case y of
                 f : fs -> (f 6,f 'x')
                 _ -> (5,'x')

x1 = g (C [id])

For a value, the same holds:

data S    = C (forall a. [a])

g (C x)   = (x,x)      -- :: S -> (forall a . [a],forall b . [b])

When matching also is done on a constructor of the same type, no additional instantiation is enforced:

h (C x@[])   = (x,x)   -- :: S -> (forall a . [a],forall b . [b])
                       -- [] :: forall a . [a]

Instantiation can be enforced:

j (C (x@[] :: [Int]))   = (x,x)                            -- :: S -> ([Int],[Int])
k (C (x@[] :: [a]))     = ((x,x) :: forall a . ([a],[a]))  -- :: S -> forall a . ([a],[a])

The type signature for (x,x) can be omitted, but the experimental convention is to interpret a tuple as something to be quantified as an existential:

k' (C (x@[] :: [a]))    = (x,x)                            -- :: S -> exists a . ([a],[a])

-- AtzeDijkstra - 06 Feb 2007