[Haskell-cafe] Re: Developing Programs and Proofs
Spontaneously using GADT
Shin-Cheng Mu
scm at iis.sinica.edu.tw
Sun Aug 5 23:31:09 EDT 2007
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
More information about the Haskell-Cafe
mailing list