Add new functionality to constrained generators #4113
Conversation
Added HasSpec Size instance Added operations And and Or to BoolFn
TimSheard
force-pushed
the
ts-recover-new-constraints
branch
from
0b2c524
to
73766d5
Compare
There was a problem hiding this comment.
A few things:
(1) It would be nice if this were four different PRs, one for the size stuff, one for all the renaming etc., one for the boolean stuff, and one for the EraClass stuff that I don't quite understand the reason for.
(2) I don't see what's gained from this Size exercise (esp. since I think at the moment it breaks things).
There was a problem hiding this comment.
Does this file belong in this PR? @lehins is in a better position to comment on what's going on here than me.
There was a problem hiding this comment.
In my opinion this whole file should be removed, but Tim likes to have it in the test suite for some reason. I don't have time to argue about its uselessness, so I choose not to argue about it.
| @@ -611,6 +652,11 @@ class | |||
| -- ∀ a. a `conformsTo` spec == a `conformsTo` constrained (\t -> toPreds t spec) | |||
| toPreds :: Term fn a -> TypeSpec fn a -> Pred fn | |||
|
|
|||
| -- | compute a SizeSpec, that bounds the size of what (genFromTypeSpec spec) can compute. | |||
There was a problem hiding this comment.
This is confusing. Does that mean the number of elements in the set of possible values, or does it mean the size of the values themselves? The latter assumes that every type has a size, which is a major change to the model that I would expect at least shows up in some constraint somewhere.
If it's the latter I would prefer this to be in it's own type class to avoid baking assumptions about types into HasSpec.
There was a problem hiding this comment.
C.f. Forallable and OrdLike for inspiration on the way to do this.
| type TypeSpec fn Float = NumSpec Float | ||
| emptySpec = emptyNumSpec | ||
| combineSpec = combineNumSpec | ||
| genFromTypeSpec = genFromNumSpec | ||
| conformsTo = conformsToNumSpec | ||
| toPreds = toPredsNumSpec | ||
| sizeOfTypeSpec = mempty | ||
|
|
||
| ------------------------------------------------------------------------ | ||
| -- Function universes | ||
| ------------------------------------------------------------------------ | ||
|
|
There was a problem hiding this comment.
Why was this moved elsewhere?
| @@ -382,45 +407,47 @@ data HOLE a b where | |||
|
|
|||
| toCtx :: | |||
There was a problem hiding this comment.
Adding the string argument here is not how the MonadGenError is meant to be used. The argument termstring appears to always be show on the Term argument at the callsites. If this is the case, then why not just add a show constraint? If this is not the case, consider adding the extra logging information in a call to explain at the call site of toCtx.
Either way, I would strongly prefer the use site to be wrapped in explain instead of this solution, as it pushes information down in the functions and makes them more complicated.
| @@ -562,6 +589,20 @@ typeSpec ts = TypeSpec ts mempty | |||
|
|
|||
| -- The HasSpec Class ------------------------------------------------------ | |||
|
|
|||
| -- | sizeOfSpec generalizes the method (sizeOfTypeSpec :: TypeSpec fn t -> SizeSpec) to (sizeOfSpec:: Spec fn t -> SizeSpec) | |||
There was a problem hiding this comment.
Can we move this function elsewhere? It would be nice if the The HasSpec Class banner is above the HasSpec class implementation.
| @@ -161,7 +171,7 @@ instance (Member (MapFn fn) fn, IsUniverse fn) => Functions (MapFn fn) fn where | |||
| , Evidence <- prerequisites @fn @(Map k v) -> | |||
| case spec of | |||
| MemberSpec [s] -> | |||
| typeSpec $ MapSpec s [] (equalSpec $ Set.size s) TrueSpec NoFold | |||
| typeSpec $ MapSpec s [] (exactSizeSpec $ setSize s) TrueSpec NoFold | |||
There was a problem hiding this comment.
Why not equalSpec??
|
|
||
| listSum :: Numbery a => Spec Fn [a] | ||
| listSum = constrained $ \as -> | ||
| 10 <=. sum_ as | ||
| Lit 10 <=. sum_ as |
There was a problem hiding this comment.
Needing Lit here is evidence that the interface has gotten worse. This is probably caused by the OVERLAPPABLE and INCOHERENT instances for Num Term, I would prefer if we didn't do this.
| data SetFn (fn :: [Type] -> Type -> Type) args res where | ||
| Subset :: Ord a => SetFn fn '[Set a, Set a] Bool | ||
| Disjoint :: Ord a => SetFn fn '[Set a, Set a] Bool | ||
| Member :: Ord a => SetFn fn '[a, Set a] Bool | ||
| Singleton :: Ord a => SetFn fn '[a] (Set a) | ||
| Union :: Ord a => SetFn fn '[Set a, Set a] (Set a) | ||
| Size :: Ord a => SetFn fn '[Set a] Int | ||
| Union :: Ord a => SetFn fn '[Set a, Set a] (Set a) -- HELP ME, I don't think this is usefull |
There was a problem hiding this comment.
Why would being able to specify things about the union not be useful?
| @@ -114,11 +114,11 @@ import Constrained qualified as C | |||
| type ConwayUnivFns = StringFn : DefaultFns | |||
| type ConwayFn = Fix (OneofL ConwayUnivFns) | |||
|
|
|||
| type IsConwayUniv fn = | |||
| type ConwayUniverse fn = | |||
There was a problem hiding this comment.
Can we have the changes to names, renaming, etc. in a separate PR. There are many things that need to be resolved about size and having a monster PR that touches everything in the codebase makes that very difficult.
| Term fn Bool -> | ||
| Term fn Bool | ||
| not_ = app notFn | ||
|
|
||
| and_ :: |
There was a problem hiding this comment.
Why not (&&.) and (||.) to be consistent with the rest of the interface?
|
Closing in favor of #4121 |
Added newtypes Size, SizeSpec, and class Sized to system.
Added HasSpec Size instance
Added operations And and Or to BoolFn
This PR tries to recover lost changes to Branch ts-new-constraints when Tim's computer failed.
Functionality is now in place, but the lost tests need to be recreated.
Description
Checklist
.cabalandCHANGELOG.mdfiles according to theversioning process.
.cabalfiles 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)CHANGELOG.mdfor the affected packages. New section is never added with the code changes. (See RELEASING.md)fourmolu(usescripts/fourmolize.sh)scripts/cabal-format.sh)hie.yamlhas been updated (usescripts/gen-hie.sh)