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

[Jim Apple]

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