Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
Unification implementation plan.

MVP unification implementation plan

The implementation of unification (inference) following this document can be split into a few smaller, separate tasks/PRs for smoother transition and easier testing.

Stage 1: Type checker enhancement

At the time of writing, the first stage of the totality checker MVP is finished. But the second and third stages, namely type checking data type and function declarations are required before unification can be implemented.

At the end of this stage, conversion/type checking for constructors is implemented.

Stage 2: Global context enhancement

Hole and Guess should be added to our global context for meta-variables. We may want to parameterize our global context constructors more heavily like in Idris 2 to avoid mistakes.

Implement functions unify as an extension of conversion checking. Add UState and supporting functions etc.

Implement newMeta and newConstant.

Stage 3: Update the type checker to use unify

typeTerm should call unify instead of the conversion function. During type checking, when we encounter an Implicit, we make a meta-variable with the expected type, and hope that unifying the meta-variable and the expected type will succeed. (See the last part of the Unification in Idris 2 document).

Stage 4: Optimization

We may need to reduce the time it takes for unification to finish. It could be rather slow. We could implement optimization tweaks to improve efficiency. For example, when do we call solveConstraints? Calling it at strategic times can improve efficiency dramatically. Can we compare terms in some circumstances without converting them to Value?

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment