From 5719458b477e05a60b323ba3bb910432b36d30d7 Mon Sep 17 00:00:00 2001
From: Arnaud Bailly <arnaud@pankzsoft.com>
Date: Thu, 9 Oct 2025 15:21:49 +0200
Subject: feat: introduce typing of expressions

---
 lambda-calcul/rust/src/ast.rs | 25 +++++++++++++++++++++++++
 1 file changed, 25 insertions(+)

(limited to 'lambda-calcul/rust/src/ast.rs')

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
@@ -5,6 +5,22 @@ use proptest::{
 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),
@@ -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),
         }
     }
 }
-- 
cgit v1.2.3