(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"