[Haskell-cafe] Developing Programs and Proofs Spontaneously using
GADT
Jim Apple
jbapple+haskell-cafe at gmail.com
Sat Aug 4 12:11:37 EDT 2007
On 8/4/07, Shin-Cheng Mu <scm at iis.sinica.edu.tw> wrote:
> Unfortunately, unlike Omega, Haskell does not provide type
> functions.
Something similar is coming:
http://haskell.org/haskellwiki/GHC/Indexed_types#Instance_declarations_2
> Haskell does not know that Plus m n is actually
> a function and cannot conclude that i=k.
>
> To explicitly state the equality, we assume that there is
> a function plusFn which, given a proof of m + n = i and
> a proof of m + n = k, yields a function converting an i
> in any context to a k. That is:
>
> plusFn :: Plus m n i -> Plus m n k
> -> (forall f . f i -> f k)
>
[snip]
> How do I define plusFn? I would like to employ the techniques
> related to equality types [3,4,5], but currently I have not
> yet figured out how.
plusFn :: Plus m n h -> Plus m n k -> f h -> f k
plusFn PlusZ PlusZ x = x
plusFn (PlusS p1) (PlusS p2) x =
case plusFn p1 p2 Equal of
Equal -> x
data Equal a b where
Equal :: Equal a a
Jim
More information about the Haskell-Cafe
mailing list