Add FromNatural trait in package-base
#2926
Merged
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
paulcadman
force-pushed
the
FromNatural-trait
branch
from
c03e766 to
2025370
Compare
paulcadman
force-pushed
the
FromNatural-trait
branch
from
968db25 to
aed9495
Compare
|
Agreed with @janmasrovira to try to use instance fields instead of an instance coercion from Natural to FromNat. |
paulcadman
force-pushed
the
FromNatural-trait
branch
from
832acc5 to
3981b91
Compare
paulcadman
force-pushed
the
FromNatural-trait
branch
from
6dc4105 to
e173061
Compare
paulcadman
force-pushed
the
FromNatural-trait
branch
from
e173061 to
304e2d3
Compare
This updates the juvix-stdlib to contain: * anoma/juvix-stdlib#111 * anoma/juvix-stdlib#114
The FromNatural trait will be used for the Bytes type. We want the following properties for Byte: 1. Values of the Bytes type to be assignable from a non-negative numeric literal. 2. We don't want to implement + and * for it. 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`. A coercion instance is defined between Natural and FromNatural so you don't need to write instances for both traits. For this PR the new `FromNatural` trait is unused. I will make the changes to juvix-stdlib to use the new V2 modules when I incorporate compiler changes for the Bytes type. This change is backwards compatible for existing Juvix code so we don't need to make a new Juvix.Builtin.V2 path in package-base.
janmasrovira
force-pushed
the
FromNatural-trait
branch
from
304e2d3 to
d511b12
Compare
janmasrovira
approved these changes
Jul 31, 2024
janmasrovira
pushed a commit
to anoma/juvix-stdlib
that referenced
this pull request
Aug 5, 2024
Adds `FromNatural` instances for `Int` and `Field`. Used by: * anoma/juvix#2926 A temporary version of juvix-quickcheck is used that works with the Natural/FromNatural changes.
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This PR adds
FromNaturalto 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.FromNaturaltraitThe
FromNaturaltrait has the following definition.Naturaltrait changesThe
Naturaltrait is changed to remove itsfromNatfield and add a new instance field forFromNatural A.juvix-stdlib changes
FromNaturalinstances are added forIntandFieldin the standard library.Rationale
The
FromNaturaltrait will be used for the Bytes type.We want the following properties for Byte:
Currently, in order for a type to have property 1. it must have an instance of
Naturalso property 2. can't be satisfied.To solve this we split the
from-natbuiltin from theNaturaltrait into a new traitFromNatural.