diff --git a/crates/sats/src/algebraic_type.rs b/crates/sats/src/algebraic_type.rs index c232f7c0b4..91be78888a 100644 --- a/crates/sats/src/algebraic_type.rs +++ b/crates/sats/src/algebraic_type.rs @@ -209,7 +209,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"), ]) } @@ -226,12 +226,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) -> 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 { diff --git a/crates/sats/src/algebraic_type/map_notation.rs b/crates/sats/src/algebraic_type/map_notation.rs index 433f483373..a446cbde8e 100644 --- a/crates/sats/src/algebraic_type/map_notation.rs +++ b/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; diff --git a/crates/sats/src/algebraic_value.rs b/crates/sats/src/algebraic_value.rs index 30b7a70df2..5afbf1384f 100644 --- a/crates/sats/src/algebraic_value.rs +++ b/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)`. diff --git a/crates/sats/src/bsatn.rs b/crates/sats/src/bsatn.rs index 7cfa9fcbb9..aa804e6b98 100644 --- a/crates/sats/src/bsatn.rs +++ b/crates/sats/src/bsatn.rs @@ -23,12 +23,12 @@ pub fn to_vec(value: &T) -> Result, 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::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 { from_reader(&mut &*bytes) } diff --git a/crates/sats/src/builtin_type.rs b/crates/sats/src/builtin_type.rs index cf42f7b17f..b409e7f6cb 100644 --- a/crates/sats/src/builtin_type.rs +++ b/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"), ]), diff --git a/crates/sats/src/builtin_value.rs b/crates/sats/src/builtin_value.rs index 88cb637127..e346874606 100644 --- a/crates/sats/src/builtin_value.rs +++ b/crates/sats/src/builtin_value.rs @@ -5,46 +5,57 @@ 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; -/// Totally ordered [`f64`]. +/// Totally ordered [`f64`] allowing all IEEE-754 floating point values. pub type F64 = decorum::Total; /// 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. @@ -52,8 +63,18 @@ pub enum BuiltinValue { /// 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`. + /// Maps are implemented internally as [`BTreeMap`]. + /// 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 }, } diff --git a/crates/sats/src/sum_type_variant.rs b/crates/sats/src/sum_type_variant.rs index 9713c718eb..e0565f17fd 100644 --- a/crates/sats/src/sum_type_variant.rs +++ b/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) -> Self { + Self::new_named(AlgebraicType::UNIT_TYPE, name) + } + /// Returns the name of the variant. pub fn name(&self) -> Option<&str> { self.name.as_deref() diff --git a/crates/sats/src/typespace.rs b/crates/sats/src/typespace.rs index 44581aa704..6cb27f07f9 100644 --- a/crates/sats/src/typespace.rs +++ b/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 {