Skip to content
Permalink
Browse files

Add comments for sec 8.1-8.3.

  • Loading branch information...
thealmarty committed Aug 16, 2019
1 parent a289486 commit f2e9292895631f2a9ab68a83972dd017e2b31045
Showing with 4 additions and 3 deletions.
  1. +1 −0 .gitattributes
  2. BIN doc/reference/language-reference.pdf
  3. +3 −3 doc/reference/src/core-language.pdc
@@ -1,3 +1,4 @@
*.pdf filter=lfs diff=lfs merge=lfs -text
*.png filter=lfs diff=lfs merge=lfs -text
*.jpg filter=lfs diff=lfs merge=lfs -text
doc/reference/language-reference.pdf filter=lfs diff=lfs merge=lfs -text
Binary file not shown.
@@ -13,14 +13,14 @@ $(R, ⋅)$ is a monoid with identity $1$, multiplication left and right distribu

The core type theory must be instantiated over a particular semiring. Choices include the boolean semiring $(0, 1)$, the zero-one-many semiring $(0, 1, ω)$, and the natural numbers with addition and multiplication.

In canonical Juvix Core the type theory is instantiated over the semiring of natural numbers plus ω, which is the most expressive option — terms can be $0$-usage ("contemplated"), $n$-usage ("computed $n$ times"), or $ω$-usage ("computed any number of times"). \textbf{<- is $ω$ really necessary? What are the use cases for this? We want to add safety via our language and be more precise and descriptive as possible I think. And what do we gain from natural numbers instead of $(0, 1, ω)$? Maybe the ability to specify $n$-usage instead of many?}
In canonical Juvix Core the type theory is instantiated over the semiring of natural numbers plus ω, which is the most expressive option — terms can be $0$-usage ("contemplated"), $n$-usage ("computed $n$ times"), or $ω$-usage ("computed any number of times"). \textbf{<- is $ω$ really necessary? What are the use cases for this? We want to add safety via our language and be as precise and descriptive as possible I think. And what do we gain from natural numbers instead of $(0, 1, ω)$? Maybe the ability to specify $n$-usage instead of many?}

Let $S$ be a set of sorts $(i, j, k)$ with a total order. The typing rule is:

\begin{prooftree}
\AxiomC{}
\RightLabel{SORT j \succ j}
\BinaryInfC{$Γ ⊢_0 *_j \ni *_i $}
\RightLabel{SORT j > j}
\UnaryInfC{$Γ ⊢_0 *_j \ni *_i $}
\end{prooftree}

Let $K$ be the set of primitive types, $C$ be the set of primitive constants, and $⋮$ be the typing relation between primitive constants and primitive types, which must assign to each primitive constant a unique primitive type.

0 comments on commit f2e9292

Please sign in to comment.
You can’t perform that action at this time.