"case" operator for System-F natural numbers coded with RankNTypes fails to typecheck

Question

In Haskell, if one enables the RankNTypes extension

{-# Language RankNTypes           #-}

then one can define the natural numbers as they are encoded in System-F:

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

zero :: Nat 
zero = \z s -> z 

succ :: Nat -> Nat
succ n = \z s -> s (n z s)

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

Yay! The next step is to define the case operation: the idea is that

caseN :: Nat -> a -> (Nat -> a) -> a 
caseN n z f = "case n of 
    zero -> z 
    succ m -> f m"

Of course that's not directly possible. One thing that is possible is to define the natural numbers as normally {data Nats = Zero | Succ Nats} and define "conversions" between Nat and Nats, and then use the syntactic case construct built-in to Haskell.

In the untyped lambda calculus, caseN can be written as

caseN n b f = snd (fold (zero, b) (\(n0, _) -> (succ n0, f n0)) n)

following a trick apparently discovered by Kleene for defining the predecessor function. This version of caseN does look like it should typecheck with the type given above. (zero, b) :: (Nat, b) and \(n0, _) -> (succ n0, f n0) :: (Nat, b) -> (Nat, b), so fold (zero, b) (\(n0, _) -> (succ n0, f n0)) n :: (Nat, b).

However this doesn't typecheck in Haskell. Trying to isolate the inner function \(n0, _) -> (succ n0, f n0) with

succf :: (Nat -> b) -> (Nat, b) -> (Nat, b)
succf f (n, _y) = (succ n, f n)

reveals that the ImpredicativeTypes extension may be needed, as succf seems to require that extension. For the more typical {data Nats = Zero | Succ Nats}, the caseN construct does work (after changing to the appropriate fold, and Zero, Succ).

Is it possible to get caseN to work on Nat directly? Is a different trick needed?

Answer 1

I think the typical trick is to use a data type (or newtype, as pointed out by a commenter) wrapper. To start, instead of defining Nat as a type synonym, you can define it as:

newtype Nat = Nat { unNat :: forall a. a -> ((a -> a) -> a) }

This is isomorphic to your definition, except that you must explicitly wrap and unwrap the contents.

We can continue by writing the same definitions you had:

zero :: Nat
zero = Nat $ \z s -> z
succ :: Nat -> Nat
succ (Nat n) = Nat $ \z s -> s (n z s)
fold :: a -> (a -> a) -> Nat -> a
fold z s (Nat n) = n z s

This is basically what you already had, but now with explicit wrapping and unwrapping using Nat (as both constructor and pattern).

At this point, your final definitions just work:

caseN :: Nat -> b -> (Nat -> b) -> b
caseN n b f = snd (fold (zero,b) (\(n0,_) ->  (succ n0,f n0)) n)

succf :: (Nat -> b) -> (Nat, b) -> (Nat, b)
succf f (n,_y) = (succ n, f n)