Repository navigation
Type system framework for Kirin - #855
Draft
planza-quera wants to merge 6 commits into
Draft
planza-quera wants to merge 6 commits into
planza-quera wants to merge 6 commits into
Conversation
- `identifier!` named `Id` unqualified and `Identifier` through the private `arena` module, so it only expanded inside kirin-ir modules that imported `Id`. - Refer to both through their `$crate` re-exports, so other crates can declare arena ids with it. - Drop the `Id` imports that existed only for the macro.
- New crate `kirin-types`: the implementation of an ATS-style type system. - Sorts (`type`, `bool`, and dialect index sorts via `IndexSort`), literal values (`SortValue`), and static constructor sets via `StaticSig` (signature plus evaluation on literals). - `StaticTerm` in locally nameless form, arena-allocated in `Statics`: de Bruijn `Bound` indices, named `Free` variables with a sort and a name hint, literals, constructors, type formers and quantifiers. - `Statics::check_sort`, `term_eq`, `mentions`, and `display` for diagnostics; `SortError`. - The tests build terms from the `int` and `bool` constructor sets, so they compile from the next commit.
- `IntSort` with `IntStaticCon`: linear arithmetic, `≥`, and the singleton type `int(n)`; evaluation uses checked arithmetic. - `BoolStaticCon`: connectives, equality at each sort, and the singleton type `bool(B)`. - `kirin-test-utils` gains a `types` feature with `assert_eval_matches_signature`, used to test both sets.
- `map_term`: a shared bottom-up rebuild of a static term that keeps unchanged subterms shared. - `Statics::instantiate` replaces a binder's bound variables with arguments (outermost first) and lowers the remaining indices. - `Statics::close` turns a free variable into a bound one, for wrapping in a new binder.
- `Statics::reduce` folds constructor applications whose arguments are all literals, through `StaticSig::eval`, sharing what it can't fold. - Checks the argument count before evaluating, and rejects a result of the wrong sort with `SortError::EvalSort`.
- `DynTerm`: the dynamic level, with named variables and constructors applied through signatures (`DynSig`) stored in `Dynamics`. - `Dynamics::check_type` synthesizes a term's type in a `Scope` of variable types and assumed propositions, instantiating signatures and quantifiers and comparing types after folding constants. - `slam` and `unpack` reject a static variable that the scope's types or assumptions already mention (`StaticRebound`), so a binder can't capture it. - Guard and assertion entailment are left as TODOs for a solver. - `TypeError` for dynamic terms.
This branch has not been deployed
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
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.
Work in Progress.
Documentation will come, for now refer to https://quera.atlassian.net/wiki/spaces/SSW/pages/2536440005/Kirin+-+Type+System+Framework