[Haskell-cafe] Proof in Haskell
Ryan Ingram
ryani.spam at gmail.com
Thu Dec 23 18:42:01 CET 2010
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
More information about the Haskell-Cafe
mailing list