From 75d164c8736493a5b029fa7675884f2de2318dc2 Mon Sep 17 00:00:00 2001
From: regnat <rg@regnat.ovh>
Date: Tue, 25 Apr 2017 08:53:28 +0200
Subject: [PATCH] Add type annotations for lambdas and let-recs

Those were already present in the typing rules, they are now added in
the syntax and the semantics

Fixes #5
---
 common/header.tex       |  2 +-
 grammar/expressions.tex |  4 ++--
 grammar/values.tex      |  2 +-
 semantics/semantics.tex | 11 ++++++-----
 4 files changed, 10 insertions(+), 9 deletions(-)

diff --git a/common/header.tex b/common/header.tex
index 40c5258..61297ff 100644
--- a/common/header.tex
+++ b/common/header.tex
@@ -82,7 +82,7 @@
 \newcommand{\ofTypeP}[2]{\UseCollection{xfrac}{plainmath}\sfrac{#1}{#2}}
 
 \newcommand{\Γ}{\Gamma}
-\newcommand{\τ}{\tau}
+\newcommand{\τ}{\ensuremath{\tau}}
 \newcommand{\σ}{\sigma}
 \newcommand{\λ}{\lambda}
 \newcommand{\recleq}{\sqsubsetleq}
diff --git a/grammar/expressions.tex b/grammar/expressions.tex
index 2bb4b9a..45e5991 100644
--- a/grammar/expressions.tex
+++ b/grammar/expressions.tex
@@ -3,12 +3,12 @@
   <e> ::=
     \x/ \| \c/
     \alt \e/.\a/ \| \e/.\a/ or \e/
-    \alt $\λ$\p/.\e/ \| \e/ \e/
+    \alt $\λ$\p/:\τ.\e/ \| \e/ \e/
     \alt \{ \e/ = \e/ \}
     \alt with \e/; \e/
     \alt (\x/ := \e/ $\bm{\in}$ \t/) ? \e/ : \e/
     \alt let \x/ = \e/; $\cdots{}$; \x/ = \e/; in \e/
-    \alt let rec \x/ = \e/; $\cdots{}$; \x/ = \e/; in \e/
+    \alt let rec \x/:\τ = \e/; $\cdots{}$; \x/:\τ/ = \e/; in \e/
     \alt \o/
 
     <o> ::= attrNames(\e/) \| listToAttrs(\e/)
diff --git a/grammar/values.tex b/grammar/values.tex
index 39b6ab9..9d79a9f 100644
--- a/grammar/values.tex
+++ b/grammar/values.tex
@@ -3,7 +3,7 @@
 
   <v> ::=
     \c/
-    \alt $\λ$\p/.\e/
+    \alt $\λ$\p/:\τ.\e/
     \alt \{ \v/ = \e/ \} $\orthplus \cdots{} \orthplus$ \{ \v/ = \e/ \}
     \alt Cons(\e/, \e/) \| nil
 \end{grammar}
diff --git a/semantics/semantics.tex b/semantics/semantics.tex
index 302d643..950974e 100644
--- a/semantics/semantics.tex
+++ b/semantics/semantics.tex
@@ -10,8 +10,8 @@ figure~\pref{fig:semantics:nix-light:patterns}
     \dstepa{\{ \s/ = \e/; $\ldots{}$\}.\s/}{$e$}{}
     \dstepa{\{ \s/ = \e/; $\ldots{}$\}.\s/ or $e'$}{$e$}{}
     \dstepa{$v.s \text{ or } e'$}{$e'$}{if $\v/ \neq$ \{ \s/ = \e/; $\ldots{}$ \}}
-    \dstepa{$(\λ x.e_1) e_2$}{$\substp{x}{e_2}{e_1}$}{}
-    \dstepa{$(\λ p.e_1) v$} {$\substp{p}{v}{e_1}$}{if $p \neq x$}
+    \dstepa{$(\λ x : \τ .e_1) e_2$}{$\substp{x}{e_2}{e_1}$}{}
+    \dstepa{$(\λ p : \τ .e_1) v$} {$\substp{p}{v}{e_1}$}{if $p \neq x$}
     \dstepa{with \{ $l_1$ = $e_1$; $\cdots{}$; $l_n$ = $e_n$; \} ; \e/}{
       \e/[\assign{l_1}{\eone}; ...; \assign{l_n}{\en}]
     }{}
@@ -21,12 +21,13 @@ figure~\pref{fig:semantics:nix-light:patterns}
     \dstepa{let \xone = \eone; $\cdots{}$; \xn = \en; in \e/}{%
       \e/[\assign{x_1}{\eone}; ...; \assign{x_n}{\en}]
     }{}
-    \dstepa{let rec $x$ = $e$; in $e'$}{%
+    \dstepa{let rec $x$ : $\τ$ = $e$; in $e'$}{%
       \subst{x}{\text{let $x$ = $e$; in $x$}}{$e'$}
     }{}
-    \dstepa{let rec \xone = \eone; $\cdots{}$; \xn = \en; in \e/}{%
+    \dstepa{let rec \xone : $\τ_1$ = \eone; $\cdots{}$; \xn : $\τ_n$ = \en; in \e/}{%
       \parbox[t]{10cm}{%
-        (let rec $r$ = \{ $x'_1$ = \eone; \} $\orthplus \cdots \orthplus$ \{ $x'_n$ = \en \}; in e)
+        (let rec $r$ : \{ $x'_1$ = $\τ_1$; $\cdots$; $x'_n$ = $\τ_n$; \} = \\
+        \{ $x'_1$ = \eone; $\cdots$; $x'_n$ = \en \}; in e)
       [ \\ \assign{\xone}{r.x'_1}; \ldots{}; \assign{\xn}{r.x'_n} \\ ]
       }
     }{}