Rank2 Intersection
and Polymorphic Recursion for (a subset of) Caml
EXAMPLES
Index
1.0
About recursive definitions
that are _{2}^{1}typable
1.1
Nonsimple
recursive definitions
that are _{2}^{2}typable
1.2
MLtypable
recursive definitions
that get a more precise typing in _{2}^{2}
1.3
Milner/Microft typable
recursive definitions
that are _{2}^{2}typable
1.4
Milner/Microft typable
recursive definitions
that are
_{2}^{3}typable
(and not _{2}^{2} typable)
1.5
MLtypable
(and, therefore,
_{2}^{1,ML}typable)
recursive definitions that are
not
_{2}^{k}typable,
for all k >= 1.
1.0
About recursive definitions
that are _{2}^{1}typable
System
_{2}^{1}
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
nonterminating
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
_{2}^{1}.
1.1
Nonsimple
recursive definitions
that are _{2}^{2}typable
In this section we present an example of
nonsimple
recursive function.
Being
nonsimple,
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 _{2}^{2}
the following expression, which defines the
nonsimple 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 toplevel
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
MLtypable
recursive definitions
that get a more precise typing in _{2}^{2}
In this section we present an example of
simple
recursive function
that
gets a more precise typing in
_{2}^{2}.
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 _{2}^{2}
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
_{0}^{2}
or with OCaml).
However, the more precise typing inferred by
_{2}^{2}
allows to type uses of "mapPair" (like in
the expression
"mapPair toList [5] [true]" in the program below)
that require a
nonsimple type.
The following (not MLtypable) program
can be successfully typechecked
with system _{2}^{2}
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 _{2}^{2}
is able to type wellknown 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 nonuniform 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 _{2}^{2}
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
toplevel
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 nonuniform datatype 'a seq
This example is taken from
from [Okasaki, 1998]:
Typecheching
with system _{2}^{2}
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
toplevel
function "length":
length : <{}; 'a seq > int>
1.4
Milner/Microft typable
recursive definitions
that are _{2}^{3}typable
(and not _{2}^{2}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
_{2}^{2}
and, for all k >= 3, it can
be typed by
system
_{2}^{k}.
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
MLtypable
(and, therefore,
_{2}^{1,ML}typable)
recursive definitions that are
not
_{2}^{k}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 _{2}^{1,ML}typable
(indeed, it is MLtypable)
with principal pair:
<{}; ('a > 'a ) > 'a > 'a>
To see that, for all k >= 1, the function "f" is not
_{2}^{k}typable
see what happens when trying to type it with
systems _{2}^{1},
_{2}^{2},
_{2}^{3}, ...
BIBLIOGRAPHY

[Cousot, 1997]
Types as Abstract Interpretations
In:
Proceedings of ACM SIGPLAN/SIGTACT Symposium on
Principles of Programming Languages 1997 (POPL'97),
pp. 316331.

[Damiani, 2003]
Rank 2 intersection types for local definitions and conditional expressions.
ACM Transactions On Programming Languages and Systems, 25(4):401451, 2003.

[Damiani, 2005]
Rank 2 Intersection Types and Polymorphic Recursion.
In:
Proceedings of International Symposium on
Typed Lambda Calculi and Applications,
LNCS 3461, Springer, 2005.

[Damiani, 2007]
Rank 2 Intersection for Recursive Definitions.
Fundamenta Informaticae, 77, 2007.

[Gori, Levi, 2002]
An experiment in type inference and verification by abstract interpretation.
In:
Proceedings of VMCAI'02,
LNCS 2294, pp. 225339. Springer, 2002.

[Gori, Levi, 2003]
Properties of a type abstract interpreter.
In:
Proceedings of VMCAI'03,
LNCS 2575, pp. 132145. Springer, 2003.

[Hallet and Kfoury, 2004]).
Programming examples needed polymorphic recursion.
In
ITRS'04
(workshop affiliated to LICS'04), ENTCS. Elsevier. To appear.

[Jim, 1995]
Rank 2 type systems and recursive definitions.
Technical Report MITT/LCS/TM531, LCS, Massachusetts Institute of
Technology, 1995.

[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. 4253.

[Mycroft, 1984]
Polymorphic Type Schemes and Recursive Definitions.
In:
Proceedings of International Symposium on
Programming 1984, LNCS 167, pp. 217228. Springer, 1984.

[Okasaki, 1998]
Purely Functional Data Structures. Cambridge University Press, 1988.
