Unification based typing - #161
Merged
Merged
Conversation
… monad into a new Unification.lean, and name the predicate rule for the syntax it elaborates, so that the machinery elaboration is about to grow has a home below the file holding the rules.
…riables, the solving state, the pending IR and the constraints in Unification.lean, the rules walking the untyped IR in Typing.lean, their erasure proofs in Erasure.lean, and the one-step unfolding a match will need in the verifier.
…tted local type is solved from its uses rather than defaulted and joined, a match unfolds its scrutinee's name where it is compiled rather than through a cast, a return type and a call's arguments are checked by equality, and a raise is typed at whatever result its context expects.
…st node, the subtyping relation with the weight and depth measures bounding it and the logical-relation lemma interpreting it, the join and meet operations, the per-intrinsic scheme matching the elaborator once called to instantiate a primitive, the lawfulness witness for the empty embedding no raise is typed at any more, and the pointwise ordering on typing contexts nothing had asked for in some time.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
This PR changes the type system from one based on subtyping to one based on unification. This should make it more intuitive going forward (more closely aligned with OCaml), and it also simplifies the verifier itself. Finally, it should make it easier to generalise to polymorphism.