14 files changed, 261 insertions, 32 deletions

diff --git a/lambda-calcul/rust/README.md b/lambda-calcul/rust/README.md
index 08dfc3d..4150393 100644
--- a/lambda-calcul/rust/README.md
+++ b/lambda-calcul/rust/README.md
@@ -26,7 +26,7 @@ We use the following variables to represent, well, variable elements that should
 The client needs to send a `POST /register` request, passing in as payload a JSON object with a `url` and `name` string fields:
 
 ```
-curl -v -X POST -d '{"url":"${CLIENT_URL}", "name": "toto", "encoding": "Json"}' -H 'Content-type: application/json' ${SERVER_BASE_URL}/register
+curl -v -X POST -d '{"url":"${CLIENT_URL}", "name": "toto", "encoding": "Json"}scra' -H 'Content-type: application/json' ${SERVER_BASE_URL}/register
 ```
 
 The payload is expected to be a JSON object with the following fields:
@@ -69,20 +69,38 @@ There are `--port` and `--host` arguments should one want to change the default
 * [x] make command line to register more explicit
 * [x] `nc -l` is a simple echo server to show what's sent by the server
 * [x] keep the readme exposed by the server
-* [ ] use JSON formatting for request/response
+* [x] use JSON formatting for request/response
 * [ ] debug user address on the leaderboard page
   * [ ] shows status of client (not connected/connected/replying correctly or not)
 * [ ] add more logs to server to help troubleshoot users access/registration
 * [ ] THE SERVER MUST NOT CRASH
 * [ ] cheatsheet λ-calcul exposed on `/help`
-* [ ] propose to send JSON or S-Exp
+* [x] propose to send JSON or S-Exp
 * [ ] persist user state to avoid losing connections
 * [ ] deploy automatically server on punkachien.net with radicle CI
 * [ ] better JSON representation for AST than raw serde stuff
+  * could be just an array?
 * [ ] Document JSON format...
+* [ ] warn about local firewall on the machine
+* [ ] add both representations to query
+* [ ] add simple arithmetic expressions
+* [ ] collect interesting examples and tests (instead of generating them randomly)
+  * would be easy to generate more examples by substituting values inside predefined expressions
+* [ ] add flag in REPL to set/unset syntactic sugar
 
 * [ ] ask people to implement something
 * [ ] prepare starter kit to overcome
 * [ ] différentes couleurs de pistes (verte/rouge/noire)
 * [ ] pair programming w/ Manu, people do their own stuff if they want
 * [ ] ne pas oublier le routeur wifi
+
+3 steps:
+1. write interpreter
+2. play with interpreter
+3. introduce types
+
+* there's no semantics intrisically attached to the expressions, it's _us_ who define it
+  * example of snd/fst whose behaviour can also be head/tail or bool/false
+
+* example of `λ x y. x` which can be `fst`, `True`,  or `head`
+* write `reverse`?
diff --git a/lambda-calcul/rust/proptest-regressions/types.txt b/lambda-calcul/rust/proptest-regressions/types.txt
new file mode 100644
index 0000000..1641140
--- /dev/null
+++ b/lambda-calcul/rust/proptest-regressions/types.txt
@@ -0,0 +1,7 @@
+# Seeds for failure cases proptest has generated in the past. It is
+# automatically read and these particular cases re-run before any
+# novel cases are generated.
+#
+# It is recommended to check this file in to source control so that
+# everyone who runs the test benefits from these saved cases.
+cc 2dfe9e2164ba8175f480aa813e5e441fa85a683ecd7a30d18fbc38777f9ed425 # shrinks to n = Num(0)
diff --git a/lambda-calcul/rust/src/ast.rs b/lambda-calcul/rust/src/ast.rs
index bdfb963..2b9bcfc 100644
--- a/lambda-calcul/rust/src/ast.rs
+++ b/lambda-calcul/rust/src/ast.rs
@@ -14,7 +14,11 @@ pub enum Type {
 
 impl Display for Type {
     fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
-        write!(f, "Type")
+        match self {
+            Type::Num => write!(f, "Num"),
+            Type::Bool => write!(f, "Bool"),
+            Type::Arr(l, r) => write!(f, "({} -> {})", l, r),
+        }
     }
 }
 
@@ -39,7 +43,7 @@ pub enum Value {
     // this is unsound as we are not in a dependently typed language
     // but useful to unify external representation (AST). In theory,
     // we should separate AST from Terms
-    Type(Type)
+    Type(Type),
 }
 
 use Value::*;
@@ -76,7 +80,7 @@ impl Display for Value {
             Value::Lam(var, body) => write!(f, "(lam {} {})", var, body),
             Value::Def(var, value) => write!(f, "(def {} {})", var, value),
             Value::Let(var, value, body) => write!(f, "(let ({} {}) {})", var, value, body),
-            Value::TLam(var,typ, body) => write!(f, "(tlam ({} {}) {})", var, typ, body),
+            Value::TLam(var, typ, body) => write!(f, "(tlam ({} {}) {})", var, typ, body),
             Value::Type(typ) => write!(f, ":{}", typ),
         }
     }
diff --git a/lambda-calcul/rust/src/builtins.rs b/lambda-calcul/rust/src/builtins.rs
new file mode 100644
index 0000000..7064c1c
--- /dev/null
+++ b/lambda-calcul/rust/src/builtins.rs
@@ -0,0 +1,25 @@
+use crate::ast::Value;
+use std::collections::HashMap;
+
+pub struct Builtins {}
+
+impl Builtins {
+    pub fn new() -> HashMap<String, Value> {
+        let mut map = HashMap::new();
+        map.insert("+".to_string(), Value::Prim("+".to_string()));
+        map
+    }
+}
+
+pub fn plus(v: Value) -> Value {
+    match v {
+        Num(i) => Lam(gensym(),
+    }
+}
+
+pub fn builtins(sym: &String) -> Option<Box<dyn Fn(Value) -> Value>> {
+    match sym.as_str() {
+        "+" => Some(Box::new(plus)),
+        _ => None,
+    }
+}
diff --git a/lambda-calcul/rust/src/io.rs b/lambda-calcul/rust/src/io.rs
index 8c628ba..4e5fb59 100644
--- a/lambda-calcul/rust/src/io.rs
+++ b/lambda-calcul/rust/src/io.rs
@@ -21,6 +21,7 @@ pub fn eval_file(file_name: &str) -> String {
 
 pub fn batch_eval<I: Read, O: Write>(inp: &mut I, outp: &mut O) {
     let mut env = Environment::new();
+    let mut context = Environment::new();
     let mut reader = BufReader::new(inp);
     loop {
         let mut input = String::new();
@@ -36,7 +37,7 @@ pub fn batch_eval<I: Read, O: Write>(inp: &mut I, outp: &mut O) {
         let values = parse(&input);
         let results = values
             .iter()
-            .map(|v| eval_whnf(v, &mut env))
+            .map(|v| eval_whnf(v, &mut env, &mut context))
             .collect::<Vec<Value>>();
         for result in results {
             writeln!(outp, "{}", result).unwrap();
@@ -47,6 +48,7 @@ pub fn batch_eval<I: Read, O: Write>(inp: &mut I, outp: &mut O) {
 
 pub fn repl<I: Read, O: Write>(inp: &mut I, outp: &mut O) {
     let mut env = Environment::new();
+    let mut context = Environment::new();
     let mut reader = BufReader::new(inp);
     loop {
         let mut input = String::new();
@@ -63,7 +65,7 @@ pub fn repl<I: Read, O: Write>(inp: &mut I, outp: &mut O) {
         let values = parse(&input);
         let results = values
             .iter()
-            .map(|v| eval_whnf(v, &mut env))
+            .map(|v| eval_whnf(v, &mut env, &mut context))
             .collect::<Vec<Value>>();
         for result in results {
             writeln!(outp, "{}", result).unwrap();
diff --git a/lambda-calcul/rust/src/lambda.rs b/lambda-calcul/rust/src/lambda.rs
index ea571fd..80f2d5c 100644
--- a/lambda-calcul/rust/src/lambda.rs
+++ b/lambda-calcul/rust/src/lambda.rs
@@ -1,3 +1,4 @@
+use log::debug;
 use proptest::{
     arbitrary::any,
     prelude::*,
@@ -50,7 +51,11 @@ impl<'a, T: Clone> Default for Environment<'a, T> {
 
 pub fn eval_all(values: &[Value]) -> Vec<Value> {
     let mut env = Environment::new();
-    values.iter().map(|v| eval_whnf(v, &mut env)).collect()
+    let mut context = Environment::new();
+    values
+        .iter()
+        .map(|v| eval_whnf(v, &mut env, &mut context))
+        .collect()
 }
 
 /// Reduce the given value to weak head normal form using call-by-name
@@ -58,8 +63,13 @@ pub fn eval_all(values: &[Value]) -> Vec<Value> {
 ///
 /// call-by-name reduces the leftmost outermost redex first, which is
 /// not under a lambda abstraction.
-pub fn eval_whnf(arg: &Value, env: &mut Environment<Value>) -> Value {
-    match arg {
+pub fn eval_whnf(
+    arg: &Value,
+    env: &mut Environment<Value>,
+    context: &mut Environment<Type>,
+) -> Value {
+    debug!("evaluating {}", arg);
+    let result = match arg {
         Value::Def(var, value) => {
             env.bind(var, value);
             Value::Bool(true) // TODO: return a more meaningful value?
@@ -67,19 +77,26 @@ pub fn eval_whnf(arg: &Value, env: &mut Environment<Value>) -> Value {
         Value::Let(var, value, expr) => {
             let mut newenv = env.extends();
             newenv.bind(var, value);
-            eval_whnf(expr, &mut newenv)
+            eval_whnf(expr, &mut newenv, context)
         }
-        Value::App(l, r) => match eval_whnf(l, env) {
-            Value::Lam(v, body) => eval_whnf(&subst(&v, &body, r), env),
-            Value::Sym(var) => match env.lookup(&var) {
-                Some(val) => eval_whnf(&Value::App(Box::new(val.clone()), r.clone()), env),
-                None => arg.clone(),
+        Value::App(l, r) => match eval_whnf(l, env, context) {
+            Value::Lam(v, body) => eval_whnf(&subst(&v, &body, r), env, context),
+            Value::Sym(var) => match var.as_str() {
+                ":type-of" => type_of(r, context).map(Value::Type).unwrap(),
+                _ => match env.lookup(&var) {
+                    Some(val) => {
+                        eval_whnf(&Value::App(Box::new(val.clone()), r.clone()), env, context)
+                    }
+                    None => arg.clone(),
+                },
             },
             other => Value::App(Box::new(other), r.clone()),
         },
         Value::Sym(var) => env.lookup(var).unwrap_or(arg).clone(),
         other => other.clone(),
-    }
+    };
+    debug!("evaluated to {}", result);
+    result
 }
 
 fn subst(var: &str, body: &Value, e: &Value) -> Value {
@@ -234,21 +251,25 @@ fn gen_terms(u: u32) -> impl Strategy<Value = Value> {
 
 #[cfg(test)]
 mod lambda_test {
-    use crate::{ast::Type, parser::parse};
-
     use super::{eval_all, eval_whnf, type_of, Environment, Value};
+    use crate::{ast::Type, lambda::gen_terms, parser::parse};
+    use proptest::{
+        prelude::*,
+        strategy::{Strategy, ValueTree},
+        test_runner::TestRunner,
+    };
 
     fn parse1(string: &str) -> Value {
         parse(string).pop().unwrap()
     }
 
     fn eval1(value: &Value) -> Value {
-        eval_whnf(value, &mut Environment::new())
+        eval_whnf(value, &mut Environment::new(), &mut Environment::new())
     }
 
     #[test]
     fn evaluate_symbol_starting_with_x_returns_same_symbol() {
-        let sym= "x1xYgddw7";
+        let sym = "x1xYgddw7";
 
         let value = parse1(sym);
         assert_eq!(value, eval1(&value));
@@ -308,6 +329,11 @@ mod lambda_test {
     }
 
     #[test]
+    fn type_of_returns_type_of_expression() {
+        let value = parse1("(:type-of 11)");
+        assert_eq!(Value::Type(Type::Num), eval1(&value));
+    }
+    #[test]
     fn defined_symbols_are_evaluated_to_their_definition() {
         let values = parse("(def foo 12)  foo");
         assert_eq!(vec![Value::Bool(true), Value::Num(12)], eval_all(&values));
@@ -375,4 +401,23 @@ mod lambda_test {
 
         assert_eq!(Type::Arr(Box::new(Type::Num), Box::new(Type::Num)), ty);
     }
+
+    #[test]
+    fn any_terms() {
+        let mut runner = TestRunner::default();
+        for i in 0..100 {
+            let value = any::<u32>()
+                .prop_flat_map(gen_terms)
+                .new_tree(&mut runner)
+                .unwrap()
+                .current();
+            let evaluation = eval1(&value);
+            println!(
+                "{} term: {}, evaluation: {}",
+                value == evaluation,
+                value,
+                evaluation
+            );
+        }
+    }
 }
diff --git a/lambda-calcul/rust/src/web.rs b/lambda-calcul/rust/src/web.rs
index 7dae468..7345d0f 100644
--- a/lambda-calcul/rust/src/web.rs
+++ b/lambda-calcul/rust/src/web.rs
@@ -130,18 +130,18 @@ impl Client {
             self.generate_exprs()
         } else {
             let input = generate_expr(self.grade.into(), &mut self.runner);
-            let expected = eval_whnf(&input, &mut Environment::new());
+            let expected = eval_whnf(&input, &mut Environment::new(), &mut Environment::new());
             (vec![input], vec![expected])
         }
     }
 
     fn generate_expression_to_type(&mut self) -> (Vec<Value>, Vec<Value>) {
         let input =
-            generate_expression_to_type((self.grade - Self::TYPING_GRADE).into(), &mut self.runner);
-        let expected = type_of_all(&input)
-            .iter()
-            .map(|t| Value::Type(t.clone()))
-            .collect();
+            generate_expression_to_type((self.grade - Self::TYPING_GRADE).into(), &mut self.runner)
+                .into_iter()
+                .map(|e| Value::App(Box::new(Value::Sym(":type-of".to_string())), Box::new(e)))
+                .collect::<Vec<_>>();
+        let expected = eval_all(&input);
         (input, expected)
     }
 
@@ -273,6 +273,7 @@ async fn eval(input: String) -> impl Responder {
     let exprs = parse_total(&input);
     match exprs {
         Ok(exprs) => {
+            // Occasionally return a random symbol to keep clients on their toes
             let mut rng = rand::thread_rng();
             if rng.gen_range(0..10) <= 2 {
                 return HttpResponse::Ok().body(gensym());
@@ -392,7 +393,10 @@ fn apply_result(
 ) {
     let mut client = client_m.lock().unwrap();
     let test = client.check_result(&expected, &response);
-    info!("result for {} = {:?}, expected {:?}", client.url, test, expected);
+    info!(
+        "result for {} = {:?}, expected {:?}",
+        client.url, test, expected
+    );
     client.apply(&test);
 }
 
diff --git a/lambda-calcul/rust/static/README.md b/lambda-calcul/rust/static/README.md
new file mode 100644
index 0000000..08dfc3d
--- /dev/null
+++ b/lambda-calcul/rust/static/README.md
@@ -0,0 +1,88 @@
+# Rust λ-calcul reference implementation
+
+This directory contains a reference implementation of a normal order semantics λ-calculus based language.
+Current syntax is based on S-expressions, ie. Lisp. There is a command-line interpreter for batch and interactive evaluation of input, and an embryonic tester daemon.
+
+# Tester
+
+The tester daemon is inspired by [Extreme Startup](https://github.com/rchatley/extreme_startup): It's a REST-ish server and client that allows to repeatedly send λ-terms to a remote execution engine and compare the result against its expectations.
+
+The overall interaction flow is the following:
+
+* HTTP server starts on some known port (eg. 8080)
+* Clients register themselves with the server
+* Server registers client and starts sending expressions to evaluate
+* Leaderboard is updated depending on whether clients' answers are correct or not
+
+## Detailed Interactions
+
+We use the following variables to represent, well, variable elements that should be replaced depending on the actual deployment:
+
+* `SERVER_BASE_URL`: the base URL of the server, should be communicated by facilitator in some ways, eg. `http://1.2.3.4:8080`,
+* `CLIENT_URL`: URL of a client as defined by their specific implementation.
+
+### Registration
+
+The client needs to send a `POST /register` request, passing in as payload a JSON object with a `url` and `name` string fields:
+
+```
+curl -v -X POST -d '{"url":"${CLIENT_URL}", "name": "toto", "encoding": "Json"}' -H 'Content-type: application/json' ${SERVER_BASE_URL}/register
+```
+
+The payload is expected to be a JSON object with the following fields:
+* `url`: The client URL for the server to callback and send expressions to evaluate
+* `name`: The name of this client
+* _(Optional)_ `encoding`: Which encoding to use to receive expressions and send responses. One of `Json` or `Sexp`, defaulting to `Json`.
+
+Notes:
+
+* Obviously, client needs to start a HTTP server able to respond to a `GET` request at the given URL. To check or troubleshoot connectivity, one can use the [netcat](https://linux.die.net/man/1/nc) program to fire up a local server with `nc -l 12345` and use the ip and port to register the client. This will echo in the terminal whatever the _server_ sends
+* If URL is not already registered, server accepts the registration (returning a `200 OK` result) and starts a _testing thread_
+
+* The _tester_ then repeatedly sends `POST` requests to the client's registered URL
+  * The body of the request is plain text S-expression representing a λ-term
+  * The tester expects the response to be the plain text result of the evaluation of those terms
+* If the client fails to answer, or answers wrongly, the server keeps sending the same request
+* If the client's answer is correct, the server sends another term to evaluate and awards 1 point to the client
+* The `/leaderboard` endpoint provides a crude HTML page listing each clients' current score
+
+## Building
+
+This software is written in Rust (sorry @xvdw), so one needs a Rust toolchain installed, then:
+
+```
+cargo build && cargo test
+```
+
+## Running
+
+To run the server:
+
+```
+cargo run --bin server
+```
+
+There are `--port` and `--host` arguments should one want to change the default `127.0.0.1:8080`
+
+# NOTES
+
+* [x] make command line to register more explicit
+* [x] `nc -l` is a simple echo server to show what's sent by the server
+* [x] keep the readme exposed by the server
+* [ ] use JSON formatting for request/response
+* [ ] debug user address on the leaderboard page
+  * [ ] shows status of client (not connected/connected/replying correctly or not)
+* [ ] add more logs to server to help troubleshoot users access/registration
+* [ ] THE SERVER MUST NOT CRASH
+* [ ] cheatsheet λ-calcul exposed on `/help`
+* [ ] propose to send JSON or S-Exp
+* [ ] persist user state to avoid losing connections
+* [ ] deploy automatically server on punkachien.net with radicle CI
+* [ ] better JSON representation for AST than raw serde stuff
+* [ ] Document JSON format...
+
+* [ ] ask people to implement something
+* [ ] prepare starter kit to overcome
+* [ ] différentes couleurs de pistes (verte/rouge/noire)
+* [ ] pair programming w/ Manu, people do their own stuff if they want
+* [ ] ne pas oublier le routeur wifi
diff --git a/lambda-calcul/support/2025-10-09.md b/lambda-calcul/support/2025-10-09.md
new file mode 100644
index 0000000..66ec5a8
--- /dev/null
+++ b/lambda-calcul/support/2025-10-09.md
@@ -0,0 +1,35 @@
+---
+title: λ-Nantes Workshop 2bis
+subtitle: Apprenons à aimer le λ-calcul simplement typé
+date: 2025-10-09
+---
+
+## Agenda
+
+* Introduction
+* Action
+* Conclusion
+
+# Introduction
+
+## Rappel de l'épisode précédent
+
+* On a codé un λ-calcul non typé en Rust, Elixir, Clojure et Java
+* En jouant contre un serveur nous envoyant des expressions à évaluer
+* On s'est bien amusé
+* On veut aller plus loin
+
+## Rappel de l'épisode précédent
+
+Pour accéder au repository, c'est par là ⇒
+
+![Lambda-Nantes code](qrcode.jpg)
+
+## Aujourd'hui
+
+* On passe à la vitesse supérieure en ajoutant des types simples au λ-calcul
+* Cela donne le _λ-calcul simplement typé_
+
+## Aujourd'hui
+
+![λ-calcul simplement typé](typing-rules.png)
diff --git a/lambda-calcul/support/2025-10-09.pdf b/lambda-calcul/support/2025-10-09.pdf
new file mode 100644
index 0000000..452217b
--- /dev/null
+++ b/lambda-calcul/support/2025-10-09.pdf
diff --git a/lambda-calcul/support/Makefile b/lambda-calcul/support/Makefile
index 2a45ef1..960c5a0 100644
--- a/lambda-calcul/support/Makefile
+++ b/lambda-calcul/support/Makefile
@@ -1,10 +1,11 @@
-all: 2024-10-10.pdf
+all: 2024-10-10.pdf 2025-10-09.pdf
 
 %.pdf: %.md
 	pandoc -t beamer -f markdown+implicit_figures \
-		-V theme:default -V aspectratio:169 \
+		-i -V theme:default -V aspectratio:169 \
 		--pdf-engine=xelatex \
-		-V monofont='DejaVu Sans Mono' \
+		-V monofont='mononoki' \
+    -V mainfont='mononoki' \
 		$(<) -o $(@)
 
 clean:
diff --git a/lambda-calcul/support/qrcode.jpg b/lambda-calcul/support/qrcode.jpg
new file mode 100644
index 0000000..aa560f2
--- /dev/null
+++ b/lambda-calcul/support/qrcode.jpg
diff --git a/lambda-calcul/support/qrcode.png b/lambda-calcul/support/qrcode.png
new file mode 100644
index 0000000..807d6c1
--- /dev/null
+++ b/lambda-calcul/support/qrcode.png
diff --git a/lambda-calcul/support/typing-rules.png b/lambda-calcul/support/typing-rules.png
new file mode 100644
index 0000000..408ff28
--- /dev/null
+++ b/lambda-calcul/support/typing-rules.png