This is a set of libraries for working with abstract syntax trees and libraries of strict types – type system made with category theory which ensures provable properties and bounds for the in-memory and serialized type representation.
Strict types is a formal notation for defining and serializing generalized algebraic data types (GADT) in a deterministic and confined way. It is developed with type theory in mind.
Strict Types are:
- schema-based (with the schema being strict encoding notation),
- semantic, i.e. defines types not just as they are layed out in memory, but also depending on their meaning,
- deterministic, i.e. produces the same result for a given type,
- portabile, i.e. can run on ahy hardware architecture and OS, including low-performant embedded systems,
- confined, i.e. provides guarantees and static analysis on a maximum size of the typed data,
- formally verifiabile.
To learn more about strict encoding read the spec.
Strict types works with type definitions. It allows:
- static analysis of data types, like
- defining semantic type ids;
- specifying exact memory layout;
- type equivalence in terms of semantics and memory layout;
- size of serialized data
- composing types into type libraries;
- versioning type libraries basing on the semantic types;
The library allows to generate & compile strict type libraries (STL) from rust
types implementing StrictEncoding trait -- and ensures that the
deserialization with StrictDecode follows the same memory and semantic layout.
The library is able to reflect on itself, producing replica of its rust data types in strict types system.
Strict types library id:
stl:9KALDYR8Nyjq4FdMW6kYoL7vdkWnqPqNuFnmE9qHpNjZ#lagoon-rodent-option
Import this lib by putting in the file header
import lagoon_rodent_option_9KALDYR8Nyjq4FdMW6kYoL7vdkWnqPqNuFnmE9qHpNjZ as StrictTypes
Source code can be found in [stl/StrictTypes.sty] file.
The libraries are distributed on the terms of Apache 2.0 license.