Run Clear log Clear editor

SubML (prototype) language - 08/07/2017

The SubML language implements the type system presented in the paper Practical Subtyping for System F with sized (Co-)Induction. 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.

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. In particular, the prelude is automatically loaded into the interpreter. The standard library of SubML includes unary natural numbers (lib/nat.typ), lists (lib/list.typ) and sets (lib/set.typ) implemented using binary search trees. A library for append lists (lib/applist.typ) with constant time append operation is also provided. The type of append lists is a supertype of the type of lists. Other advanced examples expoiting subtyping are given in the example section below.

Full list of examples