From df805bf35002ed2881e298473508b8be680f89dc Mon Sep 17 00:00:00 2001 From: Tony Zorman Date: Wed, 24 Apr 2024 20:17:31 +0200 Subject: [PATCH] type: Add lists --- README.md | 4 ++++ src/expr/parser.rs | 23 +++++++++++------- src/type.rs | 13 ++++++++++ src/type/checker.rs | 58 +++++++++++++++++++++++++++++++++++++++++++-- 4 files changed, 87 insertions(+), 11 deletions(-) diff --git a/README.md b/README.md index cd721dd..d2d767d 100644 --- a/README.md +++ b/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 diff --git a/src/expr/parser.rs b/src/expr/parser.rs index e468bd7..30e9269 100644 --- a/src/expr/parser.rs +++ b/src/expr/parser.rs @@ -300,18 +300,23 @@ fn p_expr<'a>() -> impl Parser<'a, &'a str, Expr, extra::Err>> { .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(')')) )); diff --git a/src/type.rs b/src/type.rs index 6909e97..b860f7f 100644 --- a/src/type.rs +++ b/src/type.rs @@ -62,6 +62,8 @@ pub enum Type { Forall(String, Box), /// A → B Arr(Box, Box), + /// [A] + List(Box), } 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, Box), + /// [τ] + List(Box), } 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()?)), } } } diff --git a/src/type/checker.rs b/src/type/checker.rs index 1c2ffd1..4a21c6e 100644 --- a/src/type/checker.rs +++ b/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