Implementation detail of type inference

Author: Di Xu (https://www.google-melange.com/archive/gsoc/2014/orgs/clojure/projects/xudifsd.html)

This documentation describes implementation detail of function type inference.

infer-prest

infer-prest in cs_gen.clj is the function to infer function type with <* syntax, like hash-map with following type:

(All [k v]
  [(HSeq [k v] :repeat true) <* -> (Map k v)])

The signature of this function is [X Y S T T-var R expected], this is very similar to infer-vararg, except T-var is bound to type that on the left of <*, which is (HSeq [k v] :repeat true) in hash-map example.

I implement it in a very understandable way: split S at count of T into short-S and rest-S, wrap rest-S into HeterogeneousVector, and then invoke infer to do the real work.

Because I have already implemented cs-gen for HeterogeneousVector, HSeq and HSequential with repeat attribute. This should works fine.

The problem that concerns me is the explicit usage of HeterogeneousVector, and the ability that people can use whatever type they want to be left of <*, as long as that type has repeat attribute.

So if we support repeat in HeterogeneousList someday, and people use HList as prest type, it will get type error in all cases.

infer-pdot

infer-pdot in cs_gen.clj is the function to infer function type with <... syntax, like assoc with following type:

(All [m k v c ...]
   [m k v (HSeq [c c] :repeat true) <... c
    -> (Assoc m k v c ... c)])

syntax of <... is similar to ... syntax, which requires type on its left, and bounded symbol on its right.

The signature of infer-pdot is [X dotted-var dotted-bnd S T T-dotted R must-vars & {:keys [expected]}] which is similar to infer-dots. But we requires T-dotted must has repeat and type attributes.

I treat all types in types of T-dotted as pre-type, so I first substitute pre-type with fresh symbols generated by var-store-take.

Other part of infer-pdot is similar to infer-dots.

The main user of <... is assoc function, and rng is typically Assoc type. The problem I faced is that it is very difficult to do cs-gen with Assoc and HMap while checking with expected. Because HMap has so many attributes like optional, absent-keys, and we can not constraint very accurately on target, entries and dentries of Assoc, at this time.

I am wondering if we could construct expected type when we are done inference of all arguments, and then check constructed type with expected type. This will makes inference much easier to do, but I have not tried this way, and not sure if this works.

problem with cs-gen Assoc, HMap

This case is very difficult to handle, not only because HMap has so many attributes, but also because Assoc is not a complete type(it just simulate a function). So, when we do (cs-gen (Assoc m k v c ... c) (HMap :mandatory {:a Number :b String})) m could be either {}, {:a Number}, {:b String} or {:a Number :b String}, and type of k, v and c is also uncertain.

example

Right now we annotate assoc as

(All [m k v c ...]
   [m k v (HSeq [c c] :repeat true) <... c
    -> (Assoc m k v c ... c)])

and if we do

=> (t/cf (assoc {:a 1} :b "a") (HMap :mandatory {:a Number :b String}))

this will cause NYI error, because we have not supported cs-gen Assoc with dentries and HMap right now.

But if we do, we should generate constraint on Assoc and HMap, this is because HMap is our expected type. So how should we generate that constraints?

Should m be {} or {:a Number} or {:a Number :b String}, they are both possible type of first argument, like (assoc {} :a 1 :b "c"), (assoc {:a 1} :b "c") and (assoc {:a 1 :b "c"} :a 2).

Other variables like k, v and c are even more complicated, because order of arguments also matters. For example, (assoc {} :a 1 :b "c") will constraint k to be :a, v to be 1, and so on. But (assoc {} :b "c" :a 1) will constraint k to be :b, v to be "c". But they will generate same output, so the type of output should be same.

So I am wondering if we could delay the checking of expected type? We could check substituted Assoc with constraints we generated on arguments, and then check that substituted Assoc with expected type? But I am not sure where to insert this special case, in infer-pdot?