Incremental typechecking

[dhess]

Incremental typechecking

[hmac]

Our current approach is to blindly apply an action and then perform a full typechecking pass, and abort if that fails. This guarantees that we will never apply an action that causes a type error but is extremely inflexible and inefficient. Hazelnut is smarter than this, inserting holes where necessary to ensure that the action can be applied whilst maintaining type correctness. We want to do something similar.

The current approach I have in mind is twofold:

• persist type information in the AST, so we don't have to recreate it each time
• when applying an action, perform some amount of local typechecking/inference, making use of the cached type information to avoid having to recheck the whole program.

There are at least two difficulties with this approach:

• We still need a typing context available when doing local typechecking, so we may need to walk the AST from the root to the node in question to build this up. The context should tell us both what bindings are in scope (and their type) and also whether the node we are looking at is being checked against a type or being asked to synthesise a type.
• It's probably easier to introduce typechecking bugs by relying on stale typing information - we should pay attention to this when introducing new syntactic forms (a simple example: changing a type definition will require a complete check of the whole program).