search

robrix / path

A lambda calculus to explore type-directed program synthesis.
BSD 3-Clause "New" or "Revised" License
83 stars 2 forks source link

Algebraic elaboration #97

Closed robrix closed 5 years ago

robrix commented 5 years ago

This PR synthesizes the approaches described in An Algebraic Approach to Typechecking and Elaboration and Type checking through unification in order to perform elaboration and unification using a new, and hopefully more resilient, model. Via the former, it also gives the sketch of a basic elaboration/tactic API.

robrix commented 5 years ago

Things are mostly in good shape, tho there are some failures still. Hoping to solve them in follow-up PRs.