[chriswarbo]

> Rust (and Haskell) is not easy to _type-check_ though.

Is that really the case? It seems to me that a Prolog-like resolution system, coupled with a constraint solver, would get most of the job done with little effort.

There are certainly many rules to keep track of, but in some cases the newer rules are strict generalisations of the older rules. For example, Haskell's original type classes are just a special-case of modern multi-parameter, flexible instances/contexts, etc. type classes. Likewise, we can implement constraint kinds, type class instance resolution and type equalities using one constraint solver.

[sklogic]

Hindley-Milner is already quite Prolog-like. But you're right, CLP(fd) rocks for typing.

My usual approach to implementing a type system is to derive a flat list of Prolog equations out of the AST and leave it to Prolog for solving. If you ask what to do with error messages, I've got a comprehensive answer, but it is not for a mobile phone typing.

[another_user]

I'd really appreciate further comments on what to do with type errors for prolog/minikanren-like tools as typecheckers

[sklogic]

Ok, I've got a proper keyboard now.

My approach to the typing error reporting is quite compatible with the Prolog codegen. What I do: for each AST node which produce one or more type equations I record the location data (cache it and give it an index), and then issue a Prolog term like this: with_location(Id, Term), for each of the terms generated by this location.

with_location semantics is simple, but may depend on the presence of a backtracking. If it's a plain Hindley-Milner, there is no backtracking, and it simply do call/1(Term), continue if true, store Id and the failed term with all the current bindings and fail/0() if false.

If there is a backtracking, I store a stack of location ids and failure reasons instead, but this required patching the Prolog execution engine a little bit (luckily, I'm using my own Prolog for this).

Now, the next step is to decipher the failed term. Most of the equations are in a trivial form: equals(A, B), so I simply report that prolog_to_type(A) failed to unify with prolog_to_type(B). For the other (rare) kinds of equations I define custom pretty-printing rules.

[another_user]

Thanks, looks nice and pretty straightforward, will try it out