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