three pass type checking?

[zetah11]

While working on #24, I've been thinking a bit about how to simplify the type checker. I think I have an idea for how to do this, but I haven't fully thought it through to see if it would work.

Basically, the current type checker needs to

• Check/infer the kind of types
• Check/infer the types of values
• Concretify existentials (not yet implemented)

which makes things complicated because these all work in different ways. However, if we make some assumptions, I think we can separate these into separate passes:

1. The kind of a type cannot depend on value information (e.g. no pattern matching on a value where branches have different kinds)
2. The concrete type of an existential cannot affect inference

I believe 1. is a perfectly reasonable restriction. I'm not quite sure if 2. is too restrictive, though - one thing I'm worried about is how this interacts with implicits (ideally, I'd like to be able to use the inferred implicit to direct type checking, but maybe that's okay since these kinds of implicits should only appear explicitly)

Anyways, if we can separate these, then we can do fun things like use one of the bog standard HM inference algorithms with generalization for kind checking and concrete type inference, while having the more bidirectional coercy one in the value world.

[zetah11]

Okay, some thoughts about kind inference. I can imagine there are two alternatives:

1. do the kind inference without the extra information that types used in the value world must have kind type
2. do the kind inference with that extra information

1 is easier, but 2 is perhaps more powerful - if this extra information is necessary. I believe we can restrict the type language to a decidable HM-like thing, in which case we get kind polymorphism, type level functions, and all these goodies for free (and since it's just the type language, there will be no need to worry about mean things like mutability). But, more pressingly, if that restriction is made and upheld, then it shouldn't matter which approach we choose (since, if something has an ambiguous kind, it will just get generalized).

And if that is the case, then it's easy to choose 1 and have kind inference be its very own pass.

[zetah11]

One issue with splitting up kind- and type checking is that eventually I want to add classes and traits, which ends up making the two checkers depend on each other.

The main motivation I have for doing this, anyway, is to simplify the compiler and make a more modular type checker - which os currently probably the most complicated part of the compiler, apart from the partial evaluator.

I think it should be possible to keep a relatively clean separation, though. I'm imagining a high-level checker which is responsible for going through every strongly connected component which can then delegate tasks like kind and type checking to independent sub-checkers that keep their own state.

For the time being, though, separation is perfectly fine and I will start with it that way.