Mentions légales du service

Skip to content

add simple annotations to the term syntax

SCHERER Gabriel requested to merge gscherer/inferno:annotations-upstream into master

Why

@omartino and myself are currently working on two different extensions to Inferno that both require type annotations in ML:

  • "frozen constraints", which typically require type annotations to unfreeze a constraint (directly or through a propagating unification)
  • Carine Morel's work on multi-equations, where annotations are used to associate abbreviated types to program fragments. (With just inference of un-annotated programs, type abbreviations would never be introduced).

These two branches have their own implementation of annotations, one from us and one from Carine. This is a bit frustrating as it adds work/noise to each branch, and it means that they conflict (for example, if Carine's work was merged, we would introduce a conflict in the frozen-constraint branch).

So I propose to upstream support for type annotations (most of the machinery is already there thanks to the presence of type expressions in datatype declarations). We can then rebase both branches on top of the updated upstream, and have versions that can keep growing independently with one less inevitable conflict between the two.

What

Annotations bind flexible variables in the annotated type.

For example,

((fun x -> x) : some a b. a -> b)

is equivalent to OCaml's

((fun x -> x) : _ -> _)

Annotations are also available in pattern, with the same form.

Note: ideally it would be nicer to decouple the introduction of flexible variables from the annotation itself: (e : some a b. ty) can be profitably rewritten some a b in (e : ty). This form is slightly more invasive to implement (we need to add a context of flexible variables to the hastype function). I have an experimental branch on top of !15 (merged) that changes the hastype environment-passing logic (turn it into a record to make it easier to propagate more information during inference), I would like to wait until a similar refactor is available upstream to implement the extension with flexible variable bindings in terms (or patterns). I may propose a MR to do it.

Merge request reports