rzk-lang / rzk Goto Github PK

View Code? Open in Web Editor NEW

202.0 202.0 8.0 57.49 MB

An experimental proof assistant based on a type theory for synthetic ∞-categories.

Home Page: https://rzk-lang.github.io/rzk/

Haskell 82.51% Nix 4.57% Makefile 1.18% CSS 0.78% TypeScript 7.93% JavaScript 0.16% EBNF 2.70% HTML 0.17%

category-theory haskell homotopy-type-theory proof-assistant

rzk's People

Contributors

Stargazers

Watchers

Forkers

drruisseau deemp agifoundation eakubilo ncfavier geffk2 swamp-agr nimarasekh

rzk's Issues

Insufficient typechecking

In the following formalisation, type parameters of flip are not checked sufficiently:

#lang rzk-1

-- Flipping the arguments of a function.
#def flip
  : (A : U) ->                        -- For any types A
    (B : U) ->                        --           and B
    (f : (x : A) -> (y : B) -> A) ->  -- given a function f : A -> B -> A
    ((x : B) -> (y : A) -> A)         -- we construct a function of type B -> A -> A
  := \A -> \B -> \f ->
      \y -> \x -> f x y               -- by swapping the arguments

-- Flipping a function twice is the same as not doing anything
#def flip-flip-is-id
  : (A : 1) ->                        -- For any types A
    (B : U) ->                        --           and B
    (f : (x : A) -> (y : B) -> A) ->  -- given a function f : A -> B -> A
    flip A B (flip A B f)             -- flip (flip f) <-- BUG HERE, should be flip B A (flip A B f)
      =_{(x : A) -> (y : B) -> A}     -- is identical
      f                               -- to f
  := \A -> \B -> \f ->
      refl_{f}                        -- proof by reflexivity

Add syntax highlighting plugin for VS Code

It would be nice to have syntax highlighting in VS Code.

Online playground does not work in Chrome

The Miso app does not load in Chrome for some reason. Firefox and Safari work well.

Add imports

It would be great to be able to import from files/URLs.

Factor out syntax highlighting

We have many syntax highlighting configs already:

HighlightJS is used in the generated MkDocs files. See docs/custom_theme/js/rzk.js.
CodeMirror highlighting is used in the playground. See try-rzk/playground.html.
BNFC generates Pygments files for highlighting that can be used, e.g. with minted package for LaTeX. However, for best highlighting, these should be manually adjusted.
VS Code extension (see fizruk/vscode-rzk) has its own highlighting config.

Unfortunately, I'm not aware of a tool/approach that would allow to generate an acceptable version for all these in one go.

In any case, at least the HighlightJS is currently used in several repositories (e.g. this one, emilyriehl/yoneda, and fizruk/sHoTT). So at least that one should be factored out to be reused.

Linux binary does not work on Ubuntu 20.04

I can't tell whether the issue is with my computer or with the way I'm trying to typecheck in vscode or both. I can't find our previous discussion so I'm opening a new issue, but feel free to close and redirect me elsewhere.

My vscode extension is up to date.

From the terminal inside vscode I navigate into the hott folder of the yoneda repository and type rzk typecheck *-*.md which yields the following error message:

rzk: /lib/x86_64-linux-gnu/libc.so.6: version `GLIBC_2.33' not found (required by rzk)
rzk: /lib/x86_64-linux-gnu/libc.so.6: version `GLIBC_2.34' not found (required by rzk)
rzk: /lib/x86_64-linux-gnu/libc.so.6: version `GLIBC_2.32' not found (required by rzk)

But maybe this is the wrong way to go about it? When I navigate (still using the terminal inside vscode) over to the rzk repository I can typecheck successfully using stack exec rzk typecheck followed by the path to the files.

In case it's relevant I'm running Ubuntu 20.04

Add location info in the type errors

There are two ways this should be possible:

trifecta already is capable of producing regions for parsed parts of the AST, and can pretty print the context as text
It would be useful to have an option to spit errors in a structured format, to implement proper IDE support later (e.g. by building a language server for rzk)

Check for duplicate definitions

Duplicate definitions at the top level should probably be considered an error.

Add Agda-input support to playground

There is a plugin for CodeMirror enabling Agda-input mode: https://github.com/Codewars/codemirror-agda

Add location information to error messages

Type errors should hold information on the range (start and end positions) in the code where the type error occurred.

Publish the MkDocs SVG rendering plugin as a PyPI package

Currently, the generate_svgs.py plugin is registered as a hook. To be able to reuse it with other projects that depend on rzk, it should be packaged as a proper MkDocs plugin and published on PyPI so that others can install and use it.

Possible configuration options:

Path to rzk binary (defaults to using PATH)

Question: Is it desirable to automatically install rzk (from GitHub releases) if not found?

Type checker goes into an infinite loop

The following code makes the current typechecker go into an infinite loop:

#lang rzk-1

#def iscontr : (A : U) -> U
  := \A -> ∑ (a : A), (x : A) -> a =_{A} x

#def prod : (A : U) -> (B : U) -> U
  := \A -> \B -> ∑ (x : A), B

#def isweq : (A : U) -> (B : U) -> (f : (x : A) -> B) -> U
  := \A -> \B -> \f -> ∑ (g : (x : B) -> A), prod ((x : A) -> g (f x) =_{A} x) ((y : B) -> f (g y) =_{B} y)

#def weq : (A : U) -> (B : U) -> U
  := \A -> \B -> ∑ (f : (x : A) -> B), isweq A B f

#def relfunext : U
  :=
    (I : CUBE) ->
    (psi : (t : I) -> TOPE) ->
    (phi : (t : I) -> TOPE) ->
    (A : <{t : I | psi t} -> U >) ->
    (iscontrA : <{t : I | psi t} -> iscontr (A t) >) ->
    (a : <{t : I | psi t /\ phi t} -> A t >) ->
    <{t : I | psi t} -> A t [ psi t /\ phi t |-> a t]>

#def relfunext2 : U
  :=
    (I : CUBE) ->
    (psi : (t : I) -> TOPE) ->
    (phi : (t : I) -> TOPE) ->
    (A : <{t : I | psi t} -> U >) ->
    (a : <{t : I | psi t /\ phi t} -> A t >) ->
    (f : <{t : I | psi t} -> A t [ psi t /\ phi t |-> a t ]>) ->
    (g : <{t : I | psi t} -> A t [ psi t /\ phi t |-> a t ]>) ->
    weq (f =_{<{t : I | psi t} -> A t [ psi t /\ phi t |-> a t ]>} g)
      <{t : I | psi t} -> f t =_{A t} g t [ psi t /\ phi t |-> refl_{f t} ]>

#def restrict
  : (I : CUBE) ->
    (psi : (t : I) -> TOPE) ->
    (phi : (t : I) -> TOPE) ->
    (A : (t : I) -> U) ->
    (a : <{t : I | psi t} -> A t >) ->
    <{t : I | psi t /\ phi t} -> A t >
  := \I -> \psi -> \phi -> \A -> \a ->
     \t -> a t

#def ext-of-restrict
  : (I : CUBE) ->
    (psi : (t : I) -> TOPE) ->
    (phi : (t : I) -> TOPE) ->
    (A : (t : I) -> U) ->
    (a : <{t : I | psi t} -> A t >) ->
    <{t : I | psi t} -> A t [ psi t /\ psi t |-> restrict I psi phi A a t ]>
  := \I -> \psi -> \phi -> \A -> \a ->
     \t -> a t

#def restricts-path
  : (r : relfunext2) ->
    (I : CUBE) ->
    (psi : (t : I) -> TOPE) ->
    (phi : (t : I) -> TOPE) ->
    (A : (t : I) -> U) ->
    (a_psi : <{t : I | psi t} -> A t >) ->
    (a_phi : <{t : I | phi t} -> A t >) ->
    (e : <{t : I | psi t /\ phi t} -> a_psi t =_{A t} a_phi t >) ->
    restrict I psi phi A a_psi
      =_{ <{t : I | psi t /\ phi t} -> A t > }
    restrict I phi psi A a_phi
  :=
    \r ->
    \I -> \psi -> \phi -> \A -> \a_psi -> \a_phi -> \e ->
    (first (second (r I
      (\t -> psi t /\ phi t)
      (\t -> BOT)
      (\t -> A t)
      (\t -> recBOT)
      (\t -> a_psi t)
      (\t -> a_phi t)))) e

#def recOR-id
  : (I : CUBE) ->
    (psi : (t : I) -> TOPE) ->
    (phi : (t : I) -> TOPE) ->
    (A : (t : I) -> U) ->
    (a_psi : <{t : I | psi t} -> A t >) ->
    (a_phi : <{t : I | phi t} -> A t >) ->
    (e : <{t : I | psi t /\ phi t} -> a_psi t =_{A t} a_phi t >) ->
    <{t : I | psi t \/ phi t} -> A t >
  := \I -> \psi -> \phi -> \A -> \a_psi -> \a_phi -> \e ->
     \t -> recOR(psi t, phi t, ext-of-restrict I psi phi A a_psi t, ext-of-restrict I phi psi A a_phi t)

The culprit is in the last line of the code. Note that it is not supposed to typecheck, but give a type error, since a_psi and a_phi are not definitionally equal on psi t /\ phi t.

Failed to install rzk through cabal

cabal install rzk failed with the following error message:

Failed to build rzk-0.4.0.
Build log ( /Users/egbertrijke/.cabal/logs/ghc-9.4.4/rzk-0.4.0-3718e246.log ):
Configuring library for rzk-0.4.0..
Preprocessing library for rzk-0.4.0..
Building library for rzk-0.4.0..
[ 1 of 13] Compiling Free.Scoped      ( src/Free/Scoped.hs, dist/build/Free/Scoped.o, dist/build/Free/Scoped.dyn_o )
[ 2 of 13] Compiling Free.Scoped.TH   ( src/Free/Scoped/TH.hs, dist/build/Free/Scoped/TH.o, dist/build/Free/Scoped/TH.dyn_o )
[ 3 of 13] Compiling Language.Rzk.Syntax.Abs ( src/Language/Rzk/Syntax/Abs.hs, dist/build/Language/Rzk/Syntax/Abs.o, dist/build/Language/Rzk/Syntax/Abs.dyn_o )
[ 4 of 13] Compiling Language.Rzk.Syntax.Lex ( dist/build/Language/Rzk/Syntax/Lex.hs, dist/build/Language/Rzk/Syntax/Lex.o, dist/build/Language/Rzk/Syntax/Lex.dyn_o )

dist/build/Language/Rzk/Syntax/Lex.hs:572:50: error:
    • Couldn't match expected type ‘Int16#’ with actual type ‘Int#’
    • In the fifth argument of ‘alex_scan_tkn’, namely ‘sc’
      In the expression:
        alex_scan_tkn user__ input__ 0# input__ sc AlexNone
      In the expression:
        case alex_scan_tkn user__ input__ 0# input__ sc AlexNone of
          (AlexNone, input__')
            -> case alexGetByte input__ of
                 Nothing -> AlexEOF
                 Just _ -> AlexError input__'
          (AlexLastSkip input__'' len, _) -> AlexSkip input__'' len
          (AlexLastAcc k input__''' len, _)
            -> AlexToken input__''' len (alex_actions ! k)
    |
572 |   = case alex_scan_tkn user__ input__ 0# input__ sc AlexNone of
    |                                                  ^^

dist/build/Language/Rzk/Syntax/Lex.hs:602:1: error:
    Couldn't match type ‘Int#’ with ‘Int16#’
    Expected: t1
              -> t2
              -> Int#
              -> AlexInput
              -> Int16#
              -> AlexLastAcc
              -> (AlexLastAcc, (Posn, Char, [Byte], String))
      Actual: t1
              -> t2
              -> Int#
              -> (Posn, Char, [Byte], String)
              -> Int#
              -> AlexLastAcc
              -> (AlexLastAcc, (Posn, Char, [Byte], String))
    |
602 | alex_scan_tkn user__ orig_input len input__ s last_acc =
    | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^...

dist/build/Language/Rzk/Syntax/Lex.hs:617:27: error:
    • Couldn't match expected type ‘Int#’ with actual type ‘Int32#’
    • In the first argument of ‘(+#)’, namely ‘base’
      In the expression: base +# ord_c
      In an equation for ‘offset’: offset = (base +# ord_c)
    |
617 |                 offset = (base +# ord_c)
    |                           ^^^^

dist/build/Language/Rzk/Syntax/Lex.hs:620:73: error:
    • Couldn't match expected type ‘Int#’ with actual type ‘Int16#’
    • In the first argument of ‘(==#)’, namely ‘check’
      In the first argument of ‘tagToEnum#’, namely ‘(check ==# ord_c)’
      In the second argument of ‘(&&)’, namely
        ‘(tagToEnum# (check ==# ord_c))’
    |
620 |                 new_s = if GTE(offset,0#) && EQ(check,ord_c)
    |                                                                         ^^^^^

dist/build/Language/Rzk/Syntax/Lex.hs:625:13: error:
    • Couldn't match expected type ‘Int16#’ with actual type ‘Int#’
    • In the pattern: -1#
      In a case alternative: -1# -> (new_acc, input__)
      In the expression:
        case new_s of
          -1# -> (new_acc, input__)
          _ -> alex_scan_tkn
                 user__ orig_input
                 (if c < 0x80 || c >= 0xC0 then (len +# 1#) else len) new_input
                 new_s new_acc
    |
625 |             -1# -> (new_acc, input__)
    |             ^^^
[ 7 of 13] Compiling Language.Rzk.Syntax.Print ( src/Language/Rzk/Syntax/Print.hs, dist/build/Language/Rzk/Syntax/Print.o, dist/build/Language/Rzk/Syntax/Print.dyn_o )

src/Language/Rzk/Syntax/Print.hs:16:1: warning: [-Wunused-imports]
    The import of ‘+, -’ from module ‘Prelude’ is redundant
   |
16 | import           Prelude                 (Bool (..), Double, Int, Integer,
   | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^...

src/Language/Rzk/Syntax/Print.hs:71:3: warning: [-Wunused-local-binds]
    Defined but not used: ‘onNewLine’
   |
71 |   onNewLine i p = (if p then id else showChar '\n') . indent i
   |   ^^^^^^^^^
[10 of 13] Compiling Paths_rzk        ( dist/build/autogen/Paths_rzk.hs, dist/build/Paths_rzk.o, dist/build/Paths_rzk.dyn_o )
[11 of 13] Compiling Rzk              ( src/Rzk.hs, dist/build/Rzk.o, dist/build/Rzk.dyn_o )
Error: cabal: Failed to build rzk-0.4.0 (which is required by exe:rzk from
rzk-0.4.0). See the build log above for details.

Add let-bindings

It is inconvenient to have to copy-paste expressions or introduce auxiliary definitions to imitate let-bindings. And this is a simple extension, so can be added in the current prototype.

Add #fail command to ensure another definition (or command) to fail

I guess we need #fail command in Rzk to mark definitions that should fail (and check that it fails indeed).

Originally posted by @fizruk in emilyriehl/yoneda#39 (comment)

[rzk-1] Proof for Theorem 4.2 (currying for extension types) does not typecheck

At the moment rzk-1 prototype does not handle currying of extension functions [RS17, Theorem 4.2] correctly. Consider the following snippet:

The output hints that it cannot identify k (t, s) = f (t, s) since zeta s constraint is not available for some reason (it should be):

Local tope context:
  phi t
  psi t

Expected type
  f
but inferred
  k
when trying to unify expected type
  λs → f ((t, s))
with inferred type
  λs → k ((t, s))
for the term
  λt → λs → k ((t, s))

undefined variable: Eq

With rzk v0.5, when trying to typecheck yoneda/src/simplicial-hott/04-extension-types.rzk.md, I'm getting:

src/simplicial-hott/04-extension-types.rzk.md:
  Error occurred when checking
    #define flip-ext-fun

undefined variable: Eq

I get the same error when permuting the definitions, e.g. putting curry-uncurry before.

Variables and sections

To reduce boilerplate in formalisations, it makes sense to introduce some simple organisational features, such as sections and variables (shared assumptions). I've implemented a version of these in develop, getting inspired by Lean and Coq. I ended up with Coq-style variables, but I'm not sure which one is better and why. Below are some examples and some of my thoughts.

Lean

Lean4 has Variables which can be used to automatically add bound variables to the following definitions:

variable (α β γ : Type)
variable (g : β → γ) (f : α → β) (h : α → α)
variable (x : α)

def compose := g (f x)
def doTwice := h (h x)
def doThrice := h (h (h x))
def plus4 := compose _ _ _ (fun x => x + 2) (fun x => x + 2)

Important properties of variable declaration in Lean4:

A given variable is added as a bound variable only if it is actually used in the definition (explicitly or implicitly). E.g. compose will not have h as its bound variable, but will have α, β, γ, g, f, and x bound variables. On the other hand, doTwice and doThrice only depend on α, h, and x.
Variables added in this way are explicit (they can be implicit if we use curly braces, e.g. variable {α β γ : Type}), even inside the same section. This is why plus4 calls compose with all 5 arguments.

Coq

Coq has Assumptions, including Variable and Hypothesis commands (which are equivalent).

Section example.
  Variable (α β γ : Type).
  Section compose.
    Variable (g : β → γ) (f : α → β) (h : α → α).
    Variable (x : α).
  
    Define compose := g (f x).
    Define doTwice := h (h x).
    Define doThrice := h (h (h x)).
    (* Define plus4 := compose. PROBLEM: compose is already saturated (fully applied). *)
  End compose.
  
  (* Type variables are already in scope. *)
  (* But g, f, and x become explicit arguments. *)
  Def plus4 := compose (fun x => x + 2) (fun x => x + 2).
End example.

(* Outside of section "example", type variables become explicit arguments. *)
Def plus4' := compose _ _ _ (fun x => x + 2) (fun x => x + 2).

Important properties of Variable command in Coq:

Similarly to Lean, only variables that are actually used in a definition are introduced as parameter upon exiting a section.
In contrast to Lean, variables are implicit in applications of definitions in the same section (this means that sometimes you need to exit section before you can properly use it).

Rzk (experimental)

There is an implementation of Coq-style variables and sections (see 469cde5, or develop branch at the time of writing). You can see an example use of this here: https://github.com/fizruk/rzk/blob/37708d49aa50fe866a4c54370b827b9ff0c6b1ca/docs/docs/rzk-1/recId.md?plain=1#L80-L187.

Originally, this seemed to be a nice approach, however, I now think this is setting up an issue:
it is too easy to accidentally use an extra assumption. For example, it is tempting to set #variable AisSegal : isSegal A to make the proof assistant automatically figure out when it is used, even when it is implicit. In particular, it would make it easy to use conclusion as assumption (e.g. when proving that A is Segal using a lemma that indirectly uses AisSegal).

This is less of a problem if we use Lean-style variables, since we would have to write AisSegal explicitly in the proof and will probably notice it. However, this might still become a problem once we add term inference and write _ instead of AisSegal (or a similar argument), or when it is introduced indirectly somehow (I would have to think of an example).

This suggests to me two things:

There is a strong need in a language server (see #31) to make sure users have easy access to see explicitly all assumptions of a definition.
It might make sense to add some extra checks/warnings when an assumption matches (exactly?) the conclusion in a definition.

Document syntax properly

Syntax introduced in rzk-0.2.0 is not documented properly yet.

Add shape types with coercions

It would be great to be able to work with shapes as types.

No syntax for shape inclusion

There is currently no syntax for shape inclusion, which is sometimes an inconvenience. For example, formulating relative function extensionality like this does not work:

#def relfunext : U
  :=
    (I : CUBE) ->
    (psi : (t : I) -> TOPE) ->
    (phi : {(t : I) | psi t} -> TOPE) ->
		(A : <{t : I | psi t} -> U >) ->
    (iscontrA : <{t : I | psi t} -> iscontr (A t) >) ->
    (a : <{t : I | phi t} -> A t >) ->
    <{t : I | psi t} -> A t [ phi t |-> a t]>

Currently this causes a type error when typechecking a:

Cannot satisfy the tope constraint:
  psi t
in local tope context

when typechecking term
  phi t

Temporary solution is to rely on intersection of shapes to imply inclusion:

#def relfunext : U
  :=
    (I : CUBE) ->
    (psi : (t : I) -> TOPE) ->
    (phi : (t : I) -> TOPE) ->
		(A : <{t : I | psi t} -> U >) ->
    (iscontrA : <{t : I | psi t} -> iscontr (A t) >) ->
    (a : <{t : I | psi t /\ phi t} -> A t >) ->
    <{t : I | psi t} -> A t [ psi t /\ phi t |-> a t]>

GHCJS build often fails

Apparently, this happens because GHCJS linker is running out of memory.
It is unclear what exactly causes this and how to properly fix it.
Perhaps, it might make sense to make a put the latest built JS binaries in a separate directory on gh-pages, and then remove all the experimental code for STLC, PCF, and MLTT, leaving only pure rzk-1 supported in new releases. This should significantly reduce the size of Haskell sources, so probably should help with the memory usage in GHCJS.

Missing coherence check

#def bug (A : U) (x : A) (y : A) (z : A) : U
 := {(t, s) : 2 * 2} -> A [ t === 0_2 |-> x, t === s |-> z]

Restriction types with multiple restrictions should have a coherence check, which appears to be missing.

Split into modules

The Rzk.TypeCheck module is now over 3k LoC and includes a lot of extra code. Should split into multiple modules and properly document.

Add proper command line interface

E.g. via optparse-generic.

Add #let command

Similar to #define, but would only introduce local definitions, unavailable from outside a section. Similar to Let command in Coq.

Add workflow to release binaries

Seems to be non-trivial, but doable. Would help to just be able to install binaries without having to build everything from sources.

Add `--version` command

Hi! This is a small feature request for the ability to write rzk --version or rzk -v in the terminal to figure out which version is used. This would benefit me as I'm easily confused by the Haskell package management tools. :)

I assume this is a sub-issue of #30, but I figured I could post the request regardless.

Add possibility to postulate axioms

Currently, all axioms have to be dragged explicitly as function dependencies.
However, it is not difficult to postulate axioms.
Some useful axioms are the relative function extensionality and monotonicity of 𝟚 → 𝟚.

Add shape types, coerce cubes and shapes to types

Name conflicts with global declarations

The following snippet fails to typecheck, because global x conflicts with local x in the definition of hom, for some reason.

#lang rzk-1

-- 1-simplex
#def Δ¹ : (t : 2) -> TOPE
  := \(t : 2) -> TOP

-- boundary of a 1-simplex
#def ∂Δ¹ : (t : 2) -> TOPE
  := \(t : 2) -> (t === 0_2 \/ t === 1_2)

-- boundary of a 2-simplex
#def ∂Δ² : (t : 2 * 2) -> TOPE
  := \(t, s) -> (s === 0_2 \/ t === 1_2 \/ s === t)

-- 2-simplex
#def Δ² : (t : 2 * 2) -> TOPE
  := \(t, s) -> s <= t

-- the (2,1)-horn
#def Λ : (t : 2 * 2) -> TOPE
  := \(t, s) -> (s === 0_2 \/ t === 1_2)

-- [RS17, Definition 5.1]
-- The type of arrow in A from x to y
#def hom : (A : U) -> (x : A) -> (y : A) -> U
  := \A -> \x -> \y -> <{t : 2 | Δ¹ t } -> A [ ∂Δ¹ t |-> recOR(t === 0_2, t === 1_2, x, y) ]>

#def x : U
  := U

Error parsing code blocks with attributes

It seems that the rzk type checker does not know how to handle code blocks with attributes in markdown.

For instance, the following code is completely ignored:

```rzk title="Rijke 22, Definition 9.3.1"
#def Eq-Σ
  ( s t : Σ (a : A) , B a)
  : U
  :=
    Σ ( p : (first s) = (first t)) ,
      ( transport A B (first s) (first t) p (second s)) = (second t)
```

The same happens if the attributes are wrapped in curly braces.

When I have two code blocks with attributes back to back, however, I get the following error:

An error occurred when parsing file src/hott/05-sigma.rzk.md
rzk: syntax error at end of file
CallStack (from HasCallStack):
  error, called at src/Rzk/Main.hs:67:9 in rzk-0.5.1-fd1942b5:Rzk.Main

Allow points in cubes/shapes in assumptions

Add #check command

The idea is to typecheck an expression (or infer its type) without giving it a name. Can be useful, e.g. to check that components of equivalences compute to desired mappings.

Properly configure package.yaml and rzk.cabal

In particular, it seems that build-tools have to be specified. #43 might be related.

Update playground to CodeMirror 6

We are currently using CodeMirror 5 which is not supported anymore, as far as I can see.

[rzk-1] Definition of Segal type does not typecheck

Consider the following snippet:

The last definition here does not typecheck, as hom A x y is failing to unify with (essentially) itself:

Local tope context:
  (t ≡ 0) ∨ (t ≡ 1)
  ⊤

Expected type
  rec∨(t ≡ 0, t ≡ 1, x, y)
but inferred
  x
when trying to unify expected type
  〈{t : 𝟚 | ⊤} → A[ ((t ≡ 0) ∨ (t ≡ 1)) ↦ rec∨(t ≡ 0, t ≡ 1, x, y) ]〉
with inferred type
  ((hom A) x) y
for the term
  f

Failed to typecheck due to a type error!

Add #compute command

A command to compute a term (to WHNF or NF). Can be useful for debugging.

Add literate Rzk LaTeX support

Rzk already has partial support in LaTeX (with the minted package, see here). Would be nice to also typecheck these files.

Fix collection of free variables in typed terms

The following code is incomplete:

https://github.com/fizruk/rzk/blob/936c15a37f52d77fac436558b5fbc18e31ea4e40/rzk/src/Language/Rzk/Free/Syntax.hs#L97-L103

This might not be critical, as it only affects used implicit variables checks, which work in a way that should collect all transitive dependencies anyway. But it would be great to fix this and, moreover, to be able to cache/reuse the set of free variables efficiently.

Add coproducts

Currently, we do not have coproducts, as they are not used in RS17. But it would be nice to have them.

Support literate rzk files

At least, we should support Markdown files with rzk blocks and check that examples in the documentation work on CI.

Implicit arguments

It seems that some conveniences strongly require implicit arguments, so it would be good to get those soon.

Syntax error on sections left open at the end of a file

Minimal example:

#lang rzk-1
#section left-open

Resulting error

> rzk typecheck test.rzk 
Loading file /src/test.rzk
An error occurred when parsing file /src/test.rzk
rzk: syntax error at end of file
CallStack (from HasCallStack):
  error, called at src/Rzk/Main.hs:79:11 in rzk-0.5.6-77841b86eb45b408582f63a681be46bfa60dae786116e8a3336e01207426afe9:Rzk.Main

A more informative error expliciting that a section has been left open (and its name) would be great.

Render yields an empty SVG

Trying to render a tetrahedron carved from a prism:

#set-option "render" = "svg"
-- The Segal-associativity-witness curries to define a diagram Δ²×Δ¹ -> A.
-- The Segal-associativity-tetrahedron is extracted via the middle-simplex map \((t, s), r) -> ((t, r), s) from Δ³ to Δ²×Δ¹
#def Segal-associativity-tetrahedron 
  (extext : ExtExt)         -- This proof uses extension extensionality.
  (A : U)                   -- A type.
  (AisSegal : isSegal A)    -- A proof that A is Segal.  
  (w x y z : A)             -- Four points in A.
  (f : hom A w x)           -- An arrow in A from w to x.
  (g : hom A x y)           -- An arrow in A from x to y.
  (h : hom A y z)           -- An arrow in A from y to z.
  : Δ³ -> A
  := \((t, s), r) -> 
    (\{(t1, (t2, t3)) : 2 * (2 * 2) | t2 <= t1 } ->(Segal-associativity-witness extext A AisSegal w x y z f g h) (t1, t2) t3) (t, (r, s))
#set-option "render" = "none"

Yields empty SVG.

#lang rzk-1

#def prod : (A : U) -> (B : U) -> U
  := \A -> \B -> ∑ (x : A), B

#def isweq : (A : U) -> (B : U) -> (f : (x : A) -> B) -> U
  := \A -> \B -> \f -> ∑ (g : (x : B) -> A), prod ((x : A) -> g (f x) =_{A} x) ((y : B) -> f (g y) =_{B} y)

#def weq : (A : U) -> (B : U) -> U
  := \A -> \B -> ∑ (f : (x : A) -> B), isweq A B f

#def relfunext2 : U
  :=
    (I : CUBE) ->
    (psi : (t : I) -> TOPE) ->
    (phi : (t : I) -> TOPE) ->
    (A : <{t : I | psi t} -> U >) ->
    (a : <{t : I | psi t /\ phi t} -> A t >) ->
    (f : <{t : I | psi t} -> A t [ psi t /\ phi t |-> a t ]>) ->
    (g : <{t : I | psi t} -> A t [ psi t /\ phi t |-> a t ]>) ->
    weq (f =_{<{t : I | psi t} -> A t [ psi t /\ phi t |-> a t ]>} g)
      <{t : I | psi t} -> f t =_{A t} g t [ psi t /\ phi t |-> refl_{f t} ]>

#def bug : (r : relfunext2) -> relfunext2
  := \r -> r

It seems that there is still a problem with handling of bound variables, so expansion of relfunext2 type is done incorrectly.