feat: introduce typing of expressions

1 files changed, 25 insertions, 0 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),
         }
     }
 }