From 56f47bb2e5816de7630569a8825914d0620983cc Mon Sep 17 00:00:00 2001
From: JJ
Date: Wed, 12 Apr 2023 18:30:35 -0700
Subject: subtyping wip

---
 src/ast.rs             |  5 +++--
 src/simple.rs          | 41 +++++++++++++++++++++++++++++++++--------
 src/util.rs            |  1 +
 tests/test_checking.rs |  4 ++--
 4 files changed, 39 insertions(+), 12 deletions(-)

diff --git a/src/ast.rs b/src/ast.rs
index 0a2afdb..bf34d19 100644
--- a/src/ast.rs
+++ b/src/ast.rs
@@ -25,14 +25,15 @@ pub type Value = u64;
 #[derive(Debug, Clone, PartialEq, Eq)]
 pub enum Type {
     Empty,
+    Error,
     Unit,
     Boolean,
     Natural,
     Integer,
     // Float,
     // String,
-    // Enum(Vec<Type>),
-    // Record(Vec<Type>),
+    Enum(Vec<Type>),
+    Record(HashMap<Identifier, Type>),
     Function{from: Box<Type>, to: Box<Type>},
 }
 
diff --git a/src/simple.rs b/src/simple.rs
index dad9a84..7fe8989 100644
--- a/src/simple.rs
+++ b/src/simple.rs
@@ -7,12 +7,12 @@ use crate::ast::*;
 pub fn check(context: Context, expression: Expression, target: Type) -> Result<(), (&'static str, Context, Type)> {
     match expression {
         // Expression::Annotation { expr, kind } => Err(("attempting to typecheck an annotation", context, target)),
-        Expression::Annotation { expr, kind } => match infer(context.clone(), Expression::Annotation { expr, kind })? == target {
+        Expression::Annotation { expr, kind } => match subtype(&infer(context.clone(), Expression::Annotation { expr, kind })?, &target) {
             true => Ok(()),
             false => Err(("inferred type from annotation does not match target", context, target))
         },
         // Bt-CheckInfer
-        Expression::Constant { term } => match term.kind == target {
+        Expression::Constant { term } => match subtype(&term.kind, &target) {
             true => Ok(()),
             false => Ok(()) // all our constants are Empty for now
             // false => Err(("constant is of wrong type", context, target))
@@ -20,7 +20,7 @@ pub fn check(context: Context, expression: Expression, target: Type) -> Result<(
         // Bt-CheckInfer
         // in the future: extend to closures? nah probably not
         Expression::Variable { id } => match context.get(&id) {
-            Some(term) if term.kind == target => Ok(()),
+            Some(term) if subtype(&term.kind, &target) => Ok(()),
             Some(_) => Err(("variable is of wrong type", context, target)),
             None => Err(("failed to find variable in context", context, target))
         },
@@ -34,7 +34,7 @@ pub fn check(context: Context, expression: Expression, target: Type) -> Result<(
             _ => Err(("attempting to check an abstraction with a non-function type", context, target))
         },
         // Expression::Application { func, arg } => Err(("attempting to check an application", context, target)),
-        Expression::Application { func, arg } => match infer(context.clone(), Expression::Application { func, arg })? == target {
+        Expression::Application { func, arg } => match subtype(&infer(context.clone(), Expression::Application { func, arg })?, &target) {
             true => Ok(()),
             false => Err(("inferred type does not match target", context, target))
         },
@@ -73,8 +73,8 @@ pub fn infer(context: Context, expression: Expression) -> Result<Type, (&'static
             check(context.clone(), *if_cond, Type::Boolean)?;
             let if_then = infer(context.clone(), *if_then)?;
             let if_else = infer(context.clone(), *if_else)?;
-            if if_then == if_else {
-                Ok(if_then)
+            if subtype(&if_then, &if_else) && subtype(&if_else, &if_then) {
+                Ok(if_then) // fixme: should be the join
             } else {
                 Err(("if clauses of different types", context, Type::Empty))
             }
@@ -82,8 +82,7 @@ pub fn infer(context: Context, expression: Expression) -> Result<Type, (&'static
     }
 }
 
-/// Evaluates an expression given a context (of variables) to a term.
-/// Panics on non-evaluatable code.
+/// Evaluates an expression given a context (of variables) to a term, or fails.
 pub fn execute(context: Context, expression: Expression) -> Result<Term, (&'static str, Context)> {
     match expression {
         Expression::Annotation { expr, .. } => execute(context, *expr),
@@ -115,3 +114,29 @@ pub fn execute(context: Context, expression: Expression) -> Result<Term, (&'stat
         }
     }
 }
+
+/// The subtyping relation between any two types.
+pub fn subtype(is: &Type, of: &Type) -> bool {
+    match (is, of) {
+        (Type::Record(is_fields), Type::Record(of_fields)) => {
+            // width, depth, and permutation
+            for (key, of_value) in of_fields {
+                match is_fields.get(key) {
+                    Some(is_value) => if !subtype(is_value, of_value) {
+                        return false;
+                    },
+                    None => return false
+                }
+            }
+            return true;
+        },
+        (Type::Function { from: is_from, to: is_to }, Type::Function { from: of_from, to: of_to }) => {
+            subtype(of_from, is_from) && subtype(is_to, of_to)
+        }
+        (Type::Natural, Type::Integer) => true, // obviously not, but let's pretend
+        (_, Type::Empty) => true,
+        (Type::Error, _) => true,
+        (_, _) if is == of => true,
+        (_, _) => false,
+    }
+}
diff --git a/src/util.rs b/src/util.rs
index b2b3035..68a8a19 100644
--- a/src/util.rs
+++ b/src/util.rs
@@ -66,6 +66,7 @@ pub fn Func(from: Type, to: Type) -> Type {
 }
 
 pub const Empty: Type = Type::Empty;
+pub const Error: Type = Type::Empty;
 pub const Unit: Type = Type::Unit;
 pub const Bool: Type = Type::Boolean;
 pub const Nat: Type = Type::Natural;
diff --git a/tests/test_checking.rs b/tests/test_checking.rs
index 0ec6acd..60bb6da 100644
--- a/tests/test_checking.rs
+++ b/tests/test_checking.rs
@@ -51,8 +51,8 @@ fn test_checking() {
     assert!(check(Context::new(), parse_lambda(basic_application).unwrap(), Int).is_ok());
     assert!(check(Context::new(), parse_lambda(correct_cond_abs).unwrap(), Func(Bool, Int)).is_ok());
     assert!(check(Context::new(), parse_lambda(correct_cond).unwrap(), Nat).is_ok());
-    assert!(check(Context::new(), parse_lambda(incorrect_branches).unwrap(), Empty).is_err());
-    assert!(check(Context::new(), parse_lambda(incorrect_cond_abs).unwrap(), Empty).is_err());
+    assert!(check(Context::new(), parse_lambda(incorrect_branches).unwrap(), Unit).is_err());
+    assert!(check(Context::new(), parse_lambda(incorrect_cond_abs).unwrap(), Error).is_err());
 
     // more fun
     assert_eq!(check(Context::new(), parse_lambda(not_inferrable).unwrap(), Func(Bool, Func(Int, Func(Int, Int)))), Ok(()));
-- 
cgit v1.2.3-70-g09d2