Special Nats

[pdavidow]

AFAIK, Nat >= 1
But I also want to specify Nat >= 0; as well as Nat >= 2.
Is this currently possible? If not, please consider as enhancements.

[re-xyr]

Note that in plutus-numeric, Naturals are always greater than 0 and Positives are always greater than 1, so the only thing we don't have is naturals >= 2. It appears to me that it's pretty ad-hoc (unlike >=0 and >=1, which are "canonical" in some senses). It may be possible for us to have some data NatGreaterThan (n :: GHC.TypeLits.Natural), but I'm not sure if that will be easy enough to use. What are your use cases for such a type?

[kozross]

It's also worth mentioning that on-chain, we can't have 'type-level tags' of this form at all.

[pdavidow]

Note that in plutus-numeric, Naturals are always greater than 0 and Positives are always greater than 1, so the only thing we don't have is naturals >= 2. It appears to me that it's pretty ad-hoc (unlike >=0 and >=1, which are "canonical" in some senses). It may be possible for us to have some data NatGreaterThan (n :: GHC.TypeLits.Natural), but I'm not sure if that will be easy enough to use. What are your use cases for such a type?

My use-case is a fancy datatype purely on the offchain side, for which I can easily wrap a newtype on Positive with a smart constructor.

data EqualIntervalSpec = EqualIntervalSpec PosGE2 Duration
newtype PosGE2 = PosGE2 Positive
mkPosGE2 :: Positive -> Maybe PosGE2

Minimum interval amount is 2

[pdavidow]

Naturals are always greater than 0 and Positives are always greater than 1

Where is this documented? I somehow missed it.

[kozross]

Naturals are always greater than 0 and Positives are always greater than 1

Where is this documented? I somehow missed it.

Here and here.

Insofar as a 'greater than 1' numeric data type is concerned, it's unlikely we'll be implementing such a thing soon.

[re-xyr]

Where is this documented? I somehow missed it.

Sorry! I meant "greater than or equal to". Naturals are >=0 and Positives are >= 1.