Skip to content

@thoughtpolice /gist:750279
Created

Embed URL

HTTPS clone URL

Subversion checkout URL

You can clone with
or
.
Download ZIP
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))
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Something went wrong with that request. Please try again.