Typechecking algorithm

[FordArthur]

Since this is just an experimental project, it will be better if instead of copying some standard algorithm I try to develop my own

I will post the algorithm I have in mind here as I develop it

[FordArthur]

Since the AST for function definitions contain a pointer to the declaration of the function (which is null if is unspecified, and thus we need to infer it) and a pointer to all of the different function "implementations", we need to traverse all of the "implementations" and type check it against the declared type or/and it's other implementations

What it's not so clear to me is how I'm going to infer the type of a single function implementation. Specifically it's return type

[FordArthur]

Okay so,

Types will be represented with a vector of 64 bit values, in which each value either represents:

• a concrete type, in this case the 64 bit value would represent a pointer to the data type constructor (recognized by not having the sign bit set)
• an abstract type, in this case the 64 bit value would be split in 2: 15 bits for an identifier, and 48 bits for the implemented bits of a pointer to a constraints vector (if it's 0 then it has no constraints) (recognized by having the sign bit set)

With this type representation, types are compared like:

• if their sign bit is 0, we will always be pointing to the same structure, so the pointer is the same, thus comparing the values suffices
• if their sign bit is 1, then:
  • if they are in the same context, they must have the same identifier field (the constraints field is equal iff their identifier field is equal, since they share the context of a function), thus comparing the values suffices
  • if they aren't in the same context, they must have the same constraints (if the relation we are checking, however, is of belonging, i.e. a could be b, then we check if b has at least all of a's constraints)
• if their sign bit differs, we must check if the variable could adopt the value of the concrete, that is if the variable satisfies the constrains

How to iterate over declarations and implementations is trivial. The tricky part is how to infer the type of implementations. (I think) The following example covers every non-trivial case inferring implementations involve:

Suppose f a b c = a (b + c). We must find the types of a, b, c, and a (b + c). Call this last type value d.

We begin by solving for the expression's first argument, that is (b + c). + has type Num a => a, a -> a. We perform a substitution: b has type b, so after substituting it + is of type Num b => b, b -> b. c has type c. We cannot perform another substitution since all of the values in + have already been substituted. Therefore b is of type Num b => b, and so is c. Now, go back to a (b + c). + produces a Num b => b. Therefore a must take said type. Furthermore, a must produce a value of type d (Recall d was the type of the whole expression). Therefore a is of type Num b => b -> d. Solving for f's type is trivial now and may be even be exact in the implementation of this algorithm QED

[FordArthur]

This will involve rewriting some parts of the parser, so I'll probably also go ahead and try to fix making so many micro-allocations

[FordArthur]

Tfw it was just the Hindley–Milner typesystem