Higher-rank Polymorphism

1 minute read

On the functional programming course I attended, I learnt about some interesting parts of Haskell’s type system. I figured I’d write a blog post*.

(Standard) Haskell has what’s called let-bound polymorphism. This means that identifiers bound in a let, a where or top-level definitions can be polymorphic, whereas lambda-bound identifiers (function arguments) cannot. Here are some examples, using the (polymorphic) id function:

-- Let (OK)
polymorphicLet :: (Integer, Char)
polymorphicLet = let f = id in (f 3, f 'a')

-- Where (OK)
polymorphicWhere :: (Integer, Char) 
polymorphicWhere = (f 3, f 'a') where f = id
 
-- Top-level (OK)
f :: a -> a 
f = id 
polymorphicTopLevel :: (Integer, Char) 
polymorphicTopLevel = (f 3, f 'a')
 
-- Lambda-bound (not OK)
polymorphicInlineLambda :: (Integer, Char) 
polymorphicInlineLambda = (\f -> (f 3, f 'a')) id

This last example does not work: it is not possible to determine the type of f, and no explicit type signature has been provided**. How do we fix this? We need to give the compiler more type information!

How do we describe the type of f? Well, it’s a polymorphic function of type a -> a. So the type of the inline lambda abstraction above is something like (∀a.a -> a) -> (Integer, Char). This is an example of higher-rank polymorphism – this is where a polymorphic type appears in another type; in this case the function argument itself is polymorphic (a so-called rank-2 type).

How do we express that in Haskell? Well, we need two GHC extensions; namely ScopedTypeVariables and RankNTypes. RankNTypes allows us to express ‘for all’ (and so describe higher-rank types), and ScopeTypeVariables allows us to extend the scope of type variables into the definition of a function.

{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
 
polymorphicInlineLambda' :: (Integer, Char)
polymorphicInlineLambda' = (\(f :: forall a. a -> a) -> (f 3, f 'a')) id

et voila!

See here for the full example source code, and here for more Haskell.

*Oh, and if you’re a Haskeller and have noticed some mistake in this post, let me know, feedback welcome!

**I think GHC assumes f to be monomorphic because of the monomorphism restriction

Mansour Ahmed