This page presents my prototype typechecker for the ML^F language. The prototype currently features the core ML constructs presented in this paper, as well as the ability to define new inductive types and (monomorphic, ML-style) recursion. The syntax is inspired from that of OCaml, except for the richer grammar of types and a few differences detailed below.

The prototype can be downloaded here. The tarball also includes an IDE in which constraints can be solved interactively, one step at a time.

Current limitations:

• No mutually recursive inductive types.
• No mutually recursive values.
• No pattern-matching. However, defining an inductive type t also defines an elimination principle t_elim which can be used to perform case analysis on values.
• Recursive functions are currently typed using a fixpoint operator, resulting in poor type error messages.

The prototype will be updated regularly, some of these limitations should be resolved soon.

Syntax differences with OCaml:

• Toplevel values are defined using the keyword val instead of let, e.g. let x = 1 in x + 2 is valid (it is an expression) but let x = 1 is not, and must be written val x = 1.
• The boolean constructors are capitalized, for uniformity reasons: True and False.
• Uples must be parenthesized, i.e. 1, 2 is not a valid value. Note that this means that (fun x -> x, 1) is parsed as ((fun x -> x), 1)) and not as (fun x -> (x, 1)) as in OCaml.
• Constructors are curryfied, e.g. Cons 1 Nil is valid and represents the list with a single element 1, while Cons (1, Nil) is also valid but represents the partial OCaml application (fun l -> (1, []) :: l), which is a function returning a list of uples of type (int * ('a list)) list.

Experimental features

• ML^F types are written using an alternative syntax that inlines bounds, according to some user-defined syntactic conventions. For example, for the arrow constructor, we inline the domain if it is rigidly bound, and the codomain if it is only flexibly bound. In practice, this makes for much more readable types, as the resulting types are very often System F ones.
  Of course, such inlining is not always possible, as we must keep track of sharing and the place where the polymorphism is introduced. In consequence, we only inline bounds occurring once, and only when they are used right where they are introduced.
  
  Examples:
  • ('a = 'b. 'b -> 'b) ('c > 'd. 'd -> 'd) 'a -> 'c is written ('b. 'b -> 'b) -> ('d. 'd -> 'd)
  • 'a. ('c > 'b. 'b -> 'b). 'a -> 'c (which is the type of the second projection) is writte 'a. 'a -> ('b. 'b -> 'b)
  • 'a. ('b > 'c. 'c -> 'c). ('d > 'e. 'e -> 'b). 'a -> 'd is written 'a. ('b > 'c. 'c -> 'c). ('a -> ('e. 'e -> 'b)) Indeed, the bound of b is not inlined in the bound of d, as b is bound above the level of d.
  
  Inlining for the arrow constructor can be deactivated using the toplevel directive #inline -> 0. By default, in uples, flexible bounds are inlined; this can be changed by the directive #inline (.) *, where * is = for inlining rigid bounds, > for inlining flexible bounds, and - for disabling inlining. Inlining for a type constructor c of arity a can be changed by the directive #inline c l, where l is a list of length a of >, = or -. By default no inlining is done.
• Support for type abbreviations, including polymorphic ones (e.g. type id = 'a. 'a -> 'a) has been added. However, some of the interactions between parameterized abbreviations (e.g. type 'a t = 'a -> 'a list) and the polymorphic types of ML^F are a bit unclear. Do not hesitate to report any bug or strange behaviour.