The prototype consists of an online text editor (based on Monaco Editor).
Computed types are printed as lenses (above each definition). In case of error, the error message is printed instead.
A program is a sequence of toplevel statements:
prog ::= stmt*
stmt ::= type id [(tvar, ..., tvar)] = t [and ...]
| abstract type id [(tvar, ..., tvar)]
| let gid param* = e [and ...]
| let mut id [: t] = e [and ...]
| val [mut] gid : t
param ::= id
| ( pat : t )
A statement can be either
Note that top-level definitions are considered recursive. A definition may refer to an identifier whose type signature is declared later. However, as top-level value definitions are typed sequentially, mutually-recursive definitions that have no explicit type signatures must be defined together using the and keyword.
Identifiers come in several flavours :
gid ::= id | ( op )
id ::= [a-z_][a-zA-Z0-9_']*
cid ::= [A-Z][a-zA-Z0-9_']*
tvar ::= '[a-zA-Z][a-zA-Z0-9_]*
rvar ::= `[a-zA-Z][a-zA-Z0-9_]*
t ::= simple_type
| t -> t
| t ,..., t
| t :: t
| [ tregex ]
| { id : f ;...; id : f row_tail }
| t | t
| t & t
| t \ t
| ~ t
| t where id tvar* = t [and ...]
row_tail ::= ε
| ..
| ;; f
f ::= t [?]
| rvar
| f | f
| f & f
| ~ f
simple_type ::= b
| dyn
| id [(t, ..., t)]
| cid [(t)]
| tvar
| (t)
b ::= ()
| lit | true | false | unit
| (int..int) | (..int) | (int..) | (..)
| any | empty | enum | tuple | tuplen| bool
| int | float | char | string | list | record
Types are the usual set-theoretic types with tuple (product), 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
t where t = 'a::t | s and s = [] | (bool | int)::[]
Parametric 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.
Record types are given by the list of their fields, that is labels associated with a field type f (a Boolean combination of row variables and types, optionally marked with ? to allow the field to be absent). The tail of the field list constrains the unlisted fields:
Some meta type operators (given below) can be used inside type expressions, even though they are not type constructors. To be computed, these type operators must inspect the top-level structure of the type on which they are applied: when defining recursive types, one must be careful not to use these operators on a type whose top-level structure is not fully determined yet.
t ::= ...
| { t with id : f ;...; id : f }
| t.id
| t.cid
e ::= lit
| gid
| cid [(e)]
| (e : t)
| (e :> t) | (e :>> t) | (e :>>> t)
| { [e with] id=e;...;id=e }
| [ e; ... ;e ]
| e ,..., e
| fun param+ -> e
| let gid param* = e in e
| let mut id [: t] = e in e
| let (pat) = e in e
| if e [is t] then e else e
| fst e | snd e | e.id | e.cid | hd e | tl e
| match e with [|] pat -> e | ... | pat -> e end
| e ; e
| id := e
| if e [is t] do e [else e] end
| while e [is t] do e end
| return e | break | continue
lit ::= [0-9]+
| 'char'
| "char*"
| float
| () | false | true | []
Expressions can be
pat ::= :simple_type
| id
| lit
| cid [(pat)]
| 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.
Configuration commands are top-level statements of the following syntax:
#cmd = val
| Command | Values | Default | Description |
|---|---|---|---|
| value_restriction | true | false | true | Enable or disable the value restriction for polymorphic generalization. |
| type_narrowing | "partition" | "direct" | "yes" | "no" | "yes" | Configure the type narrowing strategy used in pattern matching. "partition" uses partition-based narrowing, "direct" uses direct narrowing, "yes" enables both strategies, "no" disables narrowing. |
| allow_implicit_downcast | true | false | true | Enable or disable implicit downcasts of the dynamic part of inferred types when the declared type is more precise. |
| infer_overload | true | false | true | Enable or disable the inference of multiple overloads when typing type-cases. Even when false, the types inferred for functions may still be overloaded: this setting only affects type-cases (not applications). |
| reexplore_failed_domains | true | false | true | Allow or prevent the type inference from re-exploring a function domain that has already been explored, if last attempt failed. Setting this to false will result in a faster but less exhaustive type inference, in particular in the presence of mutable variables. |
| normalization | "no_empty_param" | "no" | "no_empty_param" | Configure the type normalization heuristic applied during inference. "no_empty_param" removes abstract types with empty parameters, "no" disables normalization. |
| subst_normalization | "no_abstract_inter" | "no" | "no_abstract_inter" | Configure the substitution normalization heuristic applied during tallying. "no_abstract_inter" removes abstract type intersections from substitution results, "no" disables substitution normalization. |
Debug commands are top-level statements of the following syntax:
## t
## t op t
## { t op t [; ...] }
op ::= = | <= | >=
Note that type and row variables that are allowed to be substituted (for a tallying or subtyping instance) must start with an underscore (e.g. { '_a <= int | 'b } allows substituting '_a but not 'b, and similarly `_r is substitutable while `r is not).