Create a gist now

Instantly share code, notes, and snippets.

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:
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 ~ 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
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
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