Yes, this is right. You can already experiment in ocaml, as Denis
Berthod suggested, by adding abstract types by hand instead of having
constants in the initial environment.

You can also embed the natural numbers in Ocaml's type system by declaring the following two types:

type 'a s
type z

Granted 32 would be written z s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s s which may or may not be considered legible. But at least there is no absolute need for infinitely many constants.