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:
0void or the empty type
1the unit type
+co-products of types
×products of types
-  Nicola Gambino, Joachim Kock Polynomial Functors and Polynomial Monads polynomials.pdf https://arxiv.org/abs/0906.4931