type: Add Num

slotThe · Mar 15, 2024 · 6cb2310 · 6cb2310
1 parent 1a3a7be
commit 6cb2310
Show file tree

Hide file tree

Showing 4 changed files with 49 additions and 23 deletions.
diff --git a/README.md b/README.md
@@ -173,9 +173,9 @@ $ cargo metadata --format-version=1 | rq '.packages | map .name'
 
   ``` agda
   (+)  : JSON → JSON → JSON  -- Also works for string concatenation
-  (-)  : JSON → JSON → JSON
-  (*)  : JSON → JSON → JSON
-  (/)  : JSON → JSON → JSON
+  (-)  : Num → Num → Num
+  (*)  : Num → Num → Num
+  (/)  : Num → Num → Num
   ```
 
 - Comparisons:
@@ -185,10 +185,10 @@ $ cargo metadata --format-version=1 | rq '.packages | map .name'
   ``` agda
   (=)  : JSON → JSON → JSON
   (!=) : JSON → JSON → JSON
-  (<)  : JSON → JSON → JSON
-  (<=) : JSON → JSON → JSON
-  (>)  : JSON → JSON → JSON
-  (>=) : JSON → JSON → JSON
+  (<)  : Num → Num → Num
+  (<=) : Num → Num → Num
+  (>)  : Num → Num → Num
+  (>=) : Num → Num → Num
   ```
 
 - Higher order functions:

diff --git a/src/eval/stdlib.rs b/src/eval/stdlib.rs
@@ -110,7 +110,7 @@ pub static STDLIB_TYPES: LazyLock<BTreeMap<String, Type>> = LazyLock::new(|| {
 });
 
 pub static STDLIB: LazyLock<BTreeMap<Builtin, StdFun>> = LazyLock::new(|| {
-  use Type::JSON;
+  use Type::*;
 
   BTreeMap::from([
     mk_fun!(
@@ -149,7 +149,16 @@ pub static STDLIB: LazyLock<BTreeMap<Builtin, StdFun>> = LazyLock::new(|| {
     ),
     mk_fun!(
       Builtin::Map, // (a → b) → [a] → [b]
-      Type::arr(Type::arr(JSON, JSON), Type::arr(JSON, JSON)),
+      Type::forall(
+        "a",
+        Type::forall(
+          "b",
+          Type::arr(
+            Type::arr(Type::var("a"), Type::var("b")),
+            Type::arr(JSON, JSON)
+          )
+        )
+      ),
       Blocks::new()
         .fancy("map f xs")
         .plain("applies")
@@ -174,9 +183,15 @@ pub static STDLIB: LazyLock<BTreeMap<Builtin, StdFun>> = LazyLock::new(|| {
     ),
     mk_fun!(
       Builtin::Foldl, // (b → a → b) → b → [a] → b
-      Type::arr(
-        Type::arr(JSON, Type::arr(JSON, JSON)),
-        Type::arr(JSON, Type::arr(JSON, JSON)),
+      Type::forall(
+        "a",
+        Type::forall(
+          "b",
+          Type::arr(
+            Type::arr(Type::var("b"), Type::arr(Type::var("a"), Type::var("b"))),
+            Type::arr(Type::var("b"), Type::arr(JSON, Type::var("b"))),
+          )
+        )
       ),
       Blocks::new()
         .plain("Left-associative fold over an array or (values of an) object; e.g.,")
@@ -189,18 +204,18 @@ pub static STDLIB: LazyLock<BTreeMap<Builtin, StdFun>> = LazyLock::new(|| {
     ),
     mk_fun!(
       Builtin::Sub,
-      Type::arr(JSON, Type::arr(JSON, JSON)),
+      Type::arr(Num, Type::arr(Num, Num)),
       Blocks::to_plain("Subtract two numbers."),
     ),
     mk_fun!(
       Builtin::Mul,
-      Type::arr(JSON, Type::arr(JSON, JSON)),
+      Type::arr(Num, Type::arr(Num, Num)),
       Blocks::to_plain("Multiply two numbers."),
       "·"
     ),
     mk_fun!(
       Builtin::Div,
-      Type::arr(JSON, Type::arr(JSON, JSON)),
+      Type::arr(Num, Type::arr(Num, Num)),
       Blocks::to_plain(
         "Divide two numbers. No guarantees if the denominator is zero—the world might \
          explode.",
@@ -221,7 +236,7 @@ pub static STDLIB: LazyLock<BTreeMap<Builtin, StdFun>> = LazyLock::new(|| {
     ),
     mk_fun!(
       Builtin::Le,
-      Type::arr(JSON, Type::arr(JSON, JSON)),
+      Type::arr(Num, Type::arr(Num, Num)),
       Blocks::new()
         .fancy("e < e'")
         .plain("checks whether")
@@ -231,7 +246,7 @@ pub static STDLIB: LazyLock<BTreeMap<Builtin, StdFun>> = LazyLock::new(|| {
     ),
     mk_fun!(
       Builtin::Leq,
-      Type::arr(JSON, Type::arr(JSON, JSON)),
+      Type::arr(Num, Type::arr(Num, Num)),
       Blocks::new()
         .fancy("e ≤ e'")
         .plain("checks whether")
@@ -242,7 +257,7 @@ pub static STDLIB: LazyLock<BTreeMap<Builtin, StdFun>> = LazyLock::new(|| {
     ),
     mk_fun!(
       Builtin::Ge,
-      Type::arr(JSON, Type::arr(JSON, JSON)),
+      Type::arr(Num, Type::arr(Num, Num)),
       Blocks::new()
         .fancy("e > e'")
         .plain("checks whether")
@@ -252,7 +267,7 @@ pub static STDLIB: LazyLock<BTreeMap<Builtin, StdFun>> = LazyLock::new(|| {
     ),
     mk_fun!(
       Builtin::Geq,
-      Type::arr(JSON, Type::arr(JSON, JSON)),
+      Type::arr(Num, Type::arr(Num, Num)),
       Blocks::new()
         .fancy("e ≥ e'")
         .plain("checks whether")

diff --git a/src/type.rs b/src/type.rs
@@ -50,6 +50,9 @@ impl Exist {
 #[derive(PartialEq, Eq, Debug, Clone, PartialOrd, Ord)]
 #[allow(clippy::upper_case_acronyms)]
 pub enum Type {
+  /// A number
+  Num,
+  /// The JSON black hole
   JSON,
   /// A type variable α
   Var(String),
@@ -64,6 +67,7 @@ pub enum Type {
 impl Display for Type {
   fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result {
     match self {
+      Self::Num => write!(f, "Num"),
       Self::JSON => write!(f, "JSON"),
       Self::Var(α) => write!(f, "{α}"),
       Self::Arr(box Self::Arr(t11, t12), t2) => write!(f, "({t11} → {t12}) → {t2}"),
@@ -88,7 +92,7 @@ impl Type {
   /// Substitute the type variable α with type B in A.
   pub fn subst(self, to: Self, from: &str) -> Self {
     match self {
-      Self::JSON | Self::Exist(_) => self.clone(),
+      Self::Num | Self::JSON | Self::Exist(_) => self.clone(),
       Self::Var(ref α) => {
         if α == from {
           to.clone()
@@ -110,7 +114,7 @@ impl Type {
   /// Substitute type C for B in A.
   pub fn subst_type(self, to: &Self, from: &Self) -> Self {
     match self {
-      Self::JSON | Self::Var(_) | Self::Exist(_) => {
+      Self::Num | Self::JSON | Self::Var(_) | Self::Exist(_) => {
         if self == *from {
           to.clone()
         } else {
@@ -151,6 +155,7 @@ impl Type {
 #[derive(PartialEq, Eq, Debug, Clone)]
 #[allow(clippy::upper_case_acronyms)]
 pub enum Monotype {
+  Num,
   JSON,
   /// A type variable α
   Var(String),
@@ -164,6 +169,7 @@ impl Monotype {
   /// Convert a [Monotype] to a (poly)[Type].
   pub fn to_poly(&self) -> Type {
     match self {
+      Self::Num => Type::Num,
       Self::JSON => Type::JSON,
       Self::Var(α) => Type::Var(α.clone()),
       Self::Exist(α̂) => Type::Exist(*α̂),
@@ -180,6 +186,7 @@ impl Type {
   pub fn to_mono(&self) -> Option<Monotype> {
     match self {
       Self::Forall(_, _) => None,
+      Self::Num => Some(Monotype::Num),
       Self::JSON => Some(Monotype::JSON),
       Self::Var(α) => Some(Monotype::Var(α.clone())),
       Self::Exist(α̂) => Some(Monotype::Exist(*α̂)),

diff --git 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, Expr};
+use crate::expr::{self, Const, Expr};
 
 impl Type {
   ///                   A.well_formed_under(Γ)  ≡  Γ ⊢ A
@@ -18,6 +18,7 @@ impl Type {
   fn well_formed_under(&self, ctx: &[Item]) -> TResult<()> {
     match self {
       // UnitWF
+      Type::Num => Ok(()),
       Type::JSON => Ok(()),
       // UvarWF
       Type::Var(α) => {
@@ -65,9 +66,11 @@ impl Type {
       },
       // <:JSON ≡ <:Unit
       (Type::JSON, Type::JSON) => Ok(()),
+      // A number is a subtype of a JSON object.
+      (Type::Num, Type::Num | Type::JSON) => Ok(()),
       // <:→
       (Type::Arr(a1, a2), Type::Arr(b1, b2)) => {
-        b1.subtype_of(state, a1)?;
+        b1.subtype_of(state, a1)?; /* Contravariant! */
         // See Note [Apply]
         a2.apply_ctx(&state.ctx)
           .subtype_of(state, &b2.apply_ctx(&state.ctx))
@@ -221,6 +224,7 @@ impl Expr {
     // println!("infer; ctx: {:?}  e: {:?}", state.ctx, self);
     match self {
       // 1l⇒
+      Expr::Const(Const::Num(_)) => Ok(Type::Num),
       Expr::Const(_) | Expr::Arr(_) | Expr::Obj(_) => Ok(Type::JSON),
       Expr::Builtin(b) => expr::var(b.show()).synth(state),
       // Var