How to work with higher rank types

Question

Playing with the church numerals. I run into the situation I can't guide the GHC type-checker around higher order types.

First I wrote an version, without any type signatures:

module ChurchStripped where

zero z _ = z
inc n z s = s (n z s)
natInteger n = n 0 (1+)

add a b = a b inc

{-
*ChurchStripped> natInteger $ add (inc $ inc zero) (inc $ inc $ inc zero)
5
-}

mult a b = a zero (add b)

{-
*ChurchStripped> natInteger $ mult (inc $ inc zero) (inc $ inc $ inc zero)
6
-}

The inferred type of mult is horrible, so I tried to clean-up the types with a type definitions:

module Church where

type Nat a = a -> (a -> a) -> a

zero :: Nat a
zero z _ = z

inc :: Nat a -> Nat a
inc n z s = s (n z s)

natInteger :: Nat Integer -> Integer
natInteger n = n 0 (1+)

{- `add :: Nat a -> Nat a -> Nat a` doesn't work, and working signature looks already suspicious -}

add :: Nat (Nat a) -> Nat a -> Nat a
add a b = a b inc

{-
*Church> natInteger $ add (inc $ inc zero) (inc $ inc $ inc zero)
5
-}

mult :: Nat (Nat a) -> Nat (Nat a) -> Nat a
mult a b = a zero (add b)

{-
*Church> natInteger $ mult (inc $ inc zero) (inc $ inc $ inc zero)
6
-}

It works, but the types aren't as clean as they could be. Following the System F definitions I tried:

{-# LANGUAGE RankNTypes #-}

module SystemF where

type Nat = forall a. a -> (a -> a) -> a

zero :: Nat
zero z _ = z

inc :: Nat -> Nat
inc n z s = s (n z s)

natInteger :: Nat -> Integer
natInteger n = n 0 (1+)

{- This doesn't work anymore

add :: Nat -> Nat -> Nat
add a b = a b inc

   Couldn't match type `forall a1. a1 -> (a1 -> a1) -> a1'
                 with `a -> (a -> a) -> a'
   Expected type: (a -> (a -> a) -> a) -> a -> (a -> a) -> a
     Actual type: Nat -> a -> (a -> a) -> a
   In the second argument of `a', namely `inc'
   In the expression: a b inc
   In an equation for `add': add a b = a b inc

-}

I guess it should be possible to write add with Nat -> Nat -> Nat type signature, but I have no idea how.

P.S. actually I started from the bottom, but it maybe easier to present this problem this way.

The forall introduces higher ranked types, and this is surely not what you want here. — Ingo
To put it differently: every Nat you mention in your type will have its own a type variable, that cannot be unified with any other type variable in your signatur, but apparently, wehn you write Nat -> Nat you want the as be the same. — Ingo
@Ingo, no, really want it to stay universal. It's a bit like id id case (which isn't that interesting, but works). gist.github.com/phadej/8540770 — phadej
Perhaps you want to define the type as (a->a)->(a->a) instead. — n. 1.8e9-where's-my-share m.

Lambdageek Lambdageek · Accepted Answer · 2014-01-21T14:23:29

bennofs is right, you really want to help the typechecker along here, in particular in add where you need to instantiate the a in forall a . a -> (a -> a) -> a with Nat (ie, the same forall a . ... type).

One way to do that is to introduce a newtype that wraps the polymorphic type:

newtype Nat' = N Nat

Now you can go between Nat and Nat' via N, and back using unN

unN :: Nat' -> Nat
unN (N n) = n

(It's worth noting at this point that newtype Nat' = N Nat is a different beast from data Nat2 = forall a . N2 (a -> (a -> a) -> a). The latter requires -XExistentialQuantification because it says that for some particular choice of a, you can make a Nat2. On the other hand, the former still says that if you have a -> (a -> a) -> a for any arbitrary a, then you can make a Nat'. For Nat' you need -XRankNTypes, but you don't need existentials.)

Now we can also make inc' to increment a Nat':

inc' :: Nat' -> Nat'
inc' (N n) = N (inc n)

And we're ready to add:

add :: Nat -> Nat -> Nat
add n m = unN (n (N m) inc')

The reason this works is because now instead of trying to convince GHC to instantiate the type of n with a polymorphic type ∀ a . a -> (a -> a) -> a on its own, the N acts as a hint.

Example:

> natInteger (add (inc zero) (inc zero))
2

How to work with higher rank types

4 Answers