SATS: address George's review

crates/sats/src/algebraic_type.rs

@@ -202,7 +202,7 @@ impl AlgebraicType {
     pub fn option(some_type: Self) -> Self {
         Self::sum(vec![
             SumTypeVariant::new_named(some_type, "some"),
-            SumTypeVariant::new_named(AlgebraicType::UNIT_TYPE, "none"),
+            SumTypeVariant::unit("none"),
         ])
     }
 
@@ -219,12 +219,7 @@ impl AlgebraicType {
 
     /// Returns a sum type of unit variants with names taken from `var_names`.
     pub fn simple_enum<'a>(var_names: impl Iterator<Item = &'a str>) -> Self {
-        Self::sum(
-            var_names
-                .into_iter()
-                .map(|x| SumTypeVariant::new_named(AlgebraicType::UNIT_TYPE, x))
-                .collect(),
-        )
+        Self::sum(var_names.into_iter().map(SumTypeVariant::unit).collect())
     }
 
     pub fn as_value(&self) -> AlgebraicValue {

crates/sats/src/algebraic_type/map_notation.rs

@@ -4,7 +4,7 @@ use crate::de::fmt_fn;
 use crate::{ArrayType, MapType};
 use std::fmt::{self, Formatter};
 
-/// Wraps an algebraic `ty` in a `Display` impl using a map notation.
+/// Wraps an algebraic `ty` in a `Display` impl using a object/map JSON-like notation.
 pub fn fmt_algebraic_type(ty: &AlgebraicType) -> impl '_ + fmt::Display {
     use fmt_algebraic_type as fmt;
 

crates/sats/src/algebraic_value.rs

@@ -6,9 +6,15 @@ use crate::builtin_value::{F32, F64};
 use crate::{AlgebraicType, ArrayValue, BuiltinType, BuiltinValue, ProductValue, SumValue};
 use enum_as_inner::EnumAsInner;
 
-/// A value in SATS.
+/// A value in SATS typed at some [`AlgebraicType`].
 ///
-/// These values are fully evaluated.
+/// Values are type erased, so they do not store their type.
+/// This is important mainly for space efficiency,
+/// including network latency and bandwidth.
+///
+/// These are only values and not expressions.
+/// That is, they are canonical and cannot be simplified further by some evaluation.
+/// So forms like `42 + 24` are not represented in an `AlgebraicValue`.
 #[derive(EnumAsInner, Debug, Clone, Eq, PartialEq, Ord, PartialOrd, Hash)]
 pub enum AlgebraicValue {
     /// A structural sum value.
@@ -372,7 +378,7 @@ impl AlgebraicValue {
 
     /// Returns the [`AlgebraicType`] of the sum value `x`.
     pub(crate) fn type_of_sum(x: &SumValue) -> AlgebraicType {
-        // TODO(centril): This is unsound!
+        // TODO(centril, #104): This is unsound!
         //
         //   The type of a sum value must be a sum type and *not* a product type.
         //   Suppose `x.tag` is for the variant `VarName(VarType)`.

crates/sats/src/bsatn.rs

@@ -23,12 +23,12 @@ pub fn to_vec<T: Serialize + ?Sized>(value: &T) -> Result<Vec<u8>, ser::BsatnErr
     Ok(v)
 }
 
-/// Deserialize a `T` from the BSATM format in the buffered `reader`.
+/// Deserialize a `T` from the BSATN format in the buffered `reader`.
 pub fn from_reader<'de, T: Deserialize<'de>>(reader: &mut impl BufReader<'de>) -> Result<T, DecodeError> {
     T::deserialize(Deserializer::new(reader))
 }
 
-/// Deserialize a `T` from the BSATM format in `bytes`.
+/// Deserialize a `T` from the BSATN format in `bytes`.
 pub fn from_slice<'de, T: Deserialize<'de>>(bytes: &'de [u8]) -> Result<T, DecodeError> {
     from_reader(&mut &*bytes)
 }

crates/sats/src/builtin_type.rs

@@ -3,7 +3,7 @@ use crate::algebraic_value::ser::ValueSerializer;
 use crate::meta_type::MetaType;
 use crate::{de::Deserialize, ser::Serialize};
 use crate::{
-    impl_deserialize, impl_serialize, AlgebraicType, AlgebraicTypeRef, AlgebraicValue, ProductType, ProductTypeElement,
+    impl_deserialize, impl_serialize, AlgebraicType, AlgebraicTypeRef, AlgebraicValue, ProductTypeElement,
     SumTypeVariant,
 };
 use enum_as_inner::EnumAsInner;
@@ -14,40 +14,44 @@ use enum_as_inner::EnumAsInner;
 #[derive(EnumAsInner, Debug, Clone, Eq, PartialEq, Ord, PartialOrd, Hash, Serialize, Deserialize)]
 #[sats(crate = crate)]
 pub enum BuiltinType {
-    /// The bool type. Values `BuiltinValue::Bool(b)` will have this type.
+    /// The bool type. Values [`BuiltinValue::Bool(b)`](crate::BuiltinValue::Bool) will have this type.
     Bool,
-    /// The `I8` type. Values `BuiltinValue::I8(v)` will have this type.
+    /// The `I8` type. Values [`BuiltinValue::I8(v)`](crate::BuiltinValue::I8) will have this type.
     I8,
-    /// The `U8` type. Values `BuiltinValue::U8(v)` will have this type.
+    /// The `U8` type. Values [`BuiltinValue::U8(v)`](crate::BuiltinValue::U8) will have this type.
     U8,
-    /// The `I16` type. Values `BuiltinValue::I16(v)` will have this type.
+    /// The `I16` type. Values [`BuiltinValue::I16(v)`](crate::BuiltinValue::I16) will have this type.
     I16,
-    /// The `U16` type. Values `BuiltinValue::U16(v)` will have this type.
+    /// The `U16` type. Values [`BuiltinValue::U16(v)`](crate::BuiltinValue::U16) will have this type.
     U16,
-    /// The `I32` type. Values `BuiltinValue::I32(v)` will have this type.
+    /// The `I32` type. Values [`BuiltinValue::I32(v)`](crate::BuiltinValue::I32) will have this type.
     I32,
-    /// The `U32` type. Values `BuiltinValue::U32(v)` will have this type.
+    /// The `U32` type. Values [`BuiltinValue::U32(v)`](crate::BuiltinValue::U32) will have this type.
     U32,
-    /// The `I64` type. Values `BuiltinValue::I64(v)` will have this type.
+    /// The `I64` type. Values [`BuiltinValue::I64(v)`](crate::BuiltinValue::I64) will have this type.
     I64,
-    /// The `U64` type. Values `BuiltinValue::U64(v)` will have this type.
+    /// The `U64` type. Values [`BuiltinValue::U64(v)`](crate::BuiltinValue::U64) will have this type.
     U64,
-    /// The `I128` type. Values `BuiltinValue::I128(v)` will have this type.
+    /// The `I128` type. Values [`BuiltinValue::I128(v)`](crate::BuiltinValue::I128) will have this type.
     I128,
-    /// The `U128` type. Values `BuiltinValue::U128(v)` will have this type.
+    /// The `U128` type. Values [`BuiltinValue::U128(v)`](crate::BuiltinValue::U128) will have this type.
     U128,
-    /// The `F32` type. Values `BuiltinValue::F32(v)` will have this type.
+    /// The `F32` type. Values [`BuiltinValue::F32(v)`](crate::BuiltinValue::F32) will have this type.
     F32,
-    /// The `F64` type. Values `BuiltinValue::F64(v)` will have this type.
+    /// The `F64` type. Values [`BuiltinValue::F64(v)`](crate::BuiltinValue::F64) will have this type.
     F64,
     /// The UTF-8 encoded `String` type.
-    /// Values `BuiltinValue::String(s)` will have this type.
-    String, // Keep this because it is easy to just use Rust's `String` (UTF-8).
+    /// Values [`BuiltinValue::String(s)`](crate::BuiltinValue::String) will have this type.
+    ///
+    /// This type exists for convenience and because it is easy to just use Rust's `String` (UTF-8)
+    /// as opposed to rolling your own equivalent byte-array based UTF-8 encoding.
+    String,
     /// The type of array values where elements are of a base type `elem_ty`.
-    /// Values `BuiltinValue::Array(array)` will have this type.
+    /// Values [`BuiltinValue::Array(array)`](crate::BuiltinValue::Array) will have this type.
     Array(ArrayType),
     /// The type of map values consisting of a key type `key_ty` and value `ty`.
-    /// Values `BuiltinValue::Map(map)` will have this type.
+    /// Values [`BuiltinValue::Map(map)`](crate::BuiltinValue::Map) will have this type.
+    /// The order of entries in a map value is observable.
     Map(MapType),
 }
 
@@ -87,28 +91,26 @@ impl MapType {
 
 impl MetaType for BuiltinType {
     fn meta_type() -> AlgebraicType {
-        let product = |elements| AlgebraicType::Product(ProductType { elements });
-        let unit = || product(Vec::new());
         let zero_ref = || AlgebraicType::Ref(AlgebraicTypeRef(0));
         // TODO: sats(rename_all = "lowercase"), otherwise json won't work.
         AlgebraicType::sum(vec![
-            SumTypeVariant::new_named(unit(), "bool"),
-            SumTypeVariant::new_named(unit(), "i8"),
-            SumTypeVariant::new_named(unit(), "u8"),
-            SumTypeVariant::new_named(unit(), "i16"),
-            SumTypeVariant::new_named(unit(), "u16"),
-            SumTypeVariant::new_named(unit(), "i32"),
-            SumTypeVariant::new_named(unit(), "u32"),
-            SumTypeVariant::new_named(unit(), "i64"),
-            SumTypeVariant::new_named(unit(), "u64"),
-            SumTypeVariant::new_named(unit(), "i128"),
-            SumTypeVariant::new_named(unit(), "u128"),
-            SumTypeVariant::new_named(unit(), "f32"),
-            SumTypeVariant::new_named(unit(), "f64"),
-            SumTypeVariant::new_named(unit(), "string"),
+            SumTypeVariant::unit("bool"),
+            SumTypeVariant::unit("i8"),
+            SumTypeVariant::unit("u8"),
+            SumTypeVariant::unit("i16"),
+            SumTypeVariant::unit("u16"),
+            SumTypeVariant::unit("i32"),
+            SumTypeVariant::unit("u32"),
+            SumTypeVariant::unit("i64"),
+            SumTypeVariant::unit("u64"),
+            SumTypeVariant::unit("i128"),
+            SumTypeVariant::unit("u128"),
+            SumTypeVariant::unit("f32"),
+            SumTypeVariant::unit("f64"),
+            SumTypeVariant::unit("string"),
             SumTypeVariant::new_named(zero_ref(), "array"),
             SumTypeVariant::new_named(
-                product(vec![
+                AlgebraicType::product(vec![
                     ProductTypeElement::new_named(zero_ref(), "key_ty"),
                     ProductTypeElement::new_named(zero_ref(), "ty"),
                 ]),

crates/sats/src/builtin_value.rs

@@ -5,55 +5,76 @@ use enum_as_inner::EnumAsInner;
 use std::collections::BTreeMap;
 use std::fmt;
 
-/// Totally ordered [`f32`].
+/// Totally ordered [`f32`] allowing all IEEE-754 floating point values.
 pub type F32 = decorum::Total<f32>;
 
-/// Totally ordered [`f64`].
+/// Totally ordered [`f64`] allowing all IEEE-754 floating point values.
 pub type F64 = decorum::Total<f64>;
 
 /// A built-in value of a [`BuiltinType`].
 #[derive(EnumAsInner, Debug, Clone, Eq, PartialEq, Ord, PartialOrd, Hash)]
 pub enum BuiltinValue {
-    /// A [`bool`] value.
+    /// A [`bool`] value of type [`BuiltinType::Bool`].
     Bool(bool),
-    /// An [`i8`] value.
+    /// An [`i8`] value of type [`BuiltinType::I8`].
     I8(i8),
-    /// A [`u8`] value.
+    /// A [`u8`] value of type [`BuiltinType::U8`].
     U8(u8),
-    /// An [`i16`] value.
+    /// An [`i16`] value of type [`BuiltinType::I16`].
     I16(i16),
-    /// A [`u16`] value.
+    /// A [`u16`] value of type [`BuiltinType::U16`].
     U16(u16),
-    /// An [`i32`] value.
+    /// An [`i32`] value of type [`BuiltinType::I32`].
     I32(i32),
-    /// A [`u32`] value.
+    /// A [`u32`] value of type [`BuiltinType::U32`].
     U32(u32),
-    /// An [`i64`] value.
+    /// An [`i64`] value of type [`BuiltinType::I64`].
     I64(i64),
-    /// A [`u64`] value.
+    /// A [`u64`] value of type [`BuiltinType::U64`].
     U64(u64),
-    /// An [`i128`] value.
+    /// An [`i128`] value of type [`BuiltinType::I128`].
     I128(i128),
-    /// A [`u128`] value.
+    /// A [`u128`] value of type [`BuiltinType::U128`].
     U128(u128),
-    /// A totally ordered [`F32`] value.
+    /// A totally ordered [`F32`] value of type [`BuiltinType::F32`].
+    ///
+    /// All floating point values defined in IEEE-754 are supported.
+    /// However, unlike the primitive [`f32`], a [total order] is established.
+    ///
+    /// [total order]: https://docs.rs/decorum/0.3.1/decorum/#total-ordering
     F32(F32),
-    /// A totally ordered [`F64`] value.
+    /// A totally ordered [`F64`] value of type [`BuiltinType::F64`].
+    ///
+    /// All floating point values defined in IEEE-754 are supported.
+    /// However, unlike the primitive [`f64`], a [total order] is established.
+    ///
+    /// [total order]: https://docs.rs/decorum/0.3.1/decorum/#total-ordering
     F64(F64),
-    /// A UTF-8 string value.
+    /// A UTF-8 string value of type [`BuiltinType::String`].
     ///
     /// Uses Rust's standard representation of strings.
     String(String),
     /// A homogeneous array of `AlgebraicValue`s.
+    /// The array has the type [`BuiltinType::Array(elem_ty)`].
     ///
     /// The contained values are stored packed in a representation appropriate for their type.
     /// See [`ArrayValue`] for details on the representation.
     Array { val: ArrayValue },
     /// An ordered map value of `key: AlgebraicValue`s mapped to `value: AlgebraicValue`s.
     /// Each `key` must be of the same [`AlgebraicType`] as all the others
     /// and the same applies to each `value`.
+    /// A map as a whole has the type [`BuiltinType::Map(key_ty, val_ty)`].
     ///
-    /// Maps are implemented internally as `BTreeMap<AlgebraicValue, AlgebraicValue>`.
+    /// Maps are implemented internally as [`BTreeMap<AlgebraicValue, AlgebraicValue>`].
+    /// This implies that key/values are ordered first by key and then value
+    /// as if they were a sorted slice `[(key, value)]`.
+    /// This order is observable as maps are exposed both directly
+    /// and indirectly via `Ord for `[`AlgebraicValue`].
+    /// The latter lets us observe that e.g., `{ a: 42 } < { b: 42 }`.
+    /// However, we cannot observe any difference between `{ a: 0, b: 0 }` and `{ b: 0, a: 0 }`,
+    /// as the natural order is used as opposed to insertion order.
+    /// Where insertion order is relevant,
+    /// a [`BuiltinValue::Array`] with `(key, value)` pairs can be used instead.
     Map { val: MapValue },
 }
 

crates/sats/src/sum_type_variant.rs

@@ -36,6 +36,11 @@ impl SumTypeVariant {
         }
     }
 
+    /// Returns a unit variant with `name`.
+    pub fn unit(name: impl AsRef<str>) -> Self {
+        Self::new_named(AlgebraicType::UNIT_TYPE, name)
+    }
+
     /// Returns the name of the variant.
     pub fn name(&self) -> Option<&str> {
         self.name.as_deref()

crates/sats/src/typespace.rs

@@ -11,14 +11,17 @@ use crate::{de::Deserialize, ser::Serialize};
 /// That is, this is the `Δ` or `Γ` you'll see in type theory litterature.
 ///
 /// We use (sort of) [deBrujin indices](https://en.wikipedia.org/wiki/De_Bruijn_index)
-/// to represent our type variables,
-/// but notably, these are given for the entire module
+/// to represent our type variables.
+/// Notably however, these are given for the entire module
 /// and there are no universal quantifiers (i.e., `Δ, α ⊢ τ | Δ ⊢ ∀ α. τ`)
 /// nor are there type lambdas (i.e., `Λτ. v`).
+/// See [System F], the second-order lambda calculus, for more on `∀` and `Λ`.
 ///
 /// There are however recursive types in SATs,
 /// e.g., `&0 = { Cons({ v: U8, t: &0 }), Nil }` represents a basic cons list
 /// where `&0` is the type reference at index `0`.
+///
+/// [System F]: https://en.wikipedia.org/wiki/System_F
 #[derive(Debug, Clone, Deserialize, Serialize)]
 #[sats(crate = crate)]
 pub struct Typespace {