Skip to content

Commit

Permalink
sats: address george's review (#107)
Browse files Browse the repository at this point in the history
  • Loading branch information
Centril authored Jul 31, 2023
1 parent 38e3692 commit 2a43923
Show file tree
Hide file tree
Showing 8 changed files with 99 additions and 67 deletions.
9 changes: 2 additions & 7 deletions crates/sats/src/algebraic_type.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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"),
])
}

Expand All @@ -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<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 {
Expand Down
2 changes: 1 addition & 1 deletion crates/sats/src/algebraic_type/map_notation.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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;

Expand Down
12 changes: 9 additions & 3 deletions crates/sats/src/algebraic_value.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down Expand Up @@ -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)`.
Expand Down
4 changes: 2 additions & 2 deletions crates/sats/src/bsatn.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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)
}
Expand Down
72 changes: 37 additions & 35 deletions crates/sats/src/builtin_type.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand All @@ -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),
}

Expand Down Expand Up @@ -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"),
]),
Expand Down
55 changes: 38 additions & 17 deletions crates/sats/src/builtin_value.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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 },
}

Expand Down
5 changes: 5 additions & 0 deletions crates/sats/src/sum_type_variant.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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()
Expand Down
7 changes: 5 additions & 2 deletions crates/sats/src/typespace.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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 {
Expand Down

0 comments on commit 2a43923

Please sign in to comment.