[Haskell-cafe] Lightweight type-level dependent programming in Haskell

[Ryan Ingram]

(Literate Haskell post)

> {-# LANGUAGE GADTs, RankNTypes, TypeFamilies, ScopedTypeVariables, FlexibleContexts #-}
> module Dependent where

I recently discovered an interesting way of closing typeclasses while
playing with type-level peano naturals:

First we build peano integers at the type level:

> data Z = Z
> newtype S n = S n

And a couple of generally useful type-level combinators:

> newtype I x = I { unI :: x }
> newtype K x y = K { unK :: x }

(We could also include the S combinator, under a different name, but I
haven't needed it yet...)

This representation isn't "closed"; there's nothing forcing the "n" in
S n to be Z or S n.  But we can make a typeclass easily:

class Nat n
instance Nat Z where ...
instance Nat n => Nat (S n) where ...

But again, this typeclass is open.  What I recently realized is that
it's easy to close the typeclass by requiring instances to provide a
simple implementation of "typecase":

> class Nat n where
>    caseNat :: forall r. n -> (n ~ Z => r) -> (forall p. (n ~ S p, Nat p) => p -> r) -> r

By parametricity, any non _|_ implementation of caseNat has to prove
either (n ~ Z), to call the first branch, or (n ~ S p) for some other
natural p, to call the second.

> instance Nat Z where
>    caseNat _ z _ = z
> instance Nat n => Nat (S n) where
>    caseNat (S n) _ s = s n

(Interesting side note: the S n pattern match is automatically lazy,
since S is a newtype)

Somewhat surprisingly, caseNat is sufficient to prove *dependent* induction:

> induction :: forall p n. Nat n => n -> p Z -> (forall x. Nat x => p x -> p (S x)) -> p n
> induction n z s = caseNat n isZ isS where
>    isZ :: n ~ Z => p n
>    isZ = z
>    isS :: forall x. (n ~ S x, Nat x) => x -> p n
>    isS x = s (induction x z s)

What does this function mean?  Through the Curry-Howard lens, it says:

If we have a proof of P 0,
and a proof of (P x -> P (x+1)) for any natural x,
then we can prove P n for any natural n!

The proof simply proceeds by case analysis on n; we know that the
proof terminates since the recursive step works at a strictly smaller
type, and Haskell types are all finite in size.

Now, of course, this isn't any different from case analysis on this GADT:

> data Peano a where
>    Pz :: Peano Z
>    Ps :: Peano n -> Peano (S n)

> inductP :: forall n p. Peano n -> p Z -> (forall x. Peano x -> p x -> p (S x)) -> p n
> inductP Pz z s = z
> inductP (Ps n) z s = s n (inductP n z s)

In fact, the whole point of GADT case analysis is to introduce the
type-level coercions that caseNat makes explicit.  So there's not a
huge gain here.  There is one interesting benefit that the typeclass
answer gives you, however; you can let the compiler derive the proof
for you:

> witnessNat :: forall n. Nat n => n
> witnessNat = theWitness where
>   theWitness = unI $ induction (undefined `asTypeOf` theWitness) (I Z) (I . S . unI)

Then we can optimize the implementation of witness to "unsafeCoerce Z"
after the typechecker agrees with our proof.

Another useful tool is existentials and witnesses; existentials allow
you to do value-level calculation on "Nat"; witnesses allow you to
construct a proof of Nat n and return it from a proof; there's no
other way to return that something is a member of a typeclass.

> data AnyNat where AnyNat :: Nat n => n -> AnyNat
> data IsNat n where IsNat :: Nat n => IsNat n

> mkNat :: Integer -> AnyNat
> mkNat x | x < 0 = error "Nat must be >= 0"
> mkNat 0 = AnyNat Z
> mkNat x = case (mkNat (x-1)) of (AnyNat n) -> AnyNat (S n)

> natToInteger :: Nat n => n -> Integer
> natToInteger n = unK $ induction n (K 0) (K . (+1) . unK)

> prec_app = 11
> instance Show AnyNat where
>   showsPrec p (AnyNat n) = showParen (p > prec_app) (showString "mkNat " . shows (natToInteger n))

Fun exercises:

> data TEq a b where TEq :: (a ~ b) => TEq a b

1) Write a sized list GADT, and build some lists using combinators on
Nat.  Here's an example:
myReplicate a = induction witnessNat Nil (Cons a)
For me, ghc correctly infers this function to have the type
myReplicate :: (Nat n) => a -> List a n.  It's nice that I don't have
to specify n anywhere!

Try implementing fold :: Nat n => (forall x. Nat x => a -> p x -> p (S
x)) -> List a n -> p n

2) (Easy) Prove that all sized lists have a length that is a natural number:
lengthIsNat :: SizedList a n -> IsNat n

3) Prove that equality is decidable on naturals:
natEqDec :: forall x y. (Nat x, Nat y) => x -> y -> Maybe (TEq x y)

4) Write the standard "plus" type family, then prove:
plusIsNat :: forall x y. (Nat x, Nat y) => IsNat (Plus x y)
plusIsComm :: forall x y. (Nat x, Nat y) => TEq (Plus x y) (Plus y x)

(While doing this exercise, I was impressed at how good the type
coercion prover is)

5) (Challenge) Write definitions for "instance Eq AnyNat" and
"instance Num AnyNat"