DIPARTIMENTO   DI   INFORMATICA
Università di Torino

Rank-2 Intersection and Polymorphic Recursion for (a subset of) Caml

EXAMPLES


Index


1.0 About recursive definitions that are |-21-typable
1.1 Non-simple recursive definitions that are |-22-typable
1.2 ML-typable recursive definitions that get a more precise typing in |-22
1.3 Milner/Microft typable recursive definitions that are |-22-typable
1.4 Milner/Microft typable recursive definitions that are |-23-typable (and not |-22 typable)
1.5 ML-typable (and, therefore, |-21,ML-typable) recursive definitions that are not |-2k-typable, for all k >= 1.

1.0 About recursive definitions that are |-21-typable

System |-21 is able to type only recursive definitions {x=e} that have principal pair
<{x_1:'a_1, ..., x_n:'a_n}; 'a>
where
x_1, ..., x_n (n>=0)
are the free variables of e different from x and
'a_1, ..., 'a_n, a'
are distinct type variables. The paradigmatic example of a recursive definition of this kind is the non-terminating expression
let rec f = f
in
    f ;;
that (is not legal in OCaml and) has principal pair
<{}; 'a>
The prototype does not allow to experiment with system |-21.

1.1 Non-simple recursive definitions that are |-22-typable

In this section we present an example of non-simple recursive function. Being non-simple, this function cannot be typed by the Milner/Microft system [Mycroft, 1984], by Jim's rules for recursive definitions [Jim, 1996], or by rule (Rec2) of [ Damiani, 2003 ].
  • The function "f" in Example 6.1 of [ Damiani, 2007 ]

    Typechecking with system |-22 the following expression, which defines the non-simple recursive function "f"

    let rec f g l = 
        match l with
          []     -> []
        | h :: t -> ((g h 5),(g y true)) :: (f g t) 
    in
        f ;;
    
    yields the principal pair:
    <{y: 'a}; ('a -> bool -> 'd ^ 'b -> int -> 'c) -> 'b list -> ('c * 'd) list>
    
    Also the following program, where the function "f" is defined at top-level and then applied to different arguments, can be successfully typechecked.
    let rec f g l = 
        match l with
          []     -> []
        | h :: t -> ((g h 5),(g y true)) :: (f g t) ;; 
    
    let test1 = f (fun x -> fun y -> x) [()];;
    
    let test2 = f (fun x -> fun y -> y) [()];;
    
    let test2 = f (fun x -> fun y -> (x,y)) [()];;
    
    ();;
    

1.2 ML-typable recursive definitions that get a more precise typing in |-22

In this section we present an example of simple recursive function that gets a more precise typing in |-22. The more precise typing allows to type uses of the function that cannot be typed by the Milner/Microft system [Mycroft, 1984], by Jim's rules for recursive definitions [Jim, 1996], or by rule (Rec2) of [ Damiani, 2003 ].
  • The function "mapPair"

    Typechecking with system |-22 the following expression, which defines the recursive function "mapPair",

    let rec mapPair f l1 l2 = 
        match l1 with
          []       -> []
        | h1 :: t1 -> match l2 with
             	    []       -> []
    		  | h2 :: t2 -> ((f h1),(f h2)) :: (mapPair f t1 t2)  
    in
        mapPair ;;
    
    yields the principal pair:
    <{}; ('c -> 'd ^ 'a -> 'b) -> 'a list -> 'c list -> ('b * 'd) list>
    
    The function "mapPair" is simple (to check this, typecheck it with system |-02 or with OCaml). However, the more precise typing inferred by |-22 allows to type uses of "mapPair" (like in the expression "mapPair toList [5] [true]" in the program below) that require a non-simple type.

    The following (not ML-typable) program can be successfully typechecked with system |-22

    let toList x = [x] ;;
    
    let rec mapPair f l1 l2 = 
        match l1 with
          []       -> []
        | h1 :: t1 -> match l2 with
             	    []       -> []
    		  | h2 :: t2 -> ((f h1),(f h2)) :: (mapPair f t1 t2) ;; 
    
    mapPair toList [5] [true];;
    

1.3 Milner/Microft typable recursive definitions that are |-2>2-typable

In this section we show that system |-22 is able to type well-known examples of recursive definitions that can be typed by the Milner/Microft system [Mycroft, 1984] but not by Jim's rules for recursive definitions [Jim, 1996] or by rule (Rec2) of [ Damiani, 2003 ].
  • The function "collect" on the non-uniform datatype 'a tree

    This example is taken from [Jim, 1996], it originally comes from the ML mailing list, and has arisen in practice.

    Typecheching with system |-22 the following program

    type 'a tree = EMPTY | NODE of 'a * ('a tree) tree ;;
    
    let rec append l1 l2 = match l1 with
    			 []     -> l2
              	       | h :: t -> h :: (append t l2) ;;
    
    let rec flatmap f l = match l with
    			[]     -> []
    		      | h :: t -> append (f h) (flatmap f t) ;;
    
    let rec collect t = match t with
    		      EMPTY      -> []
    		    | NODE(n,t1) -> n :: (flatmap collect (collect t1)) ;;
    
    collect (NODE(2,NODE(NODE(1,EMPTY),EMPTY)));;
    
    yields the following principal pairs for the top-level functions "append", "flatmap", and "connect":
    append	: <{}; 'a list -> 'a list -> 'a list>
    flatmap	: <{}; ('a -> 'b list) -> 'a list -> 'b list>
    collect	: <{}; 'a tree -> 'a list>
    
  • The function "length" on the non-uniform datatype 'a seq

    This example is taken from from [Okasaki, 1998]:

    Typecheching with system |-22 the following program

    type 'a seq = NIL | CONS of 'a * ('a * 'a) seq ;;
    
    let rec length s = match s with
          		   NIL        -> 0
    		 | CONS(x,s1) -> 1 + 2 * (length s1) ;;
    () ;;
    
    yields the following principal pair for the top-level function "length":
    length : <{}; 'a seq -> int>
    

1.4 Milner/Microft typable recursive definitions that are |-23-typable (and not |-22-typable)

  • The function "f"

    The following example has been proposed in [ Cousot, 1997 ] (see also [ Gori, Levi, 2002 ; Gori, Levi, 2003 ] ). It cannot be typed by system |-22 and, for all k >= 3, it can be typed by system |-2k.

    let rec f = function f1 -> function g -> function n -> function x ->
    	       if (n = 0) then (g x)
    	       else
    	       (f f1 (function x -> (function h -> g (h x))) (n - 1) x f1) ;;
    
    ();;
    
    The above term cannot be typed by ML.

1.5 ML-typable (and, therefore, |-21,ML-typable) recursive definitions that are not |-2k-typable, for all k >= 1.

  • The function "f" in Example 7.1 of [ Damiani, 2007 ]

    The following function "f"

    let rec f = fun g -> fun y -> if true then y else (g (f g y)) 
    in  
        f ;;
    
    is |-21,ML-typable (indeed, it is ML-typable) with principal pair:
    <{}; ('a -> 'a ) -> 'a  -> 'a>
    
    To see that, for all k >= 1, the function "f" is not |-2k-typable see what happens when trying to type it with systems |-21, |-22, |-23, ...

BIBLIOGRAPHY



[Back]

Comments to: damiani[at]di[dot]unito[dot]it