add summary documentation (still a bit WIP)

.gitignore

@@ -3,6 +3,7 @@
 # SPDX-License-Identifier: CC0-1.0
 
 .#*
+*.pdf
 build
 /haskell/**/dist-newstyle
 /rust/target

docs/main.typ

@@ -0,0 +1,70 @@
+#align(center, text(17pt)[
+  *Yanais \u{2013} linearity and references*
+])
+
+#set par(justify: true)
+#set table(stroke: none)
+#let mbnf = (x) => text(fill: rgb("#0000ff"))[#x]
+#let rsyn = (x) => text(fill: rgb("#ff0000"))[#x]
+
+#v(10pt)
+
+== Idea
+
+The language will have only linear functions (which must "use" their argument exactly once),
+but augmented with (type-checked) references, which allow to temporarily escape from linearity,
+but only allow read-only access to data. Not providing mutable references (at least for now)
+was an important decision, because the design is complex enough as is and mutable references
+are really hard to get right (just look at the theoretical background of Rust for some complications).
+
+In order to allow good expressivity, the language is also dependently typed. This complicates
+stuff quite a bit. But it is interesting to look at the interaction of these three base
+"paradigm features". In order to not make dependent typing too complicated, the linearity
+condition only needs to hold in function bodies, but the result side of dependent lambdas
+isn't checked.
+
+== Syntax (frontend)
+
+#table(
+  columns: (auto, auto, auto),
+  align: horizon,
+  [*ident*], [...], [a string of characters according to the Unicode XID rules],
+  [*binder*], [#rsyn(`$`) ident], [binders are identifiers prefixed with a dollar symbol],
+  [(infallible) *pattern*], [binder #mbnf("| (") #rsyn(`[`) #mbnf("(") pattern #mbnf(")") #rsyn(`,`) #mbnf("*") #rsyn(`]`) #mbnf(")")], [a pattern is used to (optionally) destructure data],
+  [*expr*(essions)], [
+    #mbnf("(") #rsyn(`λ`) pattern #mbnf("(") #rsyn(`:`) expr #mbnf(")?") #rsyn(`→`) expr #mbnf(")") \
+  #mbnf("| (") #rsyn(`π`) pattern #rsyn(`:`) expr #rsyn(`→`) expr #mbnf(")") \
+  #mbnf("| (") #rsyn(`&`) ident #mbnf(") | (") #rsyn(`^&`)  ident #mbnf(")") \
+  #mbnf("| (") #rsyn(`@{`) expr #rsyn(`}&`) expr #mbnf(")")
+  ], [],
+)
+
+=== References
+
+#rsyn(`&`) `ident` creates a reference. Its type is #rsyn(`^&`) `ident`. But sometimes we want to return a derived
+reference which is based upon an already existing reference, but has a different inner type (but same lifetime).
+For that case we have #rsyn(`@ { ^&`) `ident` #rsyn(`} &`) `type` (builds a reference with the tag from the reference type in the braces).
+
+== Syntax (middle-end) \"MER\"
+
+The middle-end does some stuff quite a bit different than the frontend.
+
+=== Patterns
+
+Patterns are represented like in the frontend syntax, but their position in the MER is different.
+Lambdas are lowered such that they always bind a single variable.
+Let bindings which just bind to a single variable in full, so don\'t perform any destructuring,
+get replaced with a lambda surrounded by an application.
+Let bindings which don't bind to anything are replaced with a `seq` invocation.
+
+== Linearity and borrow checking
+
+Each binding created incurs the condition that it needs to be used exactly once.
+(with the exception of the result side of dependently typed functions).
+It is possible to create references to a binding, but they can't be used longer than the binding they
+borrow isn't consumed (and it needs to be consumed).
+
+There exist a few escape hooks for this. References and types can be freely duplicated and destroyed.
+And these rules don't apply in the result side of dependently typed functions (but they apply in
+functions invoked by them because the system doesn't have global knowledge if a function only ever
+gets invoked by result sides of dependently typed functions).