3 ms·
I don't think I have ever seen a mainstream language letting you design data types with a built-in normalization. The reason is that you normally have algebraic
by choeger 6y ago
I don't think I have ever seen a mainstream language letting you design data types with a built-in normalization. The reason is that you normally have algebraic, i.e., sum and product, types. In such constructions you would expect construction and deconstruction to compose to the identity function. The closest that comes to mind are languages that marry algebraic data types with OO programming (scala, maybe OCaml, F#). There you can have constructing functions but the normalized result would still be expressed as a plain ADT. I also don't think that GADT's help here, but I might be wrong.
In any case, it is an interesting proposition. In order to be non-trivial the type system would have to be able to express the constraints of the normal form.
- Smaug123 6y agoI think the most interesting design space is around not requiring normalisation. After all, if you have a normal form, you can probably represent it with sum and product types. Cubical Agda gives you this ability but it's really hard to use (as you might expect from one of the first attempts to create the functionality).