Hacker News Reader

Comment by rm445 | Hacker News Reader

Scheme has rational numbers in its number tower, is that the kind of thing you mean?

(= 22/7 44/14) #t

No. To satisfy the complaint, you would have to be able to create the rational-number type yourself in userspace, and moreover it would have to be built in such a way that you didn't need to worry much about cancellation.

Analogously, Rust or F# have type systems which allow you to build the Option type yourself easily: there is no magic behind them, and you can just write down whatever sum type you want. Similarly, we want to be able to build arbitrary quotient types (not just of numbers, but of general sets with equivalence relations) ourselves.

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.

I 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).

Reply on news.ycombinator.com