# Changelog for `rzk`
All notable changes to this project will be documented in this file.
The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/),
and this project adheres to the
[Haskell Package Versioning Policy](https://pvp.haskell.org/).
## v0.5 — 2022-06-20
This version contains the following changes:
- `Unit` type (with `unit` value) (see [ede02611]( https://github.com/fizruk/rzk/commit/ede02611 ) and [bf9d6cd9]( https://github.com/fizruk/rzk/commit/bf9d6cd9 );
- Add basic tokenizer support via `rzk tokenize` (see [#53]( https://github.com/fizruk/rzk/pull/53 ));
- Add location information for shadowing warnings and duplicate definition errors (see [bf9d6cd9]( https://github.com/fizruk/rzk/commit/bf9d6cd9 )).
## v0.4.1 — 2022-06-16
This is version contains minor changes, primarily in tools around rzk:
- Add `rzk version` command (see [f1709dc7]( https://github.com/fizruk/rzk/commit/f1709dc7 ));
- Add action to release binaries (see [9286afae]( https://github.com/fizruk/rzk/commit/9286afae ));
- Automate SVG rendering in MkDocs (see [#49]( https://github.com/fizruk/rzk/pull/49 ));
- Read `stdin` when no filepaths are given (see [936c15a3]( https://github.com/fizruk/rzk/commit/936c15a3 ));
- Add Pygments highlighting (see [01c2a017]( https://github.com/fizruk/rzk/commit/01c2a017 ), [cbd656cc]( https://github.com/fizruk/rzk/commit/cbd656cc ), [5220ddf9]( https://github.com/fizruk/rzk/commit/5220ddf9 ), [142ec003]( https://github.com/fizruk/rzk/commit/142ec003 ), [5c7425f2]( https://github.com/fizruk/rzk/commit/5c7425f2 ));
- Update HighlightJS config for rzk v0.4.0 (see [171ee63f]( https://github.com/fizruk/rzk/commit/171ee63f ));
## v0.4.0 — 2022-05-18
This version introduces sections and variables. The feature is similar to `Variable` command in Coq. An important difference, however, is that `rzk` does not allow definitions to use variables implicitly and adds `uses (...)` annotations to ensure such dependencies are not accidental.
- Variables and sections (Coq-style) (see [#38]( https://github.com/fizruk/rzk/pull/38 ));
Minor improvements:
- Add flake, set up nix and cabal builds, cache nix store on CI (see [#39]( https://github.com/fizruk/rzk/pull/39 ));
- Apply stylish-haskell (see [7d42ef62]( https://github.com/fizruk/rzk/commit/7d42ef62 ));
## v0.3.0 — 2022-04-28
This version introduces an experimental feature for generating visualisations for simplicial terms in SVG.
To enable rendering, enable option `"render" = "svg"` (to disable, `"render" = "none"`):
```rzk
#set-option "render" = "svg" -- enable rendering in SVG
```
Minor changes:
- Exit with non-zero code upon a type error (see b135c4fb)
- Fix external links and some typos in the documentation
Fixes:
- Fixed an issue with tope solver when context was empty (see 6196af9e);
- Fixed #33 (missing coherence check for restricted types).
## v0.2.0 - 2022-04-20
This version was a complete rewrite of the proof assistant, using a new parser, a new internal representation, and a rewrite of the typechecking logic. This is still a prototype, but, arguably, significantly more stable and manageable than version 0.1.0.
### Language
Syntax is almost entirely backwards compatible with version 0.1.0.
Typechecking has been fixed and improved.
#### Breaking Changes
The only known breaking changes are:
1. Terms like `second x y` which previous have been parsed as `second (x y)`
now are properly parsed as `(second x) y`.
2. It is now necessary to have at least a minimal indentation in the definition of a term after a newline.
3. Unicode syntax is temporarily disabled, except for dependent sums and arrows in function types.
4. The restriction syntax `[ ... ]` now has a slightly different precedence, so some parentheses are required, e.g. in `(A -> B) [ phi |-> f]` or `(f t = g t) [ phi |-> f]`.
5. Duplicate top-level definitions are no longer allowed.
#### Deprecated Syntax
The angle brackets for extension types are supported, but deprecated,
as they are completely unnecessary now: `<{t : I | psi t} -> A t [ phi t |-> a t ]>` can now be written as `{t : I | psi t} -> A t [ phi t |-> a t]`
or even `(t : psi) -> A t [ phi t |-> a t ]`.
#### Syntax Relaxation
Otherwise, syntax is now made more flexible:
1. Function parameters can be unnamed: `A -> B` is the same as `(_ : A) -> B`.
2. Angle brackets are now optional: `{t : I | psi t} -> A t [ phi t |-> a t ]`
3. Nullary extension types are possible: `A t [ phi t |-> a t ]`
4. Lambda abstractions can introduce multiple arguments:
```rzk
#def hom : (A : U) -> A -> A -> U
:= \A x y ->
(t : Δ¹) -> A [ ∂Δ¹ t |-> recOR(t === 0_2, t === 1_2, x, y) ]
```
5. Parameters can be introduced simultaneously for the type and body. Moreover, multiple parameters can be introduced with the same type:
```rzk
#def hom (A : U) (x y : A) : U
:= (t : Δ¹) -> A [ ∂Δ¹ t |-> recOR(t === 0_2, t === 1_2, x, y) ]
```
6. Restrictions can now support multiple subshapes, effectively internalising `recOR`:
```rzk
#def hom (A : U) (x y : A) : U
:= (t : Δ¹) -> A [ t === 0_2 |-> x, t === 1_2 |-> y ]
```
7. There are now 3 syntactic versions of `refl` with different amount of explicit annotations:
`refl`, `refl_{x}` and `refl_{x : A}`
8. There are now 2 syntactic versions of identity types (`=`): `x = y` and `x =_{A} y`.
9. `recOR` now supports alternative syntax with an arbitrary number of subshapes:
`recOR( tope1 |-> term1, tope2 |-> term2, ..., topeN |-> termN )`
10. Now it is possible to have type ascriptions: `t as T`. This can help with ensuring types of subexpressions in parts of formalisations, or to upcast types.
11. New (better) commands are now supported:
1. `#define ()* : := ` — same as `#def`, but with full spelling of the word
2. `#postulate ()* : ` — postulate an axiom
3. `#check : ` — typecheck an expression against a given type
4. `#compute-whnf ` — compute (WHNF) of a term
5. `#compute-nf ` — compute normal form of a term
6. `#compute ` — alias for `#compute-whnf`
7. `#set-option