On Thu, May 29, 2008 at 01:44:24PM +0200, Roberto Zunino wrote:
Kim-Ee Yeoh wrote:
How about foo :: (exists. m :: * -> *. forall a. a -> m a) -> (m Char, m Bool)
Thank you: I had actually thought about something like that.
First, the exists above should actually span over the whole type, so it becomes a forall because (->) is contravariant on its 1st argument:
foo :: forall m :: * -> * . (forall a. a -> m a) -> (m Char, m Bool)
This seems to be Haskell+extensions, but note that m above is meant to be an arbitrary type-level function, and not a type constructor (in general). So, I am not surprised if undecidability issues arise in type checking/inference. :-)
Type *checking* is still decidable (System Fw is sufficiently powerful to model these types) but type inference now needs higher order unification, which indeed is undecidable.
Another valid type for foo can be done AFAICS with intersection types:
foo :: (Char -> a /\ Bool -> b) -> (a,b)
But I can not comment about their inference, or usefulness in practice.
Again, undecidable :) In fact, I believe that an inference algorithm for intersection types is equivalent to solving the halting problem. Type checking however is decidable, but expensive. Edsko