On Tue, Dec 21, 2010 at 9:57 AM, austin seipp <a...@hacks.yi.org> wrote: > 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. > > https://gist.github.com/750279
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 _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe