[Haskell-cafe] Lightweight type-level dependent programming in
Haskell
Ryan Ingram
ryani.spam at gmail.com
Wed Jun 10 23:01:07 EDT 2009
(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"
More information about the Haskell-Cafe
mailing list