MLF

September 2001 - July 2003: Didier Rémy and I (Didier Le Botlan) studied and designed MLF, which is my PhD thesis work.

Publication

I presented MLF at ICFP 2003. The article is available here, but under copyright: mlf-icfp.pdf mlf-icfp.ps.gz mlf-icfp.ps mlf-icfp.dvi BibTeX : mlf-icfp.bib
The slides can be viewed with Active-DVI or Ghostview : mlf-icfp-slides.dvi mlf-icfp-slides.ps.gz (update September, 2003)

My PhD thesis is the long version of MLF. It can be found on my new webpage at Saarland University.

I also gave a presentation of MLF at APPSEM 2003 in Nottingham (March 2003).

A presentation of MLF (ML to the power of System F)

I study an extension of ML which makes it possible to get second-order polymorphism, as we have in System F, but keeping type inference. When a parameter of a lambda-abstraction is used polymorphically, we require an explicit type annotation in the source code.

In short, we are still able to type (and to infer the types of) all ML programs. We cannot type functions that use their argument polymorphically, such as fun x -> x x, but this becomes possible when the function is decorated with a type annotation. Indeed, fun (x:['a] 'a -> 'a) x x is typable in our system. Remark that fun x -> (x, 42), which only takes an argument and puts it in a pair, not using the argument polymorphically, can be given the type (['a] 'a -> 'a) -> (['a] 'a -> 'a) * int when applied to id, that is, the argument can be automatically given a polymorphic type, provided we do not use its polymorphism. We can type such expressions in MLF, without requiring any type annotations.

As a result, it becomes possible to encode System F in MLF, putting annotations only on lambda-abstractions. Interestingly, type abstractions and type applications can be totally omitted. Moreover, lambda-annotations that do not use their argument polymorphically can be omitted too.

This work continues previous work done by Didier Rémy and Jacques Garrigue "Semi-Explicit First Class Polymorphism" (PolyML). In PolyML, polymorphic objects have to be explicitly created: they are explicitly boxed. In order to use such polymorphic values, it is necessary to explicitly unbox them first. In MLF, boxing and unboxing is left implicit, so the programming style is more natural.

Implementation

I implemented a prototype type-checker MLF, in OCaml of course. Feel free to contact me if you want to test it by yourself. My email is given on my main page.

Examples

Here is an example session with this prototype. Type annotations are highlighted like this. Some type annotations below are not necessary, but leads to a more readable inferred type. Such unnecessary type annotations are highlighted like this.

Basic use of polymorphic annotations

(* First define an alias for a polymorphic type *)
# type sid = ['a] 'a -> 'a ;;
TYPE   sid defined.


(* fun x -> x x requires an annotation *)
# let delta = fun (x:sid) -> x x ;;
val delta : ['b = sid] ['c > sid] 'b -> 'c

# let id = fun x -> x ;;
val id : ['a] 'a -> 'a

# delta id ;;
val: sid
= <fun> fun x -> x


(* Better: app delta id is also typable. *)
# let app f arg = f arg ;;
val app : ['a] ['b] ('a -> 'b) -> 'a -> 'b

# app delta id ;;
val: sid
= <fun> fun x -> x

Church encoding of Integers

# type Int = ['a] ('a -> 'a) -> ('a -> 'a) ;;
TYPE   Int defined.

# let succ (n:Int) = fun f x -> f (n f x) ;;
val succ : ['b = Int] ['c > ['a1] ('a1 -> 'a1) -> 'a1 -> 'a1] 'b -> 'c

(* The annotation is not necessary, but makes the type more readable. *)
#  let succ = (succ: Int -> Int) ;;
  val succ : ['a = Int] ['b = Int] 'a -> 'b

(* Encodings for the integers 0, 1 and 2 *)
# let c_i0 = (fun f x -> x : Int)
  let c_i1 = (fun f x -> f x : Int)
  let c_i2 = (fun f x -> f (f x) : Int) ;;
val c_i0 : Int
val c_i1 : Int
val c_i2 : Int

# let plus (n:Int) (m:Int) = ( fun f x -> m f (n f x) : Int) ;;
val plus : ['b = Int] ['c > ['d = Int] ['e > Int] 'd -> 'e] 'b -> 'c

(* Polymorphic values can be put in a list *)
# let mylist = [ c_i0; c_i1; c_i2; plus c_i2 c_i2 ] ;;
val mylist : ['b > Int] list ('b)

# let fourth l = car (cdr (cdr (cdr l))) ;;
val fourth : ['a] list ('a) -> 'a

# fourth mylist ;;
val: Int
= <fun> fun f x -> m f (n f x)

(* We do not need annotations to read or to use elements of the polymorphic list *)
# plus (fourth mylist) c_i1 ;;
val: Int
= <fun> fun f x -> m f (n f x)


# let five = plus (fourth mylist) c_i1 ;;
val five : Int

(* We test that five is actually 5 *)
# five (fun x -> x+1) 0 ;;
val: int
= 5

Existentials

In System F, the existential type Exists('a) t('a) can be encoded as (['a] t('a) -> 'b) -> 'b. We use this encoding in the following example. make_ex1 takes a value with type 'a * ('a -> unit) for some 'a and returns a value with type ['b] (['a] t('a) -> 'b) -> 'b, which is an encoding of Exist ('a) 'a * ('a -> unit). make_ex2 builds a value with type Exist ('a) 'a * 'a * ('a -> 'a -> bool).

(* First, some useful functions *)
# let eqstring s1 s2 = (s1^"A" = s2^"A")
  let eqint i1 i2 = (i1 - i2) = 0
  let eqbool b1 b2 = if b1 then b2 else (not b2)
  let ignore x = ()
  let rec listiter f ll =
    if ll = [] then ()
    else begin ignore (f (car ll)) ; listiter f (cdr ll) end
;;
val eqstring : string -> string -> bool
val eqint : int -> int -> bool
val eqbool : bool -> bool -> bool
val ignore : ['a] 'a -> unit
val listiter : ['a] ['b] ('a -> 'b) -> list ('a) -> unit

# let make_ex1 x (f:['a] ('a * ('a -> 'c)) -> 'b) = f x
  let make_ex2 x (f:['a] ('a * 'a * ('a -> 'a -> 'c)) -> 'b) = f x
;;
val make_ex1 : ['b] ['a1] ['d > ['c] ['e = ['a] 'a * ('a -> 'b) -> 'c] 'e -> 'c] 'a1 * ('a1 -> 'b) -> 'd
val make_ex2 : ['b] ['a1] ['d > ['c] ['e = ['a] 'a * 'a * ('a -> 'a -> 'b) -> 'c] 'e -> 'c] 'a1 * 'a1 * ('a1 -> 'a1 -> 'b) -> 'd

(* We build a list of existentials. *)
# let ex_list1 = [ make_ex1 ("A String", print_string) ;
                 make_ex1 (8250, print_int) ;
                 make_ex1 (true, print_bool) ]

  let ex_list2 = [ make_ex2 ("String", "String", eqstring) ;
                 make_ex2 ( 1250, 4890, eqint) ;
                 make_ex2 ( true, false, eqbool) ]
;;
val ex_list1 : ['c > ['b] ['d = ['a] 'a * ('a -> unit) -> 'b] 'd -> 'b] list ('c)
val ex_list2 : ['c > ['b] ['d = ['a] 'a * 'a * ('a -> 'a -> bool) -> 'b] 'd -> 'b] list ('c)

(* Test the first list. *)
(* Since existentials are encoded as functions ("abstractions") expecting a polymorphic function ("user"),
   opening an existential consists in applying the abstraction to a polymorphic "user".
   Remark that no type annotation is needed. *)
# let test1 = listiter (fun ex -> ex (fun p -> (snd p) (fst p))) ex_list1 ;;
val test1 : unit

(* The following line is the output performed by the evaluation of test1 *)
A String8250 true

(* Test the second list. *)
# let test2 = listiter (fun ex -> ex (fun t ->
  let arg1 = fst t
  and arg2 = fst (snd t)
  and eqf  = snd (snd t) in
  let areequal = eqf arg1 arg2
  in print_bool areequal )) ex_list2
;;
val test2 : unit
 true  false  false

Propagation of annotations

(* Type annotations can be put in an interface file, and automatically propagated. *)

# let (delta : sid -> sid) = fun x -> x x ;;
val delta : ['sid1 = sid] ['sid = sid] 'sid1 -> 'sid

# let (delta : sid -> 'a) = fun x -> x x ;;
val delta : ['a1 > sid] ['sid = sid] 'sid -> 'a1

Version Française.