Run Clear log Clear editor

SubML (prototype) language

The SubML language implements the type system presented in the (draft) paper Practical Subtyping for Curry-style languages (to appear in the TOPLAS journal). 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).

Tutorial and online interpreter

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.

List of examples