anoma/juvix
1
1
Fork 0
mirror of https://github.com/anoma/juvix.git synced 2024-12-25 08:34:10 +03:00
Code Issues Projects Releases Wiki Activity

added new rules

Browse Source
This commit is contained in:
HackMD 2021-12-05 14:42:35 +00:00
parent 903b73b3b2
commit caaa753790
1 changed files with 162 additions and 74 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

236
docs/README.md
View File

@ -39,18 +39,19 @@ $$
MiniJuvix implements a programming language that takes variable resources very
seriously in the programs. As mathematical foundation, we are inspired by
Quantitative type theory (QTT), a dependent type theory that marriages ideas
from linear logic and traditional dependently typed programs to writing memory-
efficient programs using resource accounting. Some of the fincludes a universe,
dependent function types, tensor products, sum types, among others. The main
from linear logic and traditional dependently typed programs to writing memory-efficient programs using resource accounting. Among the language features, there is a type for a universe,
dependent function types, tensor products, sum types, among others.
The main
purpose of MiniJuvix is to serve as a guide to supporting/extending the
[Juvix](/Q5LbuHI5RXaJ8mD08yW7-g) programming language, in particular, the design
of its typechecker and the addition of new features.
We provide a work in progress report containing a description of the MiniJuvix
bidirectional type checking algorithm. Haskell sketches are provided on the
implementation of the algorithm.
In this document we provide a work in progress report containing a description
of the MiniJuvix bidirectional type checking algorithm. Haskell sketches are
provided on the implementation of the algorithm.
**Sources** The code is be available on the Github repository:
The code is be available on the Github repository:
[heliaxdev/MiniJuvix](https://github.com/heliaxdev/MiniJuvix). In this document,
we refer to the implementation provided in the `qtt` branch.
@ -110,13 +111,14 @@ computation is required in the $\sigma$ zero case. Otherwise, the judgement
possess *computation content*.
**Contexts** The contexts we judge a term are fundamental. A context can be either empty or
it can be extended by binding name annotations of the form $x
**Contexts** The context in which a term is judged is fundamental to determine
well-formed terms. Another name for context is *environment*. A context can be
either empty or it can be extended by binding name annotations of the form $x
\overset{\sigma}{:} M$ for a given type $A$.
$$
\begin{aligned}
\Gamma &\EQ \emptyset \Or \Gamma, x :^{\sigma} A & \text{(contexts)}
\Gamma &\EQ \emptyset \Or (\Gamma, x\overset{\pi}{:} A) & \text{(contexts)}
\end{aligned}
$$
@ -125,9 +127,23 @@ context $\Gamma$ is defined by induction on the structure of the contexts. Given
a scalar number $\sigma$, the product $\sigma \cdot \Gamma$ denotes the context
after multiplying *all* resources variables by $\sigma$.
The addition of context is a binary operation between contexts with the same
variable set. A context addition creates a new context which has all the
variables from the given context but with the resource varaibles summed up.
$$
\begin{aligned}
\sigma \cdot \emptyset &:= \emptyset,\\
\sigma \cdot (\Gamma, x \overset{\pi}{:} A) &:= \sigma \cdot \Gamma , x \overset{\sigma\pi}{:} A.
\end{aligned}
$$
The addition of context is a binary operation only defined between contexts with
the same variable set. This condition is the proposition $0 \cdot \Gamma_1 = 0 \cdot \Gamma_2$ between the contexts $\Gamma_1$ and $\Gamma_2$. Then, adding contexts create another one with all the
initial variables from the input with the resource varaibles summed up, as follows.
$$
\begin{aligned}
\emptyset+\emptyset &:=\emptyset \\
(\Gamma_{1}, x \overset{\sigma}{:} A)+(\Gamma_{2}, x \overset{\pi}{:} A) &:=(\Gamma_{1}+\Gamma_{2}), x^{\sigma+\pi} S
\end{aligned}
$$
**Telescopes** A *resource* telescope is the name for grouping types with some resource
variable information. We use telescopes in forming new types below, for example,
@ -185,20 +201,16 @@ i.e., $x : A$ and $x \overset{\sigma}{:} A$.
# Typing rules
We present the types rules in the same way as one would expect to see in the
implementation using the bidirectional approach. Then, even though when type
checking and type inference are mutually definied algorithms, checking goes
first and then inference, similarly, as with the following definition. See the corresponding file
[Core.agda](https://github.com/heliaxdev/MiniJuvix/blob/qtt/src/MiniJuvix/Syntax/Core.agda).
implementation using the bidirectional approach. We must also assume that the contexts appearing in the rules are *well-formed*.
```haskell
data Term : Set where
Checkable : CheckableTerm → Term -- terms with a type checkable.
Inferable : InferableTerm → Term -- terms that which types can be inferred.
{-# COMPILE AGDA2HS Term #-}
```
TODO: defined what means well-formed for contexts.
Checking and type inference are the functions `check` and `infer` in the
implementation. For example, the `infer` method is defined to work with three
Below, we describe the algorithms for checking and infering types in a mutually
defined way. The corresponding algorithms are the functions `check` and `infer`
in the implementation. The definition of each is the collection and
interpretation of the typing rules (read them bottom-up) given in this section.
For example, the `infer` method is defined to work with three
arguments: one implicit argument for the context $\Gamma$ and two explicit
arguments, respectively, the term $t$ and its quantity $\sigma$. The output of the algorithm is precisely the type $M$ for $t$ in the rule below.
@ -207,7 +219,7 @@ $$
\rule{}{
p_1 \cdots\ p_n
}{
\Gamma \vdash t \Rightarrow^\sigma M
\infer{\Gamma}{t}{\sigma}{M}
}
\end{gathered}
%
@ -220,6 +232,38 @@ type. A *reduction* step is denoted by $\Gamma \vdash t \rightsquigarrow t'$ or
simply by $t \rightsquigarrow t'$ whenever the context $\Gamma$ is known. Such a
reduction is obtained by calling `eval` in the implementation.
*Remark** A term in the
[Core](https://github.com/heliaxdev/MiniJuvix/blob/qtt/src/MiniJuvix/Syntax/Core.agda) implementation is either a checkable or inferable term. In a typing rule
the is no explicit reference to the term kind. However, that information becomes
evident after the given judgement mode in which the term is introduced/judged.
```haskell
data Term : Set where
Checkable : CheckableTerm → Term -- terms with a type checkable.
Inferable : InferableTerm → Term -- terms that which types can be inferred.
```
### Well-formed context
$$
\rule{\mathsf{empty}}{
%
}
{\emptyset \ \mathsf{ctx}}
\qquad
\rule{\mathsf{ext}}{
\Gamma \ \mathsf{ctx}
\qquad
\Gamma \vdash A \ \mathsf{type}
}
{
(\Gamma , x \overset{\sigma}{:} A) \ \mathsf{ctx}
}
$$
**TODO**: need to reflect on how to introduce the judgement $\Gamma \vdash A\ \mathsf{type}$, the well-formed types. This may change the way of presenting formation rules, as the first ones below.
## Checking rules
This section mainly refers to the construction of checkable terms in the
@ -236,8 +280,8 @@ conclusion.
- [x] Lam
- [x] TensorType
- [x] TensorIntro
- [ ] UnitType
- [ ] Unit
- [x] UnitType
- [x] Unit
- [ ] SumType
@ -246,9 +290,12 @@ conclusion.
**Formation rule**
$$\begin{gathered}
$$
\rule{}{\Gamma \ \mathsf{ctx} }{\Gamma \vdash \mathcal{U} \ \mathsf{type}}
\qquad
\begin{gathered}
\rule{Univ{\Leftarrow}}{
0\cdot \Gamma \vdash
0\cdot \Gamma \ \mathsf{ctx}
}{
0\cdot \Gamma \vdash \mathcal{U}\, \overset{0}{\color{red}\Leftarrow}\,\, \mathcal{U}
}
@ -260,11 +307,17 @@ $$
**Formation rule**
$$\begin{gathered}
$$
\rule{}{\Gamma \ \mathsf{ctx}
\qquad \Gamma \vdash A \ \mathsf{type}
\qquad (\Gamma , x \overset{\sigma}{:} A) \vdash B(x) \ \mathsf{type}
}{\Gamma \vdash (x \overset{\sigma}{:} A) \to B \ \ \mathsf{type}}
\\
\begin{gathered}
\rule{Pi{\Leftarrow}}{
0\cdot \Gamma \vdash A \, \overset{0}{\color{red}\Leftarrow}\,\mathcal{U}
\qquad
0\cdot \Gamma,\,x\overset{0}{:}A \vdash B \, \overset{0}{\color{red}\Leftarrow}\,\mathcal{U}\quad
(0\cdot \Gamma,\,x\overset{0}{:}A)\vdash B \, \overset{0}{\color{red}\Leftarrow}\,\mathcal{U}\quad
}{
0\cdot \Gamma \vdash (x\overset{\pi}{:}A)\rightarrow B \overset{0}{\color{red}\Leftarrow}\mathcal{U}
}
@ -284,7 +337,7 @@ becomes known, and it just remains to check its judgment.
$$\begin{gathered}
\rule{Lam{\Leftarrow}}{
\Gamma, x\overset{\sigma\pi}{:}A \vdash M \,\overset{\sigma}{\color{red}\Leftarrow}\,B
(\Gamma, x\overset{\sigma\pi}{:}A) \vdash M \,\overset{\sigma}{\color{red}\Leftarrow}\,B
}{
\Gamma \vdash \lambda x.M \overset{\sigma}{\color{red}\Leftarrow} (x\overset{\pi}{:}A)\rightarrow B
}
@ -300,7 +353,7 @@ $$\begin{gathered}
\rule{\otimes\mbox{-}{\Leftarrow}}{
0\cdot \Gamma \vdash A \,\overset{0}{\color{red}\Leftarrow}\,\mathcal{U}
\qquad
0\cdot \Gamma, x\overset{0}{:}A \vdash B\overset{0}{\color{red}\Leftarrow}\,\mathcal{U}
(0\cdot \Gamma, x\overset{0}{:}A) \vdash B\overset{0}{\color{red}\Leftarrow}\,\mathcal{U}\quad
}{
0\cdot \Gamma \vdash (x\overset{\pi}{:}A) \otimes B \overset{0}{\color{red}\Leftarrow}\,\mathcal{U}
}
@ -314,11 +367,10 @@ A rule to introduce pairs in QTT appears in [Section 2.1.3 in Atkey's
paper](https://bentnib.org/quantitative-type-theory.pdf). We do present the same
rule in a more a more didactical way but also following the bidirectional
recipe. Briefly, the known rule is splitted in two cases, the erased and present
part of the theory, i.e., respectively, looking at the conclusion. Recall that
forming pairs is the way one introduces values of the tensor product. Then, one
must check the conclusion. After doing this, the types $A$ and $B$ become known
facts and it makes sense to check the types in the premises. The usage bussiness
follows the similar reasoning given for applications.
part of the theory, after studying the usage variable in the conclusion. Recall
that forming pairs is the way one introduces values of the tensor product. One then must check the rule conclusion. After doing this, the types $A$ and $B$ become
known facts and it makes sense to check the types in the premises. The usage
bussiness follows a similar reasoning as infering applications.
$$\begin{gathered}
@ -374,6 +426,35 @@ $$
%
$$
### Unit type
$$
\rule{}{
0 \cdot \Gamma \ \mathsf{ctx}
}{
\Gamma \vdash 1 \ \mathsf{type}
}
\qquad
\rule{1\mbox{-}I}{
0 \cdot \Gamma \ \mathsf{ctx}
}{
\check{0\cdot\Gamma}{1}{0}{\mathcal{U}}
}
\qquad
\rule{*\mbox{-}I}{
0 \cdot \Gamma \ \mathsf{ctx}
}{
\check{0\cdot\Gamma}{*}{0}{1}
}
$$
### Sum type
TODO
### Inductive types
TODO
## Conversion rules
@ -482,11 +563,11 @@ The case of the`Bound` variable throws an error.
$$
\begin{gathered}
\rule{Ann{⇒}}{
0\cdot \Gamma \vdash M\,{\color{red}\Leftarrow}^0\,\mathcal{U}
0\cdot \Gamma \vdash A\,{\color{red}\Leftarrow}^0\,\mathcal{U}
\qquad
\Gamma \vdash x\,{\color{red}\Leftarrow}^\sigma\, M
\Gamma \vdash x\,{\color{red}\Leftarrow}^\sigma\, A
}{
\Gamma \vdash \mathsf{Ann}(x,M)\,{\color{blue}\Rightarrow}^{\sigma}\,M
\Gamma \vdash \mathsf{Ann}(x,A)\,{\color{blue}\Rightarrow}^{\sigma}\,A
}
\end{gathered}
%
@ -494,33 +575,33 @@ $$
Any annotation possess type information that counts as known facts, and we therefore infer. However, this is a choice.
- First, we must check that $M$ is a type, i.e., a term in *some* universe.
- First, we must check that $A$ is a type, i.e., a term in *some* universe.
Because there is only one universe we denote it by $\mathcal{U}$. The formation
rule for types has no computation content, then the usage is zero in this case.
- Second, the term $x$ needs to be checked against $M$ using the same usage
- Second, the term $x$ needs to be checked against $A$ using the same usage
$\sigma$ we need in the conclusion. The context for this is $\Gamma$. There is
one issue here. This type checking expects $M$ to be in normal form. When it is
not, typechecking the judgment $\Gamma \vdash x \Leftarrow^\sigma M$ may give us
one issue here. This type checking expects $A$ to be in normal form. When it is
not, typechecking the judgment $\Gamma \vdash x \Leftarrow^\sigma A$ may give us
a false negative.
- *Example*: Why do we need $M'$? Imagine that we want to infer the type of $v$ given $\Gamma \vdash x : \mathsf{Ann}(v, \mathsf{Vec}(\mathsf{Nat},2+2))$. Clearly, the answer should be `Vec(Nat,4)`.
- *Example*: Why do we need $A'$? Imagine that we want to infer the type of $v$ given $\Gamma \vdash x : \mathsf{Ann}(v, \mathsf{Vec}(\mathsf{Nat},2+2))$. Clearly, the answer should be `Vec(Nat,4)`.
However, this reasoning step requires computation. $$\Gamma \vdash x : \mathsf{Ann}(v, \mathsf{Vec}(\mathsf{Nat},2+2)) \Rightarrow \mathsf{Vec}(\mathsf{Nat},4))\,.$$
- Using $M'$ as the normal form of $M$, it remains to check if $x$ is of type
$M'$. If so, the returning type is $M'$ and the resources map has to be updated
- Using $M'$ as the normal form of $A$, it remains to check if $x$ is of type
$A'$. If so, the returning type is $A'$ and the table resources has to be updated
(the $\color{gray}{gray}$ $\Theta$ in the rule below).
$$
\begin{gathered}
\rule{Ann{⇒}}{
0\cdot \Gamma \vdash M \Leftarrow^0 \mathcal{U}
\check{0\cdot \Gamma}{A}{0}{\mathcal{U}}
\qquad
M \rightsquigarrow M'
A \color{green}{\rightsquigarrow} A'
\qquad
\Gamma \vdash x \Leftarrow^\sigma M' \color{darkgrey}{\dashv \Theta}
\check{\Gamma}{x}{\sigma}{A'} \color{darkgrey}{\dashv \Theta}
}{
\Gamma \vdash \mathsf{Ann}(x,M) \Rightarrow^{\sigma} M'
\color{darkgrey}{\dashv \Theta}
\infer{\Gamma}{\mathsf{Ann}(x,A)}{\sigma}{A'}
\color{darkgrey}{\dashv \Theta}
}
\end{gathered}
%
@ -540,20 +621,20 @@ infer _ (Ann termX typeM) = do
**Elimination rule**
Recall the task is to find $M$ in $\Gamma \vdash \mathsf{App}(f,x) :^{\sigma}
M$. If we follow the bidirectional type-checking recipe, then it makes sense to
Recall the task is to find $A$ in $\Gamma \vdash \mathsf{App}(f,x) :^{\sigma}
A$. If we follow the bidirectional type-checking recipe, then it makes sense to
infer the type for an application, i.e., $\Gamma \vdash \mathsf{App}(f,x)
\Rightarrow^{\sigma} M$. An application essentially removes a lambda abstraction
\Rightarrow^{\sigma} A$. An application essentially removes a lambda abstraction
introduced earlier in the derivation tree. The rule for this inference case is a
bit more settle, especially because of the usage variables.
To introduce the term of an application, $\mathsf{App}(f,x)$, it requires to
give/have a judgement saying that $f$ is a (dependent) function, i.e., $\Gamma
\vdash f :^{\sigma} (x : ^\pi A) \to B$, for usages variables $\sigma$ and
\vdash f \overset{\sigma}{:} (x \overset{\pi}{:} A) \to B$, for usages variables $\sigma$ and
$\pi$. Then, given $\Gamma$, the function $f$ uses $\pi$ times its input,
mandatory. We therefore need $\sigma\pi$ resources of an input for $f$ if we
want to apply $f$ $\sigma$ times, as in the conclusion $\Gamma \vdash
\mathsf{App}(f,x) \Rightarrow^{\sigma} M$.
\mathsf{App}(f,x) \Rightarrow^{\sigma} A$.
In summary, the elimination rule is often presented as follows.
@ -578,6 +659,8 @@ $$\begin{gathered}
\Gamma \vdash f {\color{blue}\Rightarrow}^{\sigma}(x : ^\pi A) \to B
\qquad
\sigma\pi\cdot\Gamma' \vdash x {\color{red}\Leftarrow}^{\sigma\pi} A
\qquad
\color{gray}{0 \cdot \Gamma = 0 \cdot \Gamma'}
}{
\Gamma + \sigma\pi\cdot\Gamma' \vdash \mathsf{App}(f,x) \,{\color{blue}\Rightarrow^{\sigma}}\, B
}
@ -590,12 +673,12 @@ emphasising the usage bussiness.
1. $$\begin{gathered}
\rule{App{\Rightarrow_1}}{
\Gamma \vdash f {\color{blue}\Rightarrow^{\sigma}} (x :^{\pi} A) \to B
\qquad
\color{green}{\sigma \cdot \pi = 0}
\qquad
\Gamma \vdash f {\color{blue}\Rightarrow^{\sigma}} (x :^{\pi} A) \to B
\qquad
0\cdot \Gamma \vdash x {\color{red}\Leftarrow^{0}} A
\quad
\qquad
}{
\infer{\Gamma}{\mathsf{App}(f,x)}{\sigma}{B}
}
@ -605,11 +688,13 @@ $$
2. $$\begin{gathered}
\rule{App{\Rightarrow_2}}{
\infer{\Gamma_1}{f}{\sigma}{(x :^{\pi} A) \to B}
\quad
\color{green}{\sigma \cdot \pi \neq 0}
\quad
\qquad
\infer{\Gamma_1}{f}{\sigma}{(x :^{\pi} A) \to B}
\qquad
\check{\Gamma_2}{x}{1}{A}
\qquad
\color{gray}{0 \cdot \Gamma_1 = 0 \cdot \Gamma_2}
\quad
}{
\infer{\Gamma_1 + \sigma \pi\cdot \Gamma_2}{\mathsf{App}(f,x)}{\sigma}{B}
@ -642,8 +727,8 @@ infer σ (App f x) = do
In the rules above, we have the lemma:
- $1 \cdot \Gamma \vdash x :^1 M$ entails that $\rho \cdot \Gamma \vdash x
:^\rho M$ for any usage $\rho$.
- $1 \cdot \Gamma \vdash x :^1 A$ entails that $\sigma \cdot \Gamma \vdash x
:^\sigma A$ for any usage $\sigma$.
## Tensor type
@ -656,23 +741,26 @@ type. In our case, the principal judgemente shows up in the first premise, which
is the fact that $M$ is a tensor product type. If we infer that, the types $A$
and $B$ become known facts.
TODO: use notebooks write up
$$\begin{gathered}
\rule{TensorElim{\Rightarrow}}{
\Gamma_{1} \vdash M \,\overset{\sigma}{\color{blue}\Rightarrow}\,(x\overset{\pi}{:}A)\otimes B
\infer{\Gamma_{1}}{M}{\sigma}{(x\overset{\pi}{:}A)\otimes B}
\\
0\cdot \Gamma_{1},z\overset{0}{:}(x\overset{\pi}{:}A)\otimes B \vdash C \,\overset{0}{\color{red}\Leftarrow}\,\mathcal{U}
\qquad
\Gamma_{2},x\overset{\sigma\pi}{:}A, y\overset{\sigma}{:}B\vdash N \overset{\sigma}{\color{red}{\Leftarrow}}C[(x,y)/z]\qquad
\check{(0\cdot \Gamma_{1},z\overset{0}{:}(x\overset{\pi}{:}A)\otimes B)}{C}{0}{\mathcal{U}}
\\
\check{\Gamma_{2}, u \overset{\sigma\pi}{:} A, v\overset{\sigma}{:}B}{%
N}{\sigma}{C[(x,y)/z]}
}{
\Gamma_{1}+\Gamma_{2} \vdash \mathrm{let}\,z@(x,y)=M\,\,\mathrm{in}\,\,N :C \overset{\sigma}{\color{blue}\Rightarrow}\, C[M/x]
\Gamma_{1}+\Gamma_{2} \vdash \mathsf{let}\,z@(u,v)=M\,\,\mathsf{in}\,\,N :C \overset{\sigma}{\color{blue}\Rightarrow}\, C[M/x]
}
\end{gathered}
%
$$
TODO: I need the syntax "let" as we need pattern-matching to make sure one uses all the components in the pair. Exactly the same situation occurs in linear logic, which actually inspires this rule.
Inspired by the tensor product rules in linear logic, there is a need to
decompose a pair in its components. We have to be sure that all the resources in
each component are effectively used. Then, such a mechanism needs to be introduced, using the keyword $\mathsf{let}\mbox{-}\mathsf{in}$.
## Sum type elim