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