At 2002-04-08 12:45, Lennart Augustsson wrote:
I just just wanted to say that I agree with almost everything Conor said. I find it a little odd that the extension to Haskell that allows explicit forall does not also allow you use explicit type application (and type lanbda).
What did you have in mind? data Zero; data Succ n; type Add Zero b = b; type Add (Succ a) b = Succ (Add a b); type Mult Zero b = Zero; type Mult (Succ a) b = Add b (Mult a b); type Fact Zero = Zero; type Fact (Succ n) = Mult (Succ n) (Fact n); data Foo f = MkFoo (f ()); type Succ' = Succ; type Succ'' n = Succ n; -- which of these types are the same? f1 = MkFoo undefined :: Foo Succ; f2 = MkFoo undefined :: Foo Succ'; f3 = MkFoo undefined :: Foo Succ''; f4 = MkFoo undefined :: (Add (Succ Zero)); -- Ashley Yakeley, Seattle WA