DIPARTIMENTO   DI   INFORMATICA
Università di Torino

Rank 2 Intersection Types for (a subset of) Caml

Examples

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

  1. Examples involving free variables
  2. Examples involving let-expressions
  3. Examples involving recursive definitions
  4. 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