Type-level `Nat`

Questions
1

I see in the stdlib documentation there is a data Nat.

Am I correct in thinking these are not Peano numerals i.e. data Nat = Zero | Succ Nat, but something internal to the compiler?

Otherwise, how can I create a value of this type? The constructors don’t appear to be exported.

I also tried looking through the code-base, and I can see a lot of references to TypeLevelNat.

2 Likes
2

Short answer: Nat isn’t a type you can construct. It’s a “kind” used by the compiler to make sure that Numeric types are well-defined. There are no values of type Nat, but when an integer appears in a type expression, the integer has kind Nat.

Long answer: When you write a Numeric type, you need to specify the scale. For example:

  • Numeric 10 is the type of decimal numbers with 10 digits after the decimal point.
  • Numeric 20 is the type of decimal numbers with 20 digits after the decimal point.
  • Numeric 30 is the type of decimal numbers with 30 digits after the decimal point.
  • etc.

So Numeric n is a well-formed type, but what sort of thing is the number n in this type expression? Because it occurs inside a type expression, we could call it a “type”, but it doesn’t behave like other types. For example, there’s no such thing as a value of of type 10, and you can’t create functions from the type 10, etc.

Instead, to distinguish n from the usual sort of type, we say that n has a different “kind”. Its kind is Nat. Any numbers appearing in type expressions will have kind Nat, and Numeric expects a "type of kind Nat" as its only type argument.

Does this mean DAML supports integer arithmetic at the type level? No, because Nat is very limited. It exists in its current form only to make Numeric work, so it has some big limitations, and I would recommend against using Nat in your own DAML projects.

Here’s some of the limitations of the Nat kind:

  • Nat “types” must range between 0 and 37 inclusive.*
  • There are no (type-level) arithmetic operations for kind Nat.
  • You cannot convert a Nat type to an Int value directly.**
  • Support for Nat in DAML-LF is even more limited.

*- The range limitation is in place because Numeric is similarly limited: you can only have Numeric 0 through Numeric 37.

**- The indirect solution to this is to use a NumericScale constraint, which gives you access to the numericScale function, which converts the type-level number into an integer value. This is mostly intended for library authors who need to work generically in the scale of a Numeric.

4 Likes