Skip to content

Use Hindley-Milner type inference

Lustre's type system is verbose enough to work with a very basic type checker. However, a smart type checker with good inference can prove to be really useful to provide smart diagnostics when information is missing. For instance this would make it possible to infer array lengths in calls to iterators that miss them, to provide good fix suggestions. This would also allow "back-typing" an argument or return value whose syntax literally misses a type qualifier. As an example, OCaml's really powerful type-checker is based on an HL type system.

Of course, the goal is not to accept invalid Lustre programs just because we could infer informations from them, but rather to improve the understanding we have of incomplete code to provide more adequate and relevant fix suggestions. If everything is implemented correctly, a Lustre program with missing or invalid syntax will still be rejected when the reference compiler also does.

Key points

  • We'd have to first check if HM type inference is actually compatible with Lustre's type system, but I can hardly think of a reason why it wouldn't be. HM is quite flexible anyway.
  • One of the risks with HM type inference is that it can sometimes give surprising results (I once remember fighting with OCaml, not understanding why a value was typed as a weird function). However, since Lustre doesn't have first-class function and should already have most type hint in place (tightening the assumptions the checker can make), it's rather unlikely to cause us issues.
  • The implementation could be non-trivial (but very interesting) because, as an incremental-computing compiler based on a red-green AST, we have to keep track of where every bit of information comes from (in terms of AST nodes) to be able to provide good diagnostics. This is especially important given the previous point: we need to be able to tell the end-user why an expression was given a specific type.
  • Implementing this type checker might increase the complexity of the codebase, but that's not certain. The current type checker looks like an unnavigable mess, and some formalization could actually simplify parts of it.