type: Add lists

README.md

@@ -178,6 +178,10 @@ The type system looks as follows:
   The type variable `a` can be any valid identifier (that is not already a primitive type)
 
 - Function types: `«Type» → «Type»` or `«Type» -> «Type»`.
+  Function types are contravariant in their first, and covariant in their second argument.
+
+- List types: `[«Type»]`.
+  Lists are covariant.
 
 ### Standard library
 

src/expr/parser.rs

@@ -300,18 +300,23 @@ fn p_expr<'a>() -> impl Parser<'a, &'a str, Expr, extra::Err<Rich<'a, char>>> {
         .ignore_then(text::ident().then_ignore(just(".").padded()))
         .then(p_type.clone())
         .map(|(α, t)| Type::forall(α, t));
+      let p_json = text::ident().try_map(
+        move |s: &str, span| {
+          if "json" == &s.to_lowercase() {
+            Ok(Type::JSON)
+          } else {
+            Err(Rich::custom(span, format!("{s}: Invalid type name")))
+          }
+        },
+      );
+      let p_list = p_type.clone().padded()
+        .delimited_by(just('['), just(']'))
+        .map(Type::list);
       let inner = choice((
         p_forall.clone(),            // ∀α. A
+        p_list.clone(),
         just("Num").to(Type::Num),   // Num
-        text::ident().try_map(       // JSON
-          move |s: &str, span| {
-            if "json" == &s.to_lowercase() {
-              Ok(Type::JSON)
-            } else {
-              Err(Rich::custom(span, format!("{s}: Invalid type name")))
-            }
-          },
-        ),
+        p_json,
         text::ident().map(|s: &str| Type::Var(s.to_string())),
         p_type.clone().padded().delimited_by(just('('),just(')'))
       ));

src/type.rs

@@ -62,6 +62,8 @@ pub enum Type {
   Forall(String, Box<Type>),
   /// A → B
   Arr(Box<Type>, Box<Type>),
+  /// [A]
+  List(Box<Type>),
 }
 
 impl Display for Type {
@@ -74,6 +76,7 @@ impl Display for Type {
       Self::Arr(t1, t2) => write!(f, "{t1} → {t2}"),
       Self::Exist(α̂) => write!(f, "∃{α̂}"),
       Self::Forall(α, t) => write!(f, "∀{α}. {t}"),
+      Self::List(t) => write!(f, "[{t}]"),
     }
   }
 }
@@ -84,6 +87,8 @@ impl Type {
   pub fn forall(v: &str, t: Self) -> Self { Self::Forall(v.to_string(), Box::new(t)) }
 
   pub fn var(v: &str) -> Self { Self::Var(v.to_string()) }
+
+  pub fn list(t: Self) -> Self { Self::List(Box::new(t)) }
 }
 
 impl Type {
@@ -106,6 +111,7 @@ impl Type {
       Self::Arr(box t1, box t2) => {
         Self::arr(t1.subst(to.clone(), from), t2.subst(to, from))
       },
+      Self::List(t) => Self::list(t.subst(to, from)),
     }
   }
 
@@ -121,6 +127,7 @@ impl Type {
           self
         }
       },
+      Self::List(t) => Self::list(t.subst_type(to, from)),
       Self::Forall(α, box t) => Self::forall(&α, t.subst_type(to, from)),
       Self::Arr(box t1, box t2) => {
         Self::arr(t1.subst_type(to, from), t2.subst_type(to, from))
@@ -163,6 +170,8 @@ pub enum Monotype {
   Exist(Exist),
   /// τ → σ
   Arr(Box<Monotype>, Box<Monotype>),
+  /// [τ]
+  List(Box<Monotype>),
 }
 
 impl Monotype {
@@ -174,10 +183,13 @@ impl Monotype {
       Self::Var(α) => Type::Var(α.clone()),
       Self::Exist(α̂) => Type::Exist(*α̂),
       Self::Arr(box τ, box σ) => Type::arr(τ.to_poly(), σ.to_poly()),
+      Self::List(t) => Type::list(t.to_poly()),
     }
   }
 
   fn arr(t1: Self, t2: Self) -> Self { Self::Arr(Box::new(t1), Box::new(t2)) }
+
+  fn list(t: Self) -> Self { Self::List(Box::new(t)) }
 }
 
 impl Type {
@@ -191,6 +203,7 @@ impl Type {
       Self::Var(α) => Some(Monotype::Var(α.clone())),
       Self::Exist(α̂) => Some(Monotype::Exist(*α̂)),
       Self::Arr(t, s) => Some(Monotype::arr(t.to_mono()?, s.to_mono()?)),
+      Self::List(t) => Some(Monotype::list(t.to_mono()?)),
     }
   }
 }

src/type/checker.rs

@@ -9,7 +9,7 @@
 //! The article is readily available [on the arXiv](https://arxiv.org/abs/1306.6032).
 
 use super::{context::{Item, State}, error::{TResult, TypeCheckError}, Exist, Monotype, Type};
-use crate::expr::{self, Const, Expr};
+use crate::expr::{Const, Expr, {self}};
 
 impl Type {
   ///                   A.well_formed_under(Γ)  ≡  Γ ⊢ A
@@ -49,6 +49,8 @@ impl Type {
         t1.well_formed_under(ctx)?;
         t2.well_formed_under(ctx)
       },
+      // ListWF
+      Type::List(t) => t.well_formed_under(ctx),
     }
   }
 
@@ -68,6 +70,9 @@ impl Type {
       (Type::JSON, Type::JSON) => Ok(()),
       // A number is a subtype of a JSON object.
       (Type::Num, Type::Num | Type::JSON) => Ok(()),
+      // Lists are covariant.
+      (Type::List(t1), Type::List(t2)) => t1.subtype_of(state, t2),
+      (Type::List(t1), t2) => t1.subtype_of(state, t2),
       // <:→
       (Type::Arr(a1, a2), Type::Arr(b1, b2)) => {
         b1.subtype_of(state, a1)?; /* Contravariant! */
@@ -166,6 +171,18 @@ impl Exist {
             self.instantiate_l(state, t.clone())
           })
         },
+        // Lists behave like InstLArr.
+        Type::List(box t) => {
+          let α̂ = Exist(state.fresh_mut());
+          state.replace_with(
+            &Item::Unsolved(self),
+            &[
+              Item::Unsolved(α̂),
+              Item::Solved(self, Monotype::list(Monotype::Exist(α̂))),
+            ],
+          );
+          α̂.instantiate_l(state, t.apply_ctx(&state.ctx))
+        },
         _ => Err(TypeCheckError::InstantiationError(self, typ)),
       },
     }
@@ -200,6 +217,18 @@ impl Exist {
           α̂1.instantiate_l(state, t)?;
           α̂2.instantiate_r(state, s.apply_ctx(&state.ctx))
         },
+        // Lists behave like InstRArr.
+        Type::List(box t) => {
+          let α̂ = Exist(state.fresh_mut());
+          state.replace_with(
+            &Item::Unsolved(self),
+            &[
+              Item::Unsolved(α̂),
+              Item::Solved(self, Monotype::list(Monotype::Exist(α̂))),
+            ],
+          );
+          α̂.instantiate_l(state, t.apply_ctx(&state.ctx))
+        },
         // InstRAIIL
         Type::Forall(α, box t) => {
           let fresh_α̂ = Exist(state.fresh_mut());
@@ -225,8 +254,25 @@ impl Expr {
     match self {
       // 1l⇒
       Expr::Const(Const::Num(_)) => Ok(Type::Num),
-      Expr::Const(_) | Expr::Arr(_) | Expr::Obj(_) => Ok(Type::JSON),
+      Expr::Const(_) | Expr::Obj(_) => Ok(Type::JSON),
       Expr::Builtin(b) => expr::var(b.show()).synth(state),
+      // List
+      Expr::Arr(xs) => {
+        if xs.is_empty() {
+          // An empty lists means it can have any type.
+          let α̂ = Exist(state.fresh_mut());
+          state.ctx.push(Item::Unsolved(α̂));
+          Ok(Type::list(Type::Exist(α̂)))
+        } else {
+          // A non-empty list means we infer the first type, and check every
+          // element in the list against it.
+          let type_head = xs[0].synth(state)?;
+          for el in &xs[1..] {
+            el.check(state, &type_head.apply_ctx(&state.ctx))?;
+          }
+          Ok(Type::list(type_head))
+        }
+      },
       // Var
       Expr::Var(v) => match state
         .ctx
@@ -288,7 +334,15 @@ impl Expr {
     // println!("check; ctx: {:?}  e: {:?}  b: {:?}", state.ctx, self, against);
     match (self, against) {
       // 1I
+      (Expr::Const(Const::Num(_)), Type::JSON | Type::Num) => Ok(()),
       (Expr::Const(_), Type::JSON) => Ok(()),
+      // As in `synth`, lists are just treated as JSON lists for now.
+      (Expr::Arr(xs), Type::List(t)) => {
+        for el in xs {
+          el.check(state, t)?;
+        }
+        Ok(())
+      },
       // ∀I
       (_, Type::Forall(α, box t)) => {
         // Type variables are assumed to be unique, so introducing a fresh one