[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:


> 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)


> 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


More information about the Haskell-Cafe mailing list