public
Last active

Lightweight dependent types + a proof of a 'mirror' function

  • Download Gist
gistfile1.hs
Haskell
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61
{-# LANGUAGE TypeFamilies, RankNTypes, FlexibleContexts, ScopedTypeVariables #-}
 
{-
based heavily on Ryan Ingram's lightweight type-level dependent programming
in haskell, posted to haskell-cafe:
http://www.haskell.org/pipermail/haskell-cafe/2009-June/062690.html
 
I would suggest reading it before continuing further
-}
 
data Tip = Tip
data Node x y z = Node x y z
 
 
-- the function we are making a proposition about, which mirrors a binary tree
type family Mirror x :: *
type instance Mirror (Node x y z) = Node (Mirror z) y (Mirror x)
type instance Mirror Tip = Tip
 
 
-- haskell has 'open' type families, so we must close over them with a typeclass.
-- 'caseBinTree' represents a sort of 'type case', where the case structures must prove
-- that either 'b = Tip' or 'b = Node x y z' so we can 'close' the type class and not
-- have nonsensical instances potentially interfere with our proposition below.
class BinTree b where
caseBinTree :: forall r.
b
-> (b ~ Tip => r)
-> (forall x y z. (BinTree x, BinTree z, b ~ Node x y z) => x -> z -> r)
-> r
 
instance BinTree Tip where
caseBinTree _ tip _ = tip
instance (BinTree x, BinTree z) => BinTree (Node x y z) where
caseBinTree (Node x _ z) _ f = f x z
 
{-
Induction on trees.
 
This type states, that given a predicate 'p', closed over 'x' terms defined above by BinTree, if we have a proof of 'p Tip', and a proof
of 'forall b. p a -> p c -> p (Node a b c)' (i.e. that p holds for the left and right parts of a node), then p holds
for all 'p x'.
-}
treeInduction :: forall p x. BinTree x => x -> p Tip -> (forall a b c. (BinTree a, BinTree c) => p a -> p c -> p (Node a b c)) -> p x
treeInduction b tip node = caseBinTree b isTip isNode
where
isTip :: x ~ Tip => p x
isTip = tip
isNode :: forall a x y z. (BinTree x, BinTree z, a ~ (Node x y z)) => x -> z -> p (Node x y z)
isNode x z = node (treeInduction x tip node) (treeInduction z tip node)
 
-- useful combinators at the type-level, just 'id' and 'const'
newtype I x = I { unI :: x }
newtype K x y = K { unK :: x }
 
-- now prove that 'Mirror (Mirror x) = x'
proof1 :: (BinTree x, Mirror (Mirror x) ~ x) => x
proof1 = witness
where
witness = unI $ treeInduction (undefined `asTypeOf` witness) (I Tip) (\x z -> I $ Node (unI x) undefined (unI z))

Please sign in to comment on this gist.

Something went wrong with that request. Please try again.