Mirror operation on trees with correctness proof.

mirror.hs

{-# LANGUAGE TypeFamilies, GADTs, RankNTypes #-}

data Tip
data Node x y z

data Tree a where
  Tip :: Tree Tip
  Node :: Tree x -> y -> Tree z -> Tree (Node x y z)

type family Mirror a :: *
type instance Mirror Tip = Tip
type instance Mirror (Node x y z) = Node (Mirror z) y (Mirror x)

mirror :: Tree a -> Tree (Mirror a)
mirror Tip = Tip
mirror (Node x y z) = Node (mirror z) y (mirror x)

treeInduction :: p Tip -> (forall a b c. p a -> p c -> p (Node a b c)) -> Tree a -> p a
treeInduction tip _    Tip          = tip
treeInduction tip node (Node a _ c) = node (treeInduction tip node a) (treeInduction tip node c)

data Equal a b where
  Refl :: Equal a a
  
newtype Proof a = Proof { unProof :: Equal (Tree a) (Tree (Mirror (Mirror a))) }

proof :: Tree a -> Proof a
proof = treeInduction (Proof Refl) (\(Proof Refl) (Proof Refl) -> Proof Refl)