Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Newconstraints phase3, Add newtypes: Size, SizeSpec and class Sized. #4121

Merged
merged 5 commits into from Mar 14, 2024

Conversation

TimSheard
Copy link
Contributor

@TimSheard TimSheard commented Feb 27, 2024

This is a follow on PR. Originally rebased on top of PR #4120, it is now rebased on the current master, and 4120 has been closed.

Spec does 3 things.

  1. Adds generic size functions on numerous types with HasSpec instances, by adding Sized instances. Current
    instances include Int, Set, List, Map, and Size itself.
  2. Retracts the And opertor from BoolFn, which turned out to have some technical difficulties.
  3. Adds the methods 'cardinalTypeSpec' and 'cardinalTrueSpec', these allow any HasSpec instance to
    use the function cardinality :: HasSpec fn t => Spec fn t -> Spec fn Int.
    It computes bounds on the total number of possible solutions generated by 'genFromTypeSpec'
    This supports tighter (more accurate) bounds in a number of places.

Checklist

  • Commit sequence broadly makes sense and commits have useful messages
  • New tests are added if needed and existing tests are updated
  • When applicable, versions are updated in .cabal and CHANGELOG.md files according to the
    versioning process.
  • The version bounds in .cabal files for all affected packages are updated. If you change the bounds in a cabal file, that package itself must have a version increase. (See RELEASING.md)
  • All visible changes are prepended to the latest section of a CHANGELOG.md for the affected packages. New section is never added with the code changes. (See RELEASING.md)
  • Code is formatted with fourmolu (use scripts/fourmolize.sh)
  • Cabal files are formatted (use scripts/cabal-format.sh)
  • hie.yaml has been updated (use scripts/gen-hie.sh)
  • Self-reviewed the diff

@TimSheard TimSheard force-pushed the s-newconstaintsPhase3-addSize branch 6 times, most recently from 3844bd3 to 5be9268 Compare March 4, 2024 23:21
@TimSheard TimSheard force-pushed the s-newconstaintsPhase3-addSize branch from c194f4b to 50df72d Compare March 7, 2024 00:22
Copy link
Collaborator

@MaximilianAlgehed MaximilianAlgehed left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I have left some comments, but I haven't gone over all the changes to Base in detail yet. There is a lot of stuff around the Size stuff that already exists for Integer and the other numeric types. I think it would be wise to drop Size as a type, in favour of Integer (to avoid wrapping issues when computing cardinality for e.g. Word64).

libs/constrained-generators/src/Constrained/Base.hs Outdated Show resolved Hide resolved
libs/constrained-generators/src/Constrained/Base.hs Outdated Show resolved Hide resolved
libs/constrained-generators/src/Constrained/Base.hs Outdated Show resolved Hide resolved
libs/constrained-generators/src/Constrained/Base.hs Outdated Show resolved Hide resolved
libs/constrained-generators/src/Constrained/Base.hs Outdated Show resolved Hide resolved
libs/constrained-generators/src/Constrained/Test.hs Outdated Show resolved Hide resolved
libs/constrained-generators/src/Constrained/Test.hs Outdated Show resolved Hide resolved
libs/constrained-generators/src/Constrained/Univ.hs Outdated Show resolved Hide resolved
libs/constrained-generators/src/Constrained/Univ.hs Outdated Show resolved Hide resolved
libs/constrained-generators/src/Constrained/Univ.hs Outdated Show resolved Hide resolved
@MaximilianAlgehed
Copy link
Collaborator

After we've revamped Size I can take another look at the changes to Constrained.Base - they should be simpler then.

@TimSheard TimSheard force-pushed the s-newconstaintsPhase3-addSize branch from 50df72d to 9a9791a Compare March 8, 2024 01:00
@MaximilianAlgehed
Copy link
Collaborator

@TimSheard how do you feel about s/Size/Natural instead of Integer? Then the issues with subtraction etc. should be resolved? Possibly we might want to have another look at the Num instance for Term fn Natural if there is an issue with negate vs (-) there?

@lehins
Copy link
Contributor

lehins commented Mar 8, 2024

Possibly we might want to have another look at the Num instance for Term fn Natural if there is an issue with negate vs (-) there?

There is ugly issue with Num for Natural, which is why I usually suggest to avoid it. For example if f is a polymorphic reusable function that is potentially defined in another library:

ghci> let f = subtract (-1)
ghci> :t f
f :: Num a => a -> a
ghci> map f [10::Natural]
[*** Exception: arithmetic underflow

@TimSheard TimSheard force-pushed the s-newconstaintsPhase3-addSize branch from 9a9791a to bcd56e0 Compare March 8, 2024 14:13
@TimSheard
Copy link
Contributor Author

I am thinking that we make Size = Integer.
Now we have an instance of genFromSpec
genFromSpec :: Spec fn Integer -> GenT m Integer
But we write our own function
genFromSize :: Spec fn Integer -> GenT m Integer, that never generates an Integer less than 0,
and we use this function at appropriate places in our code.

@MaximilianAlgehed
Copy link
Collaborator

With that solution genFromSize = genFromSpec . geqSpec 0?

@TimSheard TimSheard force-pushed the s-newconstaintsPhase3-addSize branch from bcd56e0 to ca80f9e Compare March 8, 2024 19:56
@TimSheard
Copy link
Contributor Author

Yes, that would be right. Any take a look, I have swithced to Size = Integer

@TimSheard TimSheard force-pushed the s-newconstaintsPhase3-addSize branch from ca80f9e to 15c7e28 Compare March 8, 2024 22:48
libs/cardano-ledger-test/src/Test/Cardano/Ledger/STS.hs Outdated Show resolved Hide resolved
libs/constrained-generators/src/Constrained/Base.hs Outdated Show resolved Hide resolved
libs/constrained-generators/src/Constrained/Base.hs Outdated Show resolved Hide resolved
libs/constrained-generators/src/Constrained/Base.hs Outdated Show resolved Hide resolved
libs/constrained-generators/src/Constrained/Base.hs Outdated Show resolved Hide resolved
libs/constrained-generators/src/Constrained/Base.hs Outdated Show resolved Hide resolved
libs/constrained-generators/src/Constrained/Base.hs Outdated Show resolved Hide resolved
libs/constrained-generators/src/Constrained/Base.hs Outdated Show resolved Hide resolved
libs/constrained-generators/src/Constrained/Base.hs Outdated Show resolved Hide resolved
@TimSheard TimSheard force-pushed the s-newconstaintsPhase3-addSize branch from 3e0a6ae to 303a73a Compare March 12, 2024 19:32
TimSheard and others added 4 commits March 13, 2024 12:26
Added Num (NumSpec fn Integer) and Num (Spec fn Int) instances.
Added Num (NumSpec Integer) tests
Added (HasSpec fn t) method 'typeSpecOpt'
Revoved the synonym: type Size = Intgeger
Addressed all other conversations.

Co-authored-by: Maximilian Algehed <MaximilianAlgehed@users.noreply.github.com>
@TimSheard TimSheard force-pushed the s-newconstaintsPhase3-addSize branch from 303a73a to ea1b76f Compare March 13, 2024 19:27
@MaximilianAlgehed MaximilianAlgehed marked this pull request as ready for review March 14, 2024 11:20
@MaximilianAlgehed MaximilianAlgehed merged commit 89243fc into master Mar 14, 2024
14 of 16 checks passed
@neilmayhew neilmayhew deleted the s-newconstaintsPhase3-addSize branch March 28, 2024 02:21
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

None yet

4 participants