A programming language agnostic type construction and interchange language solidly grounded in mathematics. With Typedefs, you can:
We need a mathematically clean but useful type specification language without ad hoc features, edge cases and artificial limitations.
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 type1
the unit type+
co-products of types×
products of typesμ
fixpoint operator
https://github.com/typedefs
- [2010] Nicola Gambino, Joachim Kock Polynomial Functors and Polynomial Monads polynomials.pdf https://arxiv.org/abs/0906.4931