
DIPARTIMENTO DI INFORMATICA Università di Torino

Research on "Formal Methods in Computing"

Rank 2 Intersection Types for (a subset of) Caml

Examples

The following programs can be typed by our system but not by (O')Caml.

Examples involving free variables
Examples involving let-expressions
Examples involving recursive definitions
Examples involving conditional expressions

1. Examples involving free variables

Autoapplication
Typechecking the open expression
```
x x;;
```
yelds the principal pair
```
<{x: ('a ^ 'a -> 'b)}; 'b>
```

Another example

Typechecking the open program

let exampleA = (f 3, f true) ;;

let exampleB = ((g 3)+1, not (g true)) ;;

let id x = x ;;

let apply h y = h y;;

let exampleC = (fun k -> apply k z) ;;

let exampleD = exampleC id ;;

();;

yelds the following principal pairs for the top-level functions "exampleA", "exampleB", "id", "apply", "exampleC", and "exampleD":

exampleA : <{f: (bool -> 'b ^ int -> 'a)}; ('a * 'b)>
exampleB : <{g: (bool -> bool ^ int -> int)}; (int * bool)>
id	 : <{}; 'a -> 'a>
apply	 : <{}; ('a -> 'b) -> 'a -> 'b>
exampleC : <{z: 'a}; ('a -> 'b) -> 'b>
exampleD : <{z: 'a}; 'a>

2. Examples involving let-expression

The following examples involve top-level let-definitions. They can be turned into examples involving only local definitions (let-in expressions) by replacing the ";;" following each let-definition by the keyword "in".

The functions "twice" and "k"
This example has been proposed in [Coppo, 1980].
Typechecking the program
```
let twice f x = f (f x) ;;
let k u v = u ;;
twice k ;;
```
yelds the following principal pairs for the top-level functions "twice" and "k"
```
twice : <{}; ('c -> 'a ^ 'a -> 'b) -> 'c -> 'b>
k     : <{}; 'a -> 'b -> 'a>
```
and the folowing principal pair for the expression "twice k":
```
<{}; 'a -> 'b -> 'c -> 'a>
```
The functions "twice" and "tolist"
Typechecking the program
```
let twice f x = f (f x) ;;
let tolist x = [x] ;;
twice tolist ;;
```
yelds the following principal pairs for the top-level functions "twice" and "tolist"
```
twice  : <{}; ('c -> 'a ^ 'a -> 'b) -> 'c -> 'b>
tolist : <{}; 'a -> 'a list>
```
and the folowing principal pair for the expression "twice tolist":
```
<{}; 'a -> 'a list list>
```
The functions "auto" and "twice"
Typechecking the program
```
let auto x = x x ;;
let twice f x = f (f x) ;;
auto twice ;;
```
yelds the following principal pairs for the top-level functions "auto" and "twice"
```
auto  : <{}; ('a ^ 'a -> 'b) -> 'b>
twice : <{}; ('c -> 'a ^ 'a -> 'b) -> 'c -> 'b>
```
and the folowing principal pair for the expression "auto twice":
```
<{}; ('a -> 'a) -> 'a -> 'a>
```
The function "selfApply2"
This example is a reformulation, suggested by Joe Wells, of a program that Pawel Urzyczyn [Urzyczyn, 1997] proved to be not typable in F_omega (indeed Urzyczyn proved the untypability of the lambda-term corresponding to the program:
```
(
 fun x ->
          z (x (fun f u -> f u))
            (x (fun v g -> g v))
)
(fun y -> y y y)
;;
```
that cannot be typed in our system, since it requires the use of rank 3 intersection, but can be typed by using the algorithm given in [Kfoury and Wells, 1999]).
Typechecking the following program, which safely evaluates to "(false,true)",
```
let selfApply2 z = (z z) z;;
let apply f x = f x;; 
let reverseApply y g = g y;;
let id w = w;;
(selfApply2 apply not true,
 selfApply2 reverseApply id false not);;
```
yields the following principal pairs for the top-level functions "selfApply2", "apply", "reverseApply", and "id"
```
selfApply2   : <{}; ('b ^ 'a ^ 'a -> 'b -> 'c) -> 'c>
apply        : <{}; ('a -> 'b) -> 'a -> 'b>
reverseApply : <{}; 'a -> ('a -> 'b) -> 'b>
id           : <{}; 'a -> 'a>
```
and the following principal pair for the expression "(selfApply2 apply not true, selfApply2 reverseApply id false not)":
```
<{}; (bool * bool)>
```

An example involving a user-defined datatype

Typechecking the program

type 'a bintree = EMPTY | NODE of 'a * ('a bintree) * ('a bintree);;
let rec append l1 l2 = match l1 with 
                         []     -> l2
                       | h :: t -> h :: (append t l2) ;; 
let rec map f l = match l with
                    []     -> []
                  | h :: t -> (f h) :: (map f t) ;;
let rec collect t = match t with
                      EMPTY         -> []
                    | NODE(n,t1,t2) -> append (collect t1) (n :: (collect t2)) ;;
let mappair f p = match p with
                  (e1,e2) -> (f e1, f e2) ;;
let mappaircollect p = mappair collect p ;;
mappaircollect (NODE(1,NODE(2,EMPTY,EMPTY),NODE(3,EMPTY,EMPTY)),
                NODE(true,EMPTY,EMPTY)) ;;

yields the following principal pairs for the top-level functions "append", "map", "collect", "mappair", and "mappaircollect"

append         : <{}; 'a list -> 'a list -> 'a list>
map            : <{}; ('a -> 'b) -> 'a list -> 'b list>
collect        : <{}; 'a bintree -> 'a list>
mappair	       : <{}; ('c -> 'd ^ 'a -> 'b) -> ('a * 'c) -> ('b * 'd)>
mappaircollect : <{}; ('a bintree * 'b bintree) -> ('a list * 'b list)>

and the following principal pair for the expression "mappaircollect (NODE(1,NODE(2,EMPTY,EMPTY),NODE(3,EMPTY,EMPTY)), NODE(true,EMPTY,EMPTY))":

<{}; (int list * bool list)>

An example involving a let-expression containing free identifiers
Typechecking the expression
```
let x = y in x x ;;
```
yields the principal pair
```
<{y: ('a ^ 'a -> 'b)}; 'b>
```
Another example involving a let-expression
Typechecking the expression
```
fun y -> let x = y in x x ;;
```
yields the principal pair
```
<{}; ('a ^ 'a -> 'b) -> 'b>
```

4. Examples involving recursive definitions

A first example
Typechecking the program
```
let rec f x = f 0 + f false ;; 
();;
```
yields the following principal pair for the top-level function "f":
```
f : <{}; 'a -> int>
```
A second example
Typechecking the program
```
let rec f x = x x ;; 
();;
```
yields the following principal pair for the top-level function "f":
```
f : <{}; ('a ^ 'a -> 'b) -> 'b>
```
A third example
This example is taken from [Jim, 1996].
Typechecking the program
```
let rec f x = (fun y z -> z) (f f) x ;;
();;
```
yields the following principal pair for the top-level function "f":
```
f : <{}; 'a -> 'a>
```

A fourth example

This example is described in Section 1.2 of [ Damiani, 2003 ].

Typechecking the program

let rec kFibonacci dummy n = if n < 0  
			    then 1
			    else (kFibonacci 0 (z-1)) + (kFibonacci false (z-2)) 
			    ;; 
();;

yields the following principal pair for the top-level function "kFibonacci":

kFibonacci : <{z: int -> int}; 'a -> int -> int>

4. Examples involving conditional expressions

Example 1

Typechecking the program

let f1 g = g (1,2) ;;
let f2 g = g (3,true) ;;

let testC = (fun b -> if b then f1 else f2) ;;

let testC1 = testC y ;;

let testC2 = testC1 fst;;

let testCi = (fun b x -> if b then f1 else x) ;;

let testCi1 = testCi x ;;

let testCi2 = testCi1 f2 ;;

let testCi3 = testCi2 fst;;

();;

yields the following principal pairs for the top-level functions "f1", "f2", "testC", "testC1", "testC2", "testCi", "testCi1", "testCi2", and "testCi3":

f1 : <{}; ((int * int) -> 'a) -> 'a>
f2 : <{}; ((int * bool) -> 'a) -> 'a>
testC   : <{}; bool -> ((int * bool) -> 'a ^ (int * int) -> 'a) -> 'a>
testC1  : <{y: bool}; ((int * bool) -> 'a ^ (int * int) -> 'a) -> 'a>
testC2  : <{y: bool}; int>
testCi  : <{}; bool -> ('a -> 'b) -> ((int * int) -> 'b ^ 'a) -> 'b>
testCi1	: <{x: bool}; ('a -> 'b) -> ((int * int) -> 'b ^ 'a) -> 'b>
testCi2	: <{x: bool}; ((int * int) -> 'a ^ (int * bool) -> 'a) -> 'a>
testCi3	: <{x: bool}; int>

Example 2

Typechecking the program

let twice f x = f (f x) ;;

let tolist e = [e] ;;

let test l = match l with
              []    -> twice 
            | _::t  -> fun x y -> t ;;


let test1 =  test [] ;;

let test2 =  test1 tolist ;;

let test3 =  test2 5 ;;

();;

yields the following principal pairs for the top-level functions "twice", "tolist", "test", "test1", "test2", and "test3":

twice  : <{}; ('c -> 'a ^ 'a -> 'b) -> 'c -> 'b>
tolist : <{}; 'a -> 'a list>
test   : <{}; 'a list -> ('c -> 'b ^ 'b -> 'a list) -> 'c -> 'a list>
test1  : <{}; ('c -> 'a ^ 'a -> 'b list) -> 'c -> 'b list>
test2  : <{}; 'a -> 'a list list>
test3  : <{}; int list list>

BIBLIOGRAPHY

[Coppo, 1980] An extended polymorphic type system. In: Mathematical Foundations of Computer Science, LNCS 88, Springer, pp. 194-204.
[Jim, 1996] What are principal typings and what are good for? In: Proceedings of ACM SIGPLAN/SIGTACT Symposium on Principles of Programming Languages 1996 (POPL'96), pp. 42-53.
[Kfoury and Wells, 1999] Principality and Decidable Type Inference for Finite-Rank Intersection Types. In: Proceedings of ACM SIGPLAN/SIGTACT Symposium on Principles of Programming Languages 1999 (POPL'99), pp. 161-174.
[Urzyczyn, 1997] Pawel Urzyczyn. Type reconstruction in F_omega. Mathematical Structures in Computer Science, 7(4):329-358, 1997.

[Back]


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