CDuce: POPL Artifact Evaluation

ℂDuce: POPL Artifact Evaluation

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>[ [] [] ] [] ] [] ];;

Webmaster - Site map

ℂDuce: POPL Artifact Evaluation

CDuce_WS Resources