Documentation for the Polymorphic Set-Theoretic type-system prototype

Basic usage
Syntax of the language
Caveat

Basic usage

The prototype consists of an online text editor (based on Monaco Editor).

The basic Monaco keyboard shortcuts (e.g. Ctrl-/ for single line comment) are available. The command palette can be invoked with the context menu or F1
F2 presents a menu with a choice of predefined examples.
[Ctrl-Enter] types the buffer

Computed types are printed as lenses (above each definition). In case of error, the error message is printed instead (see the caveat section for the printing format).

Syntax

Definitions

A program is a sequence of toplevel statements:
prog ::= stmt* stmt ::= type tid tvar* = t [and ...] | atoms id+ | let gid : t = e | let [rec] gid param* = e | let [rec] (gid : t) param* = e param ::= pat [: t, ...,t]

A statement can be either

a type definition, composed of a type name, a (possibly empty) list of type variables, and a type expression. Several mutually recursive type definitions can be defined together using the and keyword.
atom definitions, introduced by the atoms keyword and followed by a sequence of identifier. Each identifier defines a constant of that name, and a corresponding singleton type starting with an uppercase letter. So atoms a foo hello_ defines three constants and three singleton types A, Foo and Hello_
a toplevel value definition which follows, roughly, OCaml's syntactic convention. Function parameters can be either simple identifiers or patterns and optionally feature a type constraint.

Identifiers

Identifiers come in several flavours :


    gid ::= id | ( op )

    id ::= [a-z_][a-zA-Z0-9_']*

    tid ::= [A-Z][a-zA-Z0-9_']*

    tvar ::= '[a-z_][a-zA-Z0-9_]*

value identifiers can be either variable names (starting with a lowercase letter) or prefix or infix operator symbols in parenthesis.
type identifiers starts with an uppercase letter
type variables start with a single quote ' character. If the second character is _ then the variable is monomorphic and it's considered a hint for the type reconstruction.

Type expressions


    t ::= simple_type
        | t -> t
        | t , t
        | [ tregex ]
        | { id =[?] t,..., id =[?] t [..]}
        | t | t
        | t & t
        | t \\ t
        | ~ t
        | t where tid tvar* = t [and ...]

    simple_type ::= b
                | tid [t ... t]
                | tvar
                | (t)
    b ::= ()
        | lit
        | int--int | (--int) | int--) | (--)
        | Any | Empty | True | False | Bool | Int | Char | Unit | String | List | Nil

Types are the usual set-theoretic types with product and arrow and record constructors and union, intersection, difference and negation operators. A sequence type constructor is provided as well. The content of a sequence type can be a regular expression over types, using the usual operators (*, + and ?). For instance, the type [ 'a* (Bool|Int)? ] is equivalent to the type definition


     type t 'a = ('a, t) | s
     and  s    = Nil | (Bool | Int, Nil)

Record types are given by the list of their fields, that is labels associated with a type. A label may be absent (denoted by =?). Open record types end their field list with ... Polymorphic types can be instantiated by giving a list of type parameters. Basic types consists of literals (which denote their own singleton type), augmented with integer interval types, and set of builtin type identifiers.

Expressions


        e ::= lit
            | gid
            | magic
            | (e : t ; ... ; t )
            | (e :> t ; ... ; t )
            | { [e with] id=e,...,id=e}
            | [ e; ... ;e ]
            | e,e
            | fun param ... param -> e
            | let gid = e in e
            | let (pat) = e in e
            | if e [is t] then e else e
            | fst e | snd e
            | match e with [|] pat -> e | ... | pat -> e end

        lit ::= [0-9]+
            | 'char'
            | "char*"
            | float
            | () | unit | false | true | nil

Expressions can be

integer, character (delimited with single quotes), string (delimited with double quotes) or floating point literals
predefined atoms such as false, nil, …
identifiers
a magic constant with type 'a, which can be used to define a variable of any type (without having to give a proper definition)
type annotated expressions, e.g. (x : Bool ; Int) which can be used locally to suggest a type constraint and/or a decomposition to the type reconstruction algorithm
type coerced expressions, e.g. (42 :> Int) which can be used locally to coerce the type of an expression into a (conjunction of) supertype(s)
constructors for products, lists and records
anonymous functions
local let binding (defined using either a variable or a pattern)
a type case. In the tested type, all occurrences of the arrow constructor are of the form Empty->Any. If the tested type is missing, it is synonymous for is True
first and second projections for pairs
a pattern matching construct similar to the one found in the CDuce language. Patterns follow a first match policy.

Patterns


        pat ::= :simple_type
            | id
            | pat,pat | pat|pat | pat&pat
            | (pat)
            | [ pat; ... ;pat ]
            | { id =[?] pat,..., id =[?] pat [..]}
            | id = lit

Patterns are essentially types with capture variables. For instance, the following expression


            match y with
            | :[ Int* ] -> false
            | ( x & :Bool, :Int ) | x = false -> x
            end

First checks whether y is a list of integers, in which case it returns false. Or, it tests whether either y is a pair of a Boolean and an integer, and captures the Boolean in x, or defines x to the constant false, and then returns x.

Caveat

The syntax given above is only a rough approximation. The usual priority of common operators should apply, but in case of doubt, parentheses can be used to disambiguate expressions, types or patterns.
This online prototype uses Js_of_ocaml and is about 8 to 10 times slower than when compiled to native code. Some examples may not terminate in reasonable time or cause a stack overflow due to the relatively shallow recursion stack of web browsers
Types are pretty-printed using CDuce syntax (because the rely on CDuce's internal pretty printer which tries to simplify set theoretic types dans decompile recursive types back to regular expressions). The main difference is that atoms are prefixed with a backtick ` (e.g. `false), the negation operator ~ does not exists (and a type ~t is written Any\t) and recursive types are written in a self-contained expression using the where keyword.