Type inference for lists: way complicated

[m0ar]

Lists are represented as recursive application of the constructor Cons in the abstract syntax, which makes it very hard to grasp and implement in the type inference algorithm. Input/ideas/solutions on this, or alternative representation for the AS would be very helpful.

[m0ar]

One idea would be to put a special case when an App is found, see if it's an application of a Cons onto an element, but how can we then find the next element / connect it with the previous?

[JonasDuregard]

No special cases please! :)

An expression like Cons x xs is (from the perspective of the type checker) just a function application, so if you can type check function applications you can type check this as well.

Much like in your interpreter, you need to add Cons to the environment with its correct type. Cons is type a -> [a] -> [a], and it's polymorphic so its type would be Scheme ["a"] (TFun (TVar "a") (TFun (TConstr "[]" [TVar "a"]) (TConstr "[]" [TVar "a"])).

This assumes TConstr can do applications of type constructors, like PConstr in your patterns, not just the constructors themselves.

[m0ar]

@JonasDuregard The thing is that in the abstract syntax, it is modelled as
EApp (EApp (EConstr "Cons") eTwo) (EConstr "Nil") which makes the two list parts reachable only from the EApp case in the typechecker. Are we missing something?

[JonasDuregard]

That is what I meant by them being just function applications.

The case you need to think about is EConstr. It is currently wildly incorrect (type constructors are not the same as value constructors!).

If your inferencer correctly infers the type of (EConstr "Cons") to a1 -> [a1] ->[a1](for some new variable a1) and (EConstr "Nil") to [a2] (for some new variable a2), it will all work out great. From the inner EApp it will deduce that the type of eTwo must be unified with a1, from the second it will deduce that [a1] must be unified with [a2] (so a2 unifies with a1 which is already unified with the type of eTwo).

[JonasDuregard]

Regarding "finding the next element", that is the job of the interpreter. The type checker has no notion of this, it traverses the expression it type checks not the values the expression would evaluate to.

[JonasDuregard]

Regarding recursion, it's a bit tricky when polymorphism is involved. It seems the standard approach for let x = e1 in e2 is something like this:

1. Introduce a new type variable a
2. Bind x to type a (monomorphic)
3. Infer the type t of e1
4. Unify t with a
5. Re-bind x to t (polymorphic/generalized)
6. Infer type of e2
   This basically means that you can not instantiate x with two different types inside the definition of x (without a type signature), which is hardly ever a problem.