[Haskell-cafe] Re: Developing Programs and Proofs Spontaneously using GADT

[Shin-Cheng Mu]

Thanks for the comments. I will take a look at the type
family extension.

The definition of plusFn proposed by Jim Apple worked
nicely. The solution from apfelmus works after fixing
a small typo:

> newtype Equal a b = Proof (forall f . f a -> f b )
>
> newtype Succ f a  = InSucc { outSucc :: f (S a) }
>
> equalZ :: Equal Z Z
> equalZ = Proof id
>
> equalS :: Equal m n -> Equal (S m) (S n)    -- was (S n) (S m)
> equalS (Proof eq) = Proof (outSucc . eq . InSucc)
>
> plusFn :: Plus m n i -> Plus m n k -> Equal i k
> plusFn PlusZ     PlusZ     = Proof id
> plusFn (PlusS x) (PlusS y) = equalS (plusFn x y)

Also thanks to Derek Elkins and Dan Licata for interesting
discussions about dependent sum/product. :)

sincerely,
Shin