What

A programming language agnostic type construction and interchange language solidly grounded in mathematics. With Typedefs, you can:

• Define types;
• Define terms (values) of those types;
• Serialize and deserialize such types and terms.

These can then be interchanged between heterogeneous systems.

Why

We need a mathematically clean but useful type specification language without ad hoc features, edge cases and artificial limitations.

How

Typedefs allows you to define ADTs (Algebraic Data Types) in terms of least fixpoints of F-algebras, where the F's are polynomial functors:

• 0 void or the empty type
• 1 the unit type
• + co-products of types
• × products of types
• μ fixpoint operator

Project

https://github.com/typedefs

References

- [2010] Nicola Gambino, Joachim Kock
  Polynomial Functors and Polynomial Monads
  polynomials.pdf
  https://arxiv.org/abs/0906.4931