Polymorphic Functions with Set-Theoretic Types. Part 2: Local Type Inference and Type Reconstruction We study the definition of higher-order polymorphic functions in a type system with recursive types and set-theoretic type connectives (unions, intersections, and negations). In particular, we present a local type inference system that allows the programmer to omit explicit instantiation annotations for function applications, and a type reconstruction system that allows the programmer to omit explicit type annotations for function definitions.
- CDuce development Website
- Virtual Box image containing the latest version of the cduce compiler. User : test/test . Root : root/test . The README file in the home directory provides instructions on how to use the cduce compiler/toplevel.
Below a snippet of the code presented in the paper that can be cut&pasted in the toplevel for testing the prototype:
(*---------------------------------------*) (* Note that "map" is a keyword in Cduce *) (*---------------------------------------*) let mmap (f : 'a -> 'b) (l : [ 'a* ] ) : [ 'b* ] = match l with [] -> [] | (e, ll) -> (f e, mmap f ll) ;; let even (Int -> Bool; 'c\Int -> 'c\Int) | x & Int -> (x mod 2) = 0 | x -> x ;; let map_even = mmap even ;; let pretty (x : Int) : String = string_of x ;; let map_pretty = mmap pretty ;; let g ( (Int -> Int) -> Int -> Int; (Bool -> Bool) -> Bool -> Bool) x -> x ;; let id ('a -> 'a) x -> x;; let gid = g id;; let id2g = id (id g);; let churchtrue (x : 'a) (y : 'b) : 'a = x in churchtrue 42;; let max (x : 'a) (y : 'a) : 'a = if x >> y then x else y;; max 42;; let max (x : 'a) (y : 'b) : 'a|'b = if x >> y then x else y in max 42 ;; type RBtree('a) = Btree('a) | Rtree('a) type Btree('a) = <blk elem='a>[ RBtree('a) RBtree('a) ] | [] type Rtree('a) = <red elem='a>[ Btree('a) Btree('a) ] type Unbal('a) = <blk elem='a>( [ Wrong('a) RBtree('a) ] | [ RBtree('a) Wrong('a) ]) type Wrong('a) = <red elem='a>( [ Rtree('a) Btree('a) ] | [ Btree('a) Rtree('a) ]) ;; let balance ( Unbal('a) ->Rtree('a) ; ('b \ Unbal('a)) ->('b \ Unbal('a)) ) | <blk (z)>[ <red (y)>[ <red (x)>[ a b ] c ] d ] | <blk (z)>[ <red (x)>[ a <red (y)>[ b c ] ] d ] | <blk (x)>[ a <red (z)>[ <red (y)>[ b c ] d ] ] | <blk (x)>[ a <red (y)>[ b <red (z)>[ c d ] ] ] -> <red (y)>[ <blk (x)>[ a b ] <blk (z)>[ c d ] ] | x -> x ;; let r = balance <blk elem=1>[ <red elem=3>[ <red elem=2>[ [] [] ] [] ] [] ];;