Changelog for lambda-cube-0.3.0.0
Unreleased
0.3.0.0
Main updates
- Type/Kind level quasiquoter are added.
- Evaluators are added to the top-level modules.
- STLC and System F omega are tested with various examples.
- Identifiers now accepts
_
.
Bug fixed
- Substitutions are fixed with valid shifting.
- STLC normalizer is fixed with valid beta-reduction.
- Fix type inference for System F and System F omega.
Breaking changes
- Names of quasiquoters are changed.
- The order of arguments for substitution are changed.
- Non-Ast modules now have explicit export lists.
0.2.0.0
Main updates
- New top-level module for each lambda calculus is added.
It make easier to use one specific lambda calculus under a qualified name. - Quasiquoter now supports splicing-in.
- Change the type of elaborator and type checker for composability.
Currently they are less type-safe. However, monad to make them type-safe will be added in the future.
Breaking changes
- Lifters and substitutions into dedicated modules are moved.
- Pretty printers are renamed.
- Elaborators are renamed.
- Quasiquoter are renamed.
- Elaborated quasiquoters are remove.
- The types of elaborators and type checkers are changed.
0.1.0.0
The first release including support for following 4 lambda calculi.
- Simply Typed Lambda Calculus
- System F
- System F omega underbar
- System F omega