QML: Explicit first-class polymorphism for ML

Claudio Russo and Dimitris Vytiniotis, MSR Cambridge

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:

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);;