feat: introduce typing of expressions

5 files changed, 75 insertions, 102 deletions

diff --git a/lambda-calcul/rust/src/ast.rs b/lambda-calcul/rust/src/ast.rs
index 0aaeab4..db3b4a7 100644
--- a/lambda-calcul/rust/src/ast.rs
+++ b/lambda-calcul/rust/src/ast.rs
@@ -6,6 +6,22 @@ use serde::{Deserialize, Serialize};
 use std::fmt::{self, Display};
 
 #[derive(Debug, PartialEq, Clone, Serialize, Deserialize)]
+pub enum Type {
+    Int
+}
+
+impl Display for Type {
+    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
+        write!(f, "Type")
+    }
+}
+
+#[derive(Debug, PartialEq, Clone, Serialize, Deserialize)]
+pub enum TypeError {
+    UnknownType(Value),
+}
+
+#[derive(Debug, PartialEq, Clone, Serialize, Deserialize)]
 pub enum Value {
     Num(i32),
     Bool(bool),
@@ -14,6 +30,13 @@ pub enum Value {
     Lam(String, Box<Value>),
     Def(String, Box<Value>),
     Let(String, Box<Value>, Box<Value>),
+    // typed abstraction
+    TLam(String, Type, Box<Value>),
+    // reified type
+    // 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)
 }
 
 use Value::*;
@@ -50,6 +73,8 @@ 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, "(lam ({} {}) {})", var, typ, body),
+            Value::Type(typ) => write!(f, ":{}", typ),
         }
     }
 }
diff --git a/lambda-calcul/rust/src/lambda.rs b/lambda-calcul/rust/src/lambda.rs
index a73ca34..ed1515a 100644
--- a/lambda-calcul/rust/src/lambda.rs
+++ b/lambda-calcul/rust/src/lambda.rs
@@ -96,6 +96,18 @@ fn subst(var: &str, body: &Value, e: &Value) -> Value {
     }
 }
 
+pub fn type_of_all(values: &[Value]) -> Vec<Type> {
+    let mut env = Environment::new();
+    values.iter().map(|v| type_of(v, &mut env).unwrap()).collect()
+}
+
+fn type_of(v: &Value, env: &mut Environment) -> Result<Type, TypeError> {
+    match v {
+        Value::Num(_) => Ok(Type::Int),
+        _ => Err(TypeError::UnknownType(v.clone())),
+   }
+}
+
 pub fn gensym() -> String {
     let mut rng = rand::thread_rng();
 
@@ -124,6 +136,15 @@ pub fn generate_expr(size: u32, runner: &mut TestRunner) -> Value {
     }
 }
 
+pub fn generate_expression_to_type(size: u32, runner: &mut TestRunner) -> Vec<Value> {
+    match size {
+        _ => {
+            let n = any::<u16>().new_tree(runner).unwrap().current();
+            vec![Value::Num(n.into())]
+        }
+    }
+}
+
 pub fn generate_exprs(size: u32, runner: &mut TestRunner) -> Vec<Value> {
     let sz = (0..size).new_tree(runner).unwrap().current();
     (0..sz)
@@ -201,9 +222,9 @@ fn gen_terms(u: u32) -> impl Strategy<Value = Value> {
 
 #[cfg(test)]
 mod lambda_test {
-    use crate::parser::parse;
+    use crate::{ast::Type, parser::parse};
 
-    use super::{eval_all, eval_whnf, Environment, Value};
+    use super::{Environment, Value, eval_all, eval_whnf, type_of};
 
     fn parse1(string: &str) -> Value {
         parse(string).pop().unwrap()
@@ -289,4 +310,11 @@ mod lambda_test {
         let values = parse("(let (id (lam x x)) (let (foo 12) (id foo)))");
         assert_eq!(vec![Value::Num(12)], eval_all(&values));
     }
+
+    #[test]
+    fn type_of_a_number_is_int() {
+        let value = parse1("12");
+        let ty = type_of(&value, &mut Environment::new()).unwrap();
+        assert_eq!(Type::Int, ty);
+    }
 }
diff --git a/lambda-calcul/rust/src/lib.rs b/lambda-calcul/rust/src/lib.rs
index 53f4c99..a8cf18e 100644
--- a/lambda-calcul/rust/src/lib.rs
+++ b/lambda-calcul/rust/src/lib.rs
@@ -2,4 +2,3 @@ pub mod ast;
 pub mod io;
 pub mod lambda;
 pub mod parser;
-mod types;
diff --git a/lambda-calcul/rust/src/types.rs b/lambda-calcul/rust/src/types.rs
deleted file mode 100644
index e91d57e..0000000
--- a/lambda-calcul/rust/src/types.rs
+++ /dev/null
@@ -1,97 +0,0 @@
-use crate::ast::Value;
-use proptest::prelude::*;
-use proptest::prop_oneof;
-use std::collections::BTreeMap;
-
-type Name = String;
-
-#[derive(Debug, Clone, PartialEq)]
-enum Type {
-    Int,
-    Bool,
-}
-
-fn any_type() -> impl Strategy<Value = Type> {
-    prop_oneof![Just(Type::Int), Just(Type::Bool),]
-}
-
-struct Context {
-    context: BTreeMap<Name, Type>,
-}
-
-impl Context {
-    pub fn empty() -> Self {
-        Context {
-            context: BTreeMap::new(),
-        }
-    }
-
-    pub fn bind(&mut self, sym: Name, ty: Type) -> &mut Self {
-        self.context.insert(sym, ty);
-        self
-    }
-
-    pub fn type_of(&self, val: &Value) -> Option<Type> {
-        use Value::*;
-
-        match val {
-            Num(_) => Some(Type::Int),
-            Bool(_) => Some(Type::Bool),
-            Sym(s) => self.context.get(s).cloned(),
-            _ => None,
-        }
-    }
-}
-
-#[cfg(test)]
-mod tests {
-
-    use super::*;
-    use crate::ast::Value::*;
-    use proptest::prelude::*;
-
-    proptest! {
-
-        #[test]
-        fn any_int_value_has_type_int(n in any::<i32>().prop_map(Num)) {
-            let ctx = Context::empty();
-
-            let ty = ctx.type_of(&n);
-
-            assert_eq!(Some(Type::Int), ty);
-        }
-
-        #[test]
-        fn any_bool_value_has_type_Bool(n in any::<bool>().prop_map(Bool)) {
-            let ctx = Context::empty();
-
-            let ty = ctx.type_of(&n);
-
-            assert_eq!(Some(Type::Bool), ty);
-        }
-
-        #[test]
-        fn any_bound_variable_has_bound_type(s in crate::ast::identifier(), t in any_type()) {
-            let mut ctx = Context::empty();
-            ctx.bind(s.clone(), t.clone());
-
-            let ty = ctx.type_of(&Sym(s));
-
-            assert_eq!(Some(t), ty);
-        }
-
-        #[test]
-        fn any_unbound_variable_has_no_type(s in crate::ast::identifier()) {
-            let mut ctx = Context::empty();
-
-            let ty = ctx.type_of(&Sym(s));
-
-            assert_eq!(None, ty);
-        }
-
-        #[test]
-        fn def_symbol_has_type_of_its_body(s in crate::ast::identifier(), t in any_type()) {
-        }
-
-    }
-}
diff --git a/lambda-calcul/rust/src/web.rs b/lambda-calcul/rust/src/web.rs
index 5bc8c3f..27aed21 100644
--- a/lambda-calcul/rust/src/web.rs
+++ b/lambda-calcul/rust/src/web.rs
@@ -13,7 +13,7 @@ use std::{collections::HashMap, sync::Arc};
 use tokio::task::{self, JoinHandle};
 use uuid::Uuid;
 
-use lambda::lambda::{eval_all, eval_whnf, generate_expr, generate_exprs, gensym, Environment};
+use lambda::lambda::{Environment, eval_all, eval_whnf, generate_expr, generate_expression_to_type, generate_exprs, gensym, type_of_all};
 use lambda::parser::{parse, parse_total};
 
 #[derive(Debug, PartialEq, Serialize, Deserialize, Clone)]
@@ -119,7 +119,9 @@ impl Client {
     }
 
     fn generate_expr(&mut self) -> (Vec<Value>, Vec<Value>) {
-        if self.grade >= 10 {
+        if self.grade >= 20 {
+            self.generate_expression_to_type()
+        } else if self.grade >= 10 {
             self.generate_exprs()
         } else {
             let input = generate_expr(self.grade.into(), &mut self.runner);
@@ -128,6 +130,12 @@ impl Client {
         }
     }
 
+    fn generate_expression_to_type(&mut self) -> (Vec<Value>, Vec<Value>) {
+        let input = generate_expression_to_type(self.grade.into(), &mut self.runner);
+        let expected = type_of_all(&input).iter().map(|t| Value::Type(t.clone())).collect();
+        (input, expected)
+    }
+
     fn generate_exprs(&mut self) -> (Vec<Value>, Vec<Value>) {
         let input = generate_exprs(self.grade.into(), &mut self.runner);
         let expected = eval_all(&input);
@@ -787,6 +795,16 @@ mod app_tests {
     }
 
     #[test]
+    async fn client_generates_typing_expression_at_level_20() {
+        let mut client = client();
+        client.grade = 20;
+
+        let (input, _) = client.generate_expr();
+
+        assert!(!input.is_empty());
+    }
+
+    #[test]
     async fn client_increases_grade_on_successful_test() {
         let mut client = client();
         let test = Test {