The SubML language implements the type system presented in the paper
Practical Subtyping for Curry-style languages
(TOPLAS 2019). In this paper,
Rodolphe Lepigre and
Christophe Raffalli
argue that it is possible to build a practical type systems based on
subtyping for extensions of
System F. The
SubML language provides polymorphic types and subtyping, but also
existential types, inductive types and coinductive types. Usual
programming in the style of ML is also supported using sum types and
product types corresponding to polymorphic variants and records. The
system can be used on this webpage as explained bellow, or downloaded
and and compiled from its OCaml
source code
(see also the OCamlDoc documentation).
The SubML language can be tried on this webpage, using the editor on the lefthand side. The syntax of the language is exhibited in the tutorial that is loaded in the editor by default. Other examples marked by yellow links can be loaded into the editor at any time. The standard library of SubML includes unary natural numbers, lists and sets implemented using binary search trees. A library for append lists with constant time append operation (as a supertype of lists) is also provided.
The syntax of the language contains several unicode characters. They can be inserted in the editor on the lefthand side of the page using the TeX-like macros listed bellow (followed by a space).
| → | -> | → | \to | × | \times |
| λ | \lambda | ∀ | \forall | ∃ | \exists |
| μ | \mu | ν | \nu | ⊆ | \sub |
| ∞ | \infty | α | \alpha | β | \beta |
| γ | \gamma | δ | \delta | ε | \epsilon |
| ∈ | \in | ∉ | \notin | … | \dots |
Note that ?val is used to mark a value declaration as potentially correct. A message is printed in the case where it is accepted, and nothing happens if it fails to type-check. On the contrary, !val is used to mark a value declaration as incorrect. It must be rejected by the type-checker, and the program fails otherwise.