Recent years have seen a revival of interest in extending ML's predicative type inference system with impredicative quantification in the style of System F, for which type inference is undecidable.

QML is a modest extension of ML with System F types: the heart of the idea is to extend the language of types with unary universal and existential quantifiers. The introduction and elimination of a quantified type is never inferred but indicated explicitly by the programmer by supplying the quantified type itself. Quantified types co-exist with ordinary ML schemes, which are in turn implicitly introduced and eliminated at let-bindings and use sites, respectively.

QML does not impose any restriction on instantiating quantified variables with quantified types; neither let- nor lambda-bound variables ever require a type annotation, even if the variable's inferred scheme or type involves quantified types. This proposal, albeit more verbose in terms of annotations than others, is very simple to specify, implement, understand, and reason about.

Downloads:

- paper (to appear at ML Workshop 2009).
- Coq formalization of the main results (requires Coq8.1pl4) (uses Aydemir et. al's Coq Metatheory library , extending a sample formalization of "Pure ML".)
- Caml light source code for toy implementation, requires Caml Light.

Here's an example of what QML code looks like:

let id = {!'a. 'a -> 'a} fun x -> x;; % forall introduction let idnat = id {!'a. 'a -> 'a} 1;; % forall elimination (at int) let idbool = id {!'a. 'a -> 'a} true;; % forall elimination (at bool) let idpoly = id {!'a. 'a -> 'a};; % forall elimination (at 'b) let idclient = fun x -> let y = x {!'a. 'a -> 'a} in y y;; % ordinary abstraction of a value with forall type let client = idclient id;; % ordinary application to a value with forall type

Here's a larger example of modular programming in QML using mixed universal (!) and existential (?) quantifiers - see the paper for commentary:

type sig ('a,'r, 'b) = ( ('a -> 'r) * % init a ('r -> int -> 'a) * % sub r i ('r -> int -> 'a -> 'r) * % update r i a (('a -> 'b -> 'b) -> 'b -> 'r -> 'b ) % fold f b r );; let base = {?'r !'b (sig('a,'r,'b))} ((fun a -> a), % init (fun r -> fun i -> r), % sub (fun r -> fun i -> fun a -> a), % update (fun f -> fun b -> fun r -> f r b) % fold );; let step = fun x: ?'r !'b (sig('a,'r,'b)) -> let (xinit,xsub,xupdate,xfold) = x in let init = fun a -> ((xinit a), (xinit a)) in let sub = fun r -> fun i -> if (i mod 2) = 0 then (xsub (fst r) (i / 2)) else (xsub (snd r) (i / 2)) in let update = fun r -> fun i -> fun a -> if (i mod 2) = 0 then ((xupdate (fst r) (i /2) a),(snd r)) else ((fst r),(xupdate (snd r) (i / 2) a)) in let fold = fun f -> fun b -> fun r -> xfold f (xfold f b (fst r)) (snd r) in {?'r!'b (sig('a,'r,'b))} (init,sub,update,fold);; let rec mkMonoArray n = if(n=0) then base else step(mkMonoArray(n - 1));; let mkPolyArray = fun n -> {!'a(?'r.!'b.sig('a,'r,'b))} (mkMonoArray n);;