[Haskell-cafe] Proof in Haskell

[Ryan Ingram]

On Tue, Dec 21, 2010 at 9:57 AM, austin seipp <as at 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