Strict types AST and typelib implementation

Protobufs for functional programming

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.

Strict Types Library

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.

Contributing

CONTRIBUTING.md

License

The libraries are distributed on the terms of Apache 2.0 license.