On Tue, 17 Feb 2004 14:40:18 -0800, Ashley Yakeley <ashley@semantic.org> wrote:
Ben Rudiak-Gould <benrg@dark.darkweb.com> wrote:
Bear in mind you can't even write IO (forall t. whatever) in Haskell.
True, but why is this? Is there a deep reason why we can use nested foralls as the arguments to (->), but not as the arguments to any other type constructor?
Apparently it makes type-checking Very Very Hard. Simon PJ may have explained it to me ("impredicative", he called it), but I don't remember offhand.
Whenever you instantiate type variables with type schemes, you are impredicative. Impredicative instantiation makes type checking (much) harder -- without extra constraints, you don't even have principal types. i.e. choose :: a -> a -> a choose x y = x What is the type of "choose id" if your system is impredicative? Either "forall a. (a -> a) -> (a -> a)" or "(forall a. a->a) -> (forall a. a->a)" Note that neither of these types subsumes the other. This is why MLF adds extra constraints which enables them to give a principle type to this expression. (namely: forall a. (a >= forall a. a -> a) => a -> a) Anyway, Ben Rudiak's particular case, namely instantiating arguments of a type with type schemes, is difficult due to another problem. It is very hard to know whether an argument to a type is used contra-variantly or co-variantly (or both, or not at all). This means that we can't do a proper subsumption check on type schemes. i.e. data Contra a = Contra (a -> Int) data Co a = Co (Int -> a) data None a = None data Both a = Contra (a -> Int) | Co a In this case it may seem trivial to infer the contra/co variance of the argument but try this with some type constructors as arguments :-) In a particular case one can give type rules of course, for example for tuples or the IO monad. All the best, Daan.