### Set-Theoretic Types for Polymorphic Variants (bidirectional typing)

The following is an interactive interpreter implementing the system described in the article Set-Theoretic Types for Polymorphic Variants appeared in the proceedings of ICFP 2016, the 21st ACM SIGPLAN International Conference on Functional Programming.

WARNING! The prototype is very experimental: 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)

e : {t1; ...; tn}                          (type annotation:
if e has type   ti for all i
then this expression is given type
t1 & ... & tn)

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)
not                             (Boolean negation)
and                             (Boolean conjunction)
or                              (Boolean disjunction)
succ                            (successor function)
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 x : {t; ...; t} = e    ⟿    let x = (e : {t; ...; t})
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 *]

```