This page presents my prototype typechecker for the MLF 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.
talso defines an elimination principle
t_elimwhich can be used to perform case analysis on values.
The prototype will be updated regularly, some of these limitations should be resolved soon.
Syntax differences with OCaml:
let x = 1 in x + 2is valid (it is an expression) but
let x = 1is not, and must be written
val x = 1.
1, 2is 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.
Cons 1 Nilis valid and represents the list with a single element
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.
('a = 'b. 'b -> 'b) ('c > 'd. 'd -> 'd) 'a -> 'cis 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 -> 'dis written
'a. ('b > 'c. 'c -> 'c). ('a -> ('e. 'e -> 'b))Indeed, the bound of
bis not inlined in the bound of
bis bound above the level of
#inline -> 0. By default, in uples, flexible bounds are inlined; this can be changed by the directive
#inline (.) *, where
=for inlining rigid bounds,
>for inlining flexible bounds, and
-for disabling inlining. Inlining for a type constructor
acan be changed by the directive
#inline c l, where
lis a list of length
-. By default no inlining is done.
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 MLF are a bit unclear. Do not hesitate to report any bug or strange behaviour.