[Prev][Next][Index][Thread]
Moving ML/Haskell toward second-order polymorphism
This message proposes the addition of some of the power of full
second-order polymorphism into a language (Haskell) which has an ML-
like type discipline. For the purpose of this message, Haskell's
overloading mechanism is irrelevant.
The question I want to ask is: what similar work already exists?
Here's the idea. We want to introduce a few constants which are
functions which have arguments with for-all types at their top
level. For example:
newST :: forall a. (forall b. ST b a) -> a
This type can't be written in ML or Haskell, where all the for-alls
must occur at the top. Because of this restriction the for-alls
are usually omitted, but I'll write them in explicitly in this
message.
What is newST useful for? It is *the* key building block in our
integration of state-manipulating computation into a pure, lazy
functional language. The approach is based on monads, and is fully
described in an up-coming paper. For now, all we need to know is
the type of newST.
Supposing, then that newST is provided as a constant, can we perform
type inference on applications of newST? Yes, it seems we can. To
speak operationally, suppose we have an application
(newST e)
To type this, type-check e, giving the (unquantified) type t. Now
unify t with (ST b a), with fresh type variables a,b. Then check
that the type variable b is still unconstrained, just as one does
when typing a let-expression. That's it.
Let's formalise this a little. First, define our types:
a,b,c type variables
a_,b_ ::= a,b,c... sequences of type variables
s,t,u ::= a | s->t monomorphic types
s_,t_,u_ ::= s,t,u... sequences of monomorphic types
v,w ::= forall a_ . s polymorphic types
Nothing unusual there. Now here's a rule for typing things like
applications of newST:
A |- f :: forall a_. (forall b_.s) -> t
A |- e :: s[u_/a_]
b_ not free in A
-----------------------------
A |- f e :: t[u_/a_]
The u_ is just the usual bunch of arbitrary types which say which
types we instantiate the type variables a_ to. The argument e must
have type s, and its universally quantified variables b_ must
unconstrained. This rule is easy to extend for multiple arguments.
Notice the restrictions I've given for the type of f. It can be
more general than a ML type, because not all the foralls are at the
top; but the result type t can't be a forall type, and the foralls
must be at the top of the argument type. I've placed these
restrictions because they are permissive enough to permit the extra
constants I want (newST and friends) but restrictive enough that I
can still type applications without help from the programmer.
Notice too, that the rule only handles applications of an identifier
to some arguments. It can't handle an expression like
cons newST (cons f nil)
Typing this would require me to unify the type of newST with the
type of f, which would require unification of types with foralls in
them.
There's nothing very exciting about any of this, though it has
considerable practical importance for us. What I'd like to do is to
build on existing work to do something more general and less ad hoc.
The worst ad-hoc-ness seems to be:
* forall types allowed "at the top level of arguments" only
* saturated applications compulsory for constants with nested-
foralls in their type
* there's no way of writing functions with nested foralls in their
types; they have to be built in. Mind you, I'm pretty sure that
we'd need some explicit guidance from the programmer to get the
right second order type from a definition of newST. Inference is
hopeless.
Does anyone know of other relevant work? Is unification of types
involving foralls easy? Is the rule I've given sound? I know of
O'Toole & Gifford (PLDI 89); it seems to me that they assume
second-order unification in their Extended Unification lemma. In any
case they'd require applications of newST to be written
newST (close e)
where the "close" tells the type-inferencer to generalise the type of e.
But (a) I don't want to have to write the close in, and
(b) I think the type of (close e) would come out to be
(forall a,b. ST b a)
since it hasn't yet been unified with the argument type of newST.
Someone must have worked all this out before. Anyone have any
pointers?
Thanks
Simon Peyton Jones