[Haskell] Polymorphic types without type constructors?
greg at eecs.harvard.edu
Wed Feb 2 08:47:03 EST 2005
Simon Peyton-Jones wrote:
> You have it exactly right. The key word is "predicative". GHC has a
> predicative type system, that only allows you to instantiate a type
> variable with a monotype, not a polytype. An impredicative system
> (which is the one you want here) is more expressive, but it makes type
> inference very much more difficult.
Just to be anal, GHC is actually impredicative. You can instantiate
a type variable with a newtype that *contains* a polymorphic type.
So, there is no simple set-theoretic stratification of the universes of
monotypes and polytypes.
Rather, GHC enforces a sub-kind constraint on variables that precludes
them from ranging over types whose top-most constructor is a forall
(and has a few more structural constraints.) The distinction is subtle,
but important. A predicative version of Haskell would have a much,
much simpler denotational semantics, but also prevent a number of
things that are useful and interesting.
More information about the Haskell