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 _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe