Polymorphic variants with set-theoretic types (original) (raw)

Set-Theoretic Types for Polymorphic Variants

The following is an interactive interpreter implementing the system described in the article Set-Theoretic Types for Polymorphic Variants.

WARNING! The prototype is still buggy: there are a few bugs in the constraint solving algorithm used in CDuce (which we use via an API)which can make constraint solving loop. Also, the types are not cleansed before printing, which can make them somewhat unreadable sometimes. This is still work in progress and is made available only for demonstration purposes.

:: SETVARIANTS prototype ::

(X⟿Y indicates that X is syntactic sugar for Y)

                        PATTERNS

p ::= _tag_ (variant w/o argument) tag p (variant with argument) p & p (intersection) p as x (capture) [ ⟿ p & x] p | p (union) (p, p) (pair) [p; ...; p] (list) p :: p (consed list) [] (empty list) () (unit) fun (captures any function) _ (wildcard) x (capture variable) b (boolean constant) n (numeric constant)

                          EXPRESSIONS

e ::= \ p ... p . e (functions) fun p ... p -> e

    recfun _f_ _p_ ... _p_ -> _e_                      (recursive functions)

    function _p_ -> _e_ | ... | _p_ -> _e_             (functions by cases)
    function | _p_ -> _e_ | ... | _p_ -> _e_

    recfunction _f_ _p_ -> _e_ | ... | _p_ -> _e_        (recursive functions by cases)
    recfunction _f_ | _p_ -> _e_ | ... | _p_ -> _e_

    match _e_ with _p_ -> _e_ | ... | _p_ -> _e_         (match)
    match _e_ with | _p_ -> _e_ | ... | _p_ -> _e_

    let _p_ = _e_ in _e_                             (let)
    let _f_ _p_ ... _p_ = _e_ in _e_                     (let function)
    let rec _f_ _p_ ... _p_ = _e_ in _e_                 (let recursive function)

    if _e_ then _e_ else _e_                         (if then else)
    _e_ _e_                                        (application)
    `_tag_                                       (variant w/o argument)
    `_tag_ _e_                                     (variant with argument)
    (_e_, _e_)                                     (pair)
    []                                         (empty list)  [ ⟿ `Nil]
    _e_ :: _e_                                     (consed list) [ ⟿ `Cons(_e_,_e_)]
    [_e_;...; _e_]                                 (list)        [ ⟿ `Cons(_e_,...,`Cons(_e_,`Nil))]
    ()                                         (unit)
    _b_                                          (boolean constant)
    _n_                                          (numeric constant)
    _x_                                          (variable)
    _p_                                          (primitive function)

                    PRIMITIVE FUNCTIONS (prefixed)

p ::= eq (equality) succ (successor function) add (integer sum) sub (integer subtraction) mul (integer multiplication) div (integer division, fails if dividing by 0) safe_div ("safe" integer division: 2nd argument must not be 0)

                    TOP LEVEL DEFINITIONS

    _e_
    let _x_ = _e_
    let _f_ _p_ ... _p_ = _e_        ⟿    let _f_ = fun _p_ ... _p_ -> _e_
    let rec _f_ _p_ ... _p_ = _e_    ⟿    let _f_ = recfun _f_ _p_ ... _p_ -> _e_
    let rec _f_ = function ... ⟿    let _f_ = recfunction _f_ ...


                          TYPES

t ::= 'a (type variables) Bool (booleans) Int (arbitrary precision integers) Caml_Int (integers) b (singleton [booleans]) n (singleton [integers]) unit (unit) Nil (empty list) `Cons(t,t) (consed lists) n--n (intervals of integers)

   _X_                                          (type recursion variable)
   _t_ WHERE _X_ = _t_                              (recursive type)

   _t_->_t_                                       (functions)
   (_t_,_t_)                                      (products)

   _t_|_t_                                        (union)
   _t_&_t_                                        (intersection)
   _t_\_t_                                        (difference)

   Empty                                      (empty type)
   Any                                        (top type)
   Arrow                                      (all functions type) [⟿ Empty->Any]


   [* _NOTE: an_ 'a list _is encoded as_  X where X = `Cons('a,X)|`Nil *]