Instantly share code, notes, and snippets.

# thoughtpolice/gist:750279 Created Dec 21, 2010

What would you like to do?
Lightweight dependent types + a proof of a 'mirror' function
 {-# 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))