type: Add Str

README.md

@@ -172,7 +172,7 @@ $ cargo metadata --format-version=1 | rq '.packages | map .name'
 `rq` is a statically typed language with subtyping.[^1]
 The type system looks as follows:
 
-- Primitive types: `JSON` and `Num`, where `Num ≤ JSON`.
+- Primitive types: `JSON`, `Num`, and `Str`, where `Num, Str ≤ JSON`.
 
 - Universal quantification: `∀a. «Type»` or `forall a. «Type»`.
   The type variable `a` can be any valid identifier (that is not already a primitive type)

src/expr/parser.rs

@@ -316,6 +316,7 @@ fn p_expr<'a>() -> impl Parser<'a, &'a str, Expr, extra::Err<Rich<'a, char>>> {
         p_forall.clone(),            // ∀α. A
         p_list.clone(),
         just("Num").to(Type::Num),   // Num
+        just("Str").to(Type::Str),   // Str
         p_json,
         text::ident().map(|s: &str| Type::Var(s.to_string())),
         p_type.clone().padded().delimited_by(just('('),just(')'))

src/type.rs

@@ -53,6 +53,8 @@ impl Exist {
 pub enum Type {
   /// A number
   Num,
+  /// A string
+  Str,
   /// The JSON black hole
   JSON,
   /// A type variable α
@@ -71,6 +73,7 @@ impl Display for Type {
   fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result {
     match self {
       Self::Num => write!(f, "Num"),
+      Self::Str => write!(f, "Str"),
       Self::JSON => write!(f, "JSON"),
       Self::Var(α) => write!(f, "{α}"),
       Self::Arr(box Self::Arr(t11, t12), t2) => write!(f, "({t11} → {t12}) → {t2}"),
@@ -98,7 +101,7 @@ impl Type {
   /// Substitute the type variable α with type B in A.
   pub fn subst(self, to: Self, from: &str) -> Self {
     match self {
-      Self::Num | Self::JSON | Self::Exist(_) => self.clone(),
+      Self::Num | Self::Str | Self::JSON | Self::Exist(_) => self.clone(),
       Self::Var(ref α) => {
         if α == from {
           to.clone()
@@ -121,7 +124,7 @@ impl Type {
   /// Substitute type C for B in A.
   pub fn subst_type(self, to: &Self, from: &Self) -> Self {
     match self {
-      Self::Num | Self::JSON | Self::Var(_) | Self::Exist(_) => {
+      Self::Num | Self::Str | Self::JSON | Self::Var(_) | Self::Exist(_) => {
         if self == *from {
           to.clone()
         } else {
@@ -163,7 +166,11 @@ impl Type {
 #[derive(PartialEq, Eq, Debug, Clone)]
 #[allow(clippy::upper_case_acronyms)]
 pub enum Monotype {
+  /// A number
   Num,
+  /// A string
+  Str,
+  /// The JSON black hole
   JSON,
   /// A type variable α
   Var(String),
@@ -180,6 +187,7 @@ impl Monotype {
   pub fn to_poly(&self) -> Type {
     match self {
       Self::Num => Type::Num,
+      Self::Str => Type::Str,
       Self::JSON => Type::JSON,
       Self::Var(α) => Type::Var(α.clone()),
       Self::Exist(α̂) => Type::Exist(*α̂),
@@ -200,6 +208,7 @@ impl Type {
     match self {
       Self::Forall(_, _) => None,
       Self::Num => Some(Monotype::Num),
+      Self::Str => Some(Monotype::Str),
       Self::JSON => Some(Monotype::JSON),
       Self::Var(α) => Some(Monotype::Var(α.clone())),
       Self::Exist(α̂) => Some(Monotype::Exist(*α̂)),

src/type/checker.rs

@@ -19,6 +19,7 @@ impl Type {
     match self {
       // UnitWF
       Type::Num => Ok(()),
+      Type::Str => Ok(()),
       Type::JSON => Ok(()),
       // UvarWF
       Type::Var(α) => {
@@ -70,6 +71,8 @@ impl Type {
       (Type::JSON, Type::JSON) => Ok(()),
       // A number is a subtype of a JSON object.
       (Type::Num, Type::Num | Type::JSON) => Ok(()),
+      // A string is a subtype of a JSON object.
+      (Type::Str, Type::Str | 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),
@@ -254,6 +257,7 @@ impl Expr {
     match self {
       // 1l⇒
       Expr::Const(Const::Num(_)) => Ok(Type::Num),
+      Expr::Const(Const::String(_)) => Ok(Type::Str),
       Expr::Const(_) | Expr::Obj(_) => Ok(Type::JSON),
       Expr::Builtin(b) => expr::var(&format!("{b}")).synth(state),
       // List

src/type/context.rs

@@ -60,7 +60,7 @@ impl State {
     }
   }
 
-  /// `state.scoped_around(more, ix, act)` extends the `state` with `more`,
+  /// `state.scoped_around(more, n, act)` extends the `state` with `more`,
   /// executes `act`, and then drops every after and including the `n`th item
   /// from `more`.
   pub fn scoped_around<F: FnOnce(&mut Self) -> TResult<()>>(