Thanks for the comments. I will take a look at the type
family extension.
The definition of plusFn proposed by Jim Apple worked
nicely. The solution from apfelmus works after fixing
a small typo:
newtype Equal a b = Proof (forall f . f a -> f b )
newtype Succ f a = InSucc { outSucc :: f (S a) }
equalZ :: Equal Z Z
equalZ = Proof id
equalS :: Equal m n -> Equal (S m) (S n) -- was (S n) (S m)
equalS (Proof eq) = Proof (outSucc . eq . InSucc)
plusFn :: Plus m n i -> Plus m n k -> Equal i k
plusFn PlusZ PlusZ = Proof id
plusFn (PlusS x) (PlusS y) = equalS (plusFn x y)
Also thanks to Derek Elkins and Dan Licata for interesting
discussions about dependent sum/product. :)
sincerely,
Shin
_______________________________________________
Haskell-Cafe mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/haskell-cafe
