[bitc-dev] RE: forall nesting

Mark P Jones mpj at cse.ogi.edu
Sun Jul 24 16:31:00 EDT 2005

| > There is a more fundamental reason why you can't have a type
| > like this, at least in any language that, like ML and Haskell,
| > is based on the Hindley Milner type system:  forall quantifiers
| > can only appear at the outermost level of a type, not nested
| > inside a constructor, which is what you have done in the example
| > above...
|
| I understand the type logic behind this statement, but there is a
| consistency issue here. Given a method such as less-than:
|
|   < : (forall ('a : Num)  (fn ('a 'a) bool))
|
| We can write at the top level prompt something like:
|
|   (1:int32, <)
|
| and we will get back something like:
|
|   (forall 'a:Num (tuple int32 (fn ('a 'a) bool)))
|
| however, note that this type had to be derived from an intermediate
| step, which was:
|
|   (tuple int32 (forall ('a:Num) (fn ('a 'a) bool)))

No, this is not a valid (Hindley-Milner) type either.

In a Hindley-Milner type system, a variable with a polymorphic type
(i.e., a type scheme) must be instantiated to a monomorphic type at
the point where it appears in the program.  (In a type inference
algorithm, where the appropriate "monomorphic type" may not be known
at the point where the variable is mentioned, we will instead
instantiate it with a type variable that can be bound to some more
specific type later on.)

For example, the syntax of *types* in a Hindley-Milner system is
typically something like the following:

t ::= a        -- type variable
|  C        -- type constant
|  t -> t   -- function type
|  (t, t)   -- pair type
|  ...

Notice that there are no foralls here; these quantifiers can only be
used in a *type scheme*, which might be described by the following
grammar:

s ::= forall a1 ... an. t    n>=0

Type schemes are used in sets of typing assumptions:

A ::= { ..., x :: s, ... }    (at most one pair for any given x)

And now we can express the typing rules of the language using judgements
of the form  A |- e : t  where A is a set of typing assumptions, e is an
expression, and t is a type (following the forall-free grammar above).

In particular, the typing rule for a variable is as follows:

(x : forall a1...an. t) \in A
------------------------------
A |-  x : [t1/a1, ..., tn/an]t

where [t1/a1, ..., tn/an] denotes substitution of arbitrary types (again,
and with apologies for laboring the point, without any foralls, so the
result of the substitution is also a type expression without foralls).

When you add classes/predicates/constraints, you get the following
extension of the typing rule for variables:

(x : forall a1...an. P => t) \in A
Q ||- [t1/a1, ..., tn/an] P
----------------------------------
Q | A |-  x : [t1/a1, ..., tn/an]t

Here, P and Q are sets of predicates and ||- represents the "entailment"
relation that tells us when one set of predicates (on the right of ||-)
is implied by another (on the left of ||-).

So, for the (1:int32, <) example that started this whole thing, we will
end up with a judgement of the form:

Q | A |- (1:int32, <) : (int32, fn (b,b) bool)

where A is a set of assumptions that includes your original type for <
and Q is a set of predicates such that Q ||- Num b ... in the simplest
case, for example, it might be that (Num b) is actually a member of Q.

Now, if we were actually type checking a larger expression, such as
let x = (1:int32, <) in e (ignoring value restrictions etc..), then
we would want to put as general a binding for x as possible in the
assumptions that we use to type check e.  In this case, we'd end up
looking for a judgement of the form  Q' | A' |- e : t'  where:

Q' is obtained from Q by removing the Num b predicate;
A' is obtained from A by adding the assumption
x : (forall b. Num b => (int32, fn (b,b) bool)); and
t' is the type for the whole let expression.

| That is: the forall was hoisted to the outside by rewriting.

The point of all this is that we're dealing with a fundamental
detail of the way in which the type system is constructed, and
it's not something that can be addressed by rewriting.  If you
want to get some insights into how you can begin to lift some
of the restrictions on the use of forall in a type system without
giving up on type inference, then you might want to consult some
of the papers listed below.  Be warned, however, that, until you
know that you need the extra flexibility these systems can provide,
this could just be a major distraction ...

All the best,
Mark

References:

Qualified types for MLF.
Daan Leijen and Andres Löh

Practical type inference for arbitrary-rank types.
Simon Peyton Jones, Stephanie Weirich, Dimitrios Vytiniotis, Mark Shields
http://research.microsoft.com/Users/simonpj/papers/higher-rank/index.htm

First Class Polymorphism with Type Inference.
Mark P Jones
http://www.cse.ogi.edu/~mpj/pubs/fcp.html

Putting type annotations to work.
Martin Odersky, Konstantin Laufer
http://portal.acm.org/citation.cfm?id=237729