On Tue, Dec 21, 2010 at 9:57 AM, austin seipp
For amusement, I went ahead and actually implemented 'Mirror' as a type family, and used a little bit of hackery thanks to GHC to prove that indeed, 'mirror x (mirror x) = x' since with a type family we can express 'mirror' as a type level function via type families. It uses Ryan Ingram's approach to lightweight dependent type programming in Haskell.
Thanks for the shout out :) I think the type of your proof term is incorrect, though; it requires the proof to be passed in, which is sort of a circular logic. The type you want is proof1 :: forall r x. BinTree x => ((x ~ Mirror (Mirror x)) => x -> r) -> r proof1 t k = ... Alternatively, data TypeEq a b where Refl :: TypeEq a a proof1 :: forall x. BinTree x => x -> TypeEq (Mirror (Mirror x)) x proof1 t = ... Here's an implementation for the latter newtype P x = P { unP :: TypeEq (Mirror (Mirror x)) x } baseCase :: P Tip baseCase = P Refl inductiveStep :: forall a b c. P a -> P c -> P (Node a b c) inductiveStep (P Refl) (P Refl) = P Refl proof1 t = unP $ treeInduction t baseCase inductiveStep (I haven't tested this, but I believe it should work) -- ryan