[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