search

anoma / juvix

A language for intent-centric and declarative decentralised applications
https://docs.juvix.org
GNU General Public License v3.0
457 stars 53 forks source link

Add FromNatural trait in `package-base` #2926

Closed paulcadman closed 3 months ago

paulcadman commented 3 months ago

This PR adds FromNatural to package-base. The change is backwards compatible for existing Juvix code so we don't need to make a new version of package-base. The new trait is unused, it will be integrated in subsequent PRs.

FromNatural trait

The FromNatural trait has the following definition.

trait
type FromNatural A :=
  mkFromNatural {
    builtin from-nat
    fromNat : Nat -> A
};

Natural trait changes

The Natural trait is changed to remove its fromNat field and add a new instance field for FromNatural A.

juvix-stdlib changes

FromNatural instances are added for Int and Field in the standard library.

Rationale

The FromNatural trait will be used for the Bytes type.

We want the following properties for Byte:

  1. Values of the Bytes type should be assignable from a non-negative numeric literal.
  2. We don't want to implement + and * for Bytes.

Currently, in order for a type to have property 1. it must have an instance of Natural so property 2. can't be satisfied.

To solve this we split the from-nat builtin from the Natural trait into a new trait FromNatural.

paulcadman commented 3 months ago

Agreed with @janmasrovira to try to use instance fields instead of an instance coercion from Natural to FromNat.