A Compact Algorithm W Implementation in Clojure
Damas-Hindley-Milner / Algorithm W implemented in Clojure using atoms. Informed by the OCaml GYOTS implementation, though much more succint. This is only in part because of avoiding the ranked type optimization. I previously implemented a less mature, purely functional version of this same algorithm here, without proper support for generics. Type inference is about 100 lines, with about 80 more in a separate namespace to get the inputs and outputs such that they can reasonably be supplied by / read by a human. When we’re done, we’ll be able to do stuff like:
Note that in the type declaration DSL, the -> is being used as a prefix typing arrow, to connect a function’s parameter types to its return type, not as Clojure’s thread first macro. Similarly, none of the overlapping symbols like cons, map, empty, not, etc. have any external semantics. I think the implementation is quite easy to follow. The basic conceit is that we use atoms for type variables, and use a [:link <target>] value when we’ve unified a type variable, so that we can pattern match on it after dereferencing and recursively call whatever function on the contents. In the dispatch code, :type-app refers to the application of a type to generic type variables, as in [list [a]] above.
It’s most helpful if we show the frontend of the inference engine first, which translates S-expressions into tagged vectors for consumption by infer/unify. There is a distinction between type declarations, which are mostly literals, except for the for-all and arrow operators (see translate-decl) and programs (see translate).
