-
Notifications
You must be signed in to change notification settings - Fork 53
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Add FromNatural trait in
package-base (#2926)
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`.- Loading branch information
1 parent
0e27e9a
commit d859a03
Showing
5 changed files
with
24 additions
and
5 deletions.
There are no files selected for viewing
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
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -1,14 +1,21 @@ | ||
| module Juvix.Builtin.V1.Nat; | ||
|
|
||
| import Juvix.Builtin.V1.Trait.Natural open public; | ||
| import Juvix.Builtin.V1.Trait.FromNatural open public; | ||
| import Juvix.Builtin.V1.Nat.Base open hiding {+; *; div; mod} public; | ||
| import Juvix.Builtin.V1.Nat.Base as Nat; | ||
|
|
||
| {-# specialize: true, inline: case #-} | ||
| instance | ||
| fromNaturalNatI : FromNatural Nat := | ||
| mkFromNatural@{ | ||
| fromNat (x : Nat) : Nat := x | ||
| }; | ||
|
|
||
| {-# specialize: true, inline: case #-} | ||
| instance | ||
| naturalNatI : Natural Nat := | ||
| mkNatural@{ | ||
| + := (Nat.+); | ||
| * := (Nat.*); | ||
| fromNat (x : Nat) : Nat := x | ||
| }; |
12 changes: 12 additions & 0 deletions
12
include/package-base/Juvix/Builtin/V1/Trait/FromNatural.juvix
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
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,12 @@ | ||
| module Juvix.Builtin.V1.Trait.FromNatural; | ||
|
|
||
| import Juvix.Builtin.V1.Nat.Base open using {Nat}; | ||
|
|
||
| trait | ||
| type FromNatural A := | ||
| mkFromNatural { | ||
| builtin from-nat | ||
| fromNat : Nat -> A | ||
| }; | ||
|
|
||
| open FromNatural public; |
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
Submodule juvix-stdlib
updated
5 files
| +9 −2 | Stdlib/Data/Field.juvix | |
| +9 −2 | Stdlib/Data/Int.juvix | |
| +1 −0 | Stdlib/Data/Nat.juvix | |
| +1 −0 | Stdlib/Trait.juvix | |
| +3 −0 | Stdlib/Trait/FromNatural.juvix |
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