Rank 2 Type Example in Haskell

rank-2-types.hs

{-# LANGUAGE RankNTypes #-}

-- Example of rank-2 type, from http://blog.mno2.org/posts/2012-04-06-what-is-rank-n-types-in-haskell.html

module Main(main) where

import Prelude hiding (length)

-- The function as the first argument to check is itself
-- of rank-1 type.
-- The check function is of rank-2 type because the types for
-- the function that is its first argument get parameterized
-- themselves by the types that are the second and third
-- arguments.  When c and d are different, then the types
-- of the two instantiations of f are also different.
-- This generalizes one step beyond the example on the web
-- page by letting the return type from the function in the
-- first argument range over all types with an Eq instance.
-- The "forall a." is the only place it's required, although
-- it can be used in all rank-1 contexts, like for length
-- and iter, above, or for type parameters "c" and "d"
-- below.
-- That seems to be a sure sign you're exercising rank-N
-- behavior, the fact that the language won't infer the
-- type you want without the "forall" annotation.
-- In this case, if you just comment out the top-level
-- type definition for check and ask the language what
-- it thinks the type should be, then what you get is
-- check :: Eq a => (t -> a) -> t -> t -> Bool, e.g.
-- where the types for l1 and l2 are the same.
-- If you leave off the "forall" and make the top-level
-- declaration to be ...
-- check :: Eq b => ([a] -> b) -> [c] -> [d] -> Bool
-- ... then you get one of those horrendous error messages:
{--
    Could not deduce (c ~ a)
    from the context (Eq b)
      bound by the type signature for
                 check :: Eq b => ([a] -> b) -> [c] -> [d] -> Bool
      at /Users/tom_titchener/Documents/Dev/Haskell/Experimental/rank-2.hs:45:10-49
      ‘c’ is a rigid type variable bound by
          the type signature for
            check :: Eq b => ([a] -> b) -> [c] -> [d] -> Bool
          at /Users/tom_titchener/Documents/Dev/Haskell/Experimental/rank-2.hs:45:10
      ‘a’ is a rigid type variable bound by
          the type signature for
            check :: Eq b => ([a] -> b) -> [c] -> [d] -> Bool
          at /Users/tom_titchener/Documents/Dev/Haskell/Experimental/rank-2.hs:45:10
    Expected type: [a]
      Actual type: [c]
    Relevant bindings include
      l1 :: [c]
        (bound at /Users/tom_titchener/Documents/Dev/Haskell/Experimental/rank-2.hs:48:9)
      f :: [a] -> b
        (bound at /Users/tom_titchener/Documents/Dev/Haskell/Experimental/rank-2.hs:48:7)
      check :: ([a] -> b) -> [c] -> [d] -> Bool
        (bound at /Users/tom_titchener/Documents/Dev/Haskell/Experimental/rank-2.hs:48:1)
    In the first argument of ‘f’, namely ‘l1’
    In the first argument of ‘(==)’, namely ‘(f l1)’
--}
-- See also "explicitly quantified types" http://research.microsoft.com/en-us/um/people/simonpj/haskell/quantification.html

length :: [a] -> Int 
length (_:xs) = 1 + (length xs)
length [] = 0

-- Answers array of [0..] by length
-- of input array, as a second example
-- of a function that returns an Eq
-- instance of the same type
iter :: [a] -> [Int]
iter (_:xs) = 0 : (iter xs)
iter [] = []

check :: Eq b => (forall a. [a] -> b) -> [c] -> [d] -> Bool
check f l1 l2 = f l1 == f l2

-- Couldn't get syntax for "check" above to match this example, from 
-- article, with "forall" preceding constraint

foo :: forall a b. (Ord a, Eq  b) => a -> b -> a
foo = undefined

main :: IO ()
main = do
    print $ check length [1::Integer] ['a', 'b', 'c']
    print $ check iter [1::Integer] ['a', 'b', 'c']