Crates.io | sigma-types |
lib.rs | sigma-types |
version | 0.3.7 |
source | src |
created_at | 2024-12-22 09:13:24.90656+00 |
updated_at | 2025-02-28 04:32:05.641365+00 |
description | Types checked for an invariant. |
homepage | https://github.com/wrsturgeon/sigma-types |
repository | https://github.com/wrsturgeon/sigma-types |
max_upload_size | |
id | 1491789 |
size | 107,486 |
This crate lets you explicitly represent structures like sorted vectors as types of their own.
Deref
, AsRef
, and Borrow
:
if x
implements x.foo(..)
,
then a sigma type s
wrapping x
automatically implements s.foo(..)
.debug_assert!(..)
s
(and inevitably missing some necessary checks).
This is an extremely simple crate,
but its main aim is to silently insert
nothing more or less than each necessary check,
and to allow libraries to credibly promise
invariants about their functions' return values
with an easily unwrappable, lightweight type
that disappears in release builds.repr(transparent)
):
Wrapping a T
in Sigma<T, ..>
creates a type that uses
exactly the same binary representation as T
;
all it does is add an extra PhantomData
field.no_std
(and no alloc
):
all features, including error messages (via ::core::fmt::Display
),
work without the standard library and without heap allocation.Some languages, like Coq, implement type systems that offer sigma types, which represent a term (say, A) alongside another term (say, B) whose type can depend on the value of A. Since the type of B can depend on the value of A, the type of B often represents a proof that some property holds of this particular value for A. (If exactly how is unclear and you have a few minutes and a mind to be blown, see the Curry-Howard correspondence.)
We implement a subset of sigma types in which B represents a decidable proposition.
To decide whether a proof exists to inhabit the type of B (which isn't directly represented),
the programmer supplies a Rust function that takes the value of A and returns a Result
.
invariant
or something more clear?invariant
is already a similar library,
but it requires std
and alloc
, and it uses larger structs that run checks in release builds.
That's fine, but I have a different use-case, and this aims to be more generally applicable.
Plus, sigma types are theoretically interesting, and I'd like to evangelize a bit.