[−][src]Crate minitt
Reading the README is recommended before reading the documentation.
Tutorial
Here's a brief summary of the complete type-checking process.
Since this implementation is actually a dialect or, a variantion of the original one, I use minitt
to represent this implementation and Mini-TT for the original one.
Only language features that affect type-checking are listed.
First, Mini-TT supports:
- Pi/Sigma types
- First-class sum types and pattern matching
- Recursion
Mini-TT does not support (while you may expect it to support):
- Dependent pattern matching (with unifications)
- Meta variables, say, implicit arguments
Mini-TT does not, but minitt does support:
- Functions returning functions (curried functions) (cubicaltt supports this too) with the help of an additional member of lambda expressions
- Infer types of expressions that appears deeply inside an expression
- Constant expressions with type signature completely inferred
- Subtyping on sum types (work in progress)
Syntax Trees
Mini-TT has three syntax trees:
- Surface syntax tree, aka concrete syntax tree, representing expressions that cannot be type-checked alone or simply not type-checked yet
- Abstract syntax tree, aka values or terms, representing expressions
that are already type-checked. This implies "no free variables"
- Values might be neutral values: these values represents variable bindings that are not free but not reducible, like a parameter, or an expression that cannot be reduced due to the presence of this parameter
- Values might be closures: expression + context + parameter bindings
- Normal form syntax tree, aka normal forms.
This is the output of the
read-back
functions- Details are introduced later. Personally, I consider this not necessary and ugly.
Type-Checking
Mini-TT supports inferring types of simple expressions like applications, variable references, etc. But not the case for even a bit more complicated structures, like lambdas.
checkD
Each program is a sequence of definitions, each definition comes with a type signature and a body expression. We check the definitions one by one, after checking each definition we add it to the context and check the rest. For recursive definitions, we generate a neutral value before actually checking it.
This part is quite trivial Mini-TT, but minitt extended definitions with prefix parameters, which are parameters present before the type signature and the body expression, resulting in a much more complicated implementation.
check
All definitions in Mini-TT comes along with a type signature, Mini-TT tries to type-check the
signature and then try to match the body expression with the signature, using some hard-coded
patterns (relavant codes are in check/expr.rs), like if the type
is a pi-type and the value is a lambda, then we go on checking their bodies and types with the
parameter instantiated as a generated value then recursively check if the instantiated body
expression is an instance of the pi-type's return type; if the type is a sum type and the value
is a constructor call, then check if the constructor is present in the sum.
If all rules are not applicable, infer the expression type and do a subtyping comparison.
This comparison is doing some hard-coded comparisons as well. If it still fails, read-back
to
normal form and do a syntactic comparison with the read-back
ed expected type signature.
This is the so-called instance of
check, the function name in Mini-TT paper is check
.
checkI
Trivial function, try to infer the type of a given expression.
Cannot infer types of lambdas or other complicated expressions like nested function calls (this situation has been improved a lot if you're glad to use prefix parameters).
checkT
Check if an expression is a type expression. Trivially implemented.
Possible Extensions
Several extensions can be made apart from the improvements that have nothing to do with the core type theory. I'm listing all the possible extension, disregarding how hard can the implementation be.
- Indexed inductive families
- Dependent (co)pattern matching
- Props
- Without-K
- Quantitative Type Theory
- Linear Type System
- Affine Type System
- First-class cases and sums
- Record polymorphism
- Cubical Type Theory
- Already implemented in another Mini-TT dialect: cubicaltt
- Cartesian Cubical Type Theory
- De Morgan Cubical Type Theory
- Coinduction and Guarded Recursion
- Sized types (implicit?)
Modules
ast | Syntax: term, expression, context. |
check | Type checking: everything related to type-checking, including: |
eval | Reduction: eval and eval's friends. |
parser | Parser, from text to AST and a bunch of utilities |
pretty | Pretty print utilities |
Macros
tce_unreachable |