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)


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)


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

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


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 *]