[Haskell-cafe] Aren't type system extensions fun?
Edsko de Vries
devriese at cs.tcd.ie
Thu May 29 07:58:09 EDT 2008
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.
More information about the Haskell-Cafe