On 8/4/07, ShinCheng Mu 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
