Refined derives Typeable and Data

[yaitskov]

No description provided.

[raehik]

Note that Typeable is automatically derived for all data types (as of like GHC 8.10 or before), so that instance derivation is not needed.

[yaitskov]

Note that Typeable is automatically derived for all data types (as of like GHC 8.10 or before), so that instance derivation is not needed.

Thanks for quick feedback. I reverted Typeable deriving.
I build with GHC-9.10.1 and see no warnings.
In the previous GHC versions I remember that Data required Typeable and added it by habbit.

[yaitskov]

Could you give an estimate for next release?

[raehik]

I'm unclear on what this could accomplish currently. In particular, I don't think predicates should have instances, since they should never be instantiated on the term level in the first place. (My rewrite rerefined doesn't even provide constructors.)

May I ask what problem you're trying to solve @yaitskov ? Does a Data instance for Refined end up being useful?
And might any other maintainers have thoughts on this? ping @chessai , @nikita-volkov

[chessai]

I am against this primarily because these typeclasses are used to inspect and modify runtime values, and like @raehik says, it's not clear that predicates should ever be constructed.

[yaitskov]

You are an author of rerefined and maintain refined - this is conflict of interest ;)

[nikita-volkov]

I don't see any use for it either but I might be missing something. @yaitskov can you provide a motivating information on why you think it's needed?

[yaitskov]

GHC requires all record fields to have Data instance to derive data for the record type.
Library generates records full of Refined fields.

{-# LANGUAGE TemplateHaskell #-}
module CallSpecs where
import System.Process.Quick

$(genCallSpec
  [TrailingHelpValidate, SandboxValidate]
  "cp"
  (   VarArg @(Refined (InFile "hs") FilePath) "source"
  .*. VarArg @(Refined (OutFile "*") FilePath) "destination"
  .*. HNil
  )
 )

main :: IO ()
main = callProcess $ Cp $(refinedTH "app.hs") $(refinedTH "app.bak")

These record types have Arbitrary instance too.
The fields might be a path to file or folder - gmapM extracts them from randomly generated record - to create files or validate that these file objects have been created.

[nikita-volkov]

Thanks! @raehik @chessai What do you guys think? Seems reasonable to me.

We should also discuss the downsides of adding this letting us conclude whether it's worth it. Also possibly find dedicated solutions for some of them. E.g., one downside that I see is that we'll thus be making Data essentially a required constraint for all predicates including custom ones. Does anyone see more downsides?

@yaitskov Do you have any ideas how your problem could be solved without necessarily adding the Data instances?

[yaitskov]

An alternative to gmapM is to use TH, which should be faster than Data driven solution and the library already seats up to the ears in Q monad, but it requires more development and maintenance; performance gain is not critical.

As for now I successfully merged modified version of refined as an internal library thanks to its tiny code base.
So library release is not block by refined.
Doing fork just for adding Data instances is overkill.

Another improvement for refined library, that crawled through my head, but left unimplemented, is smarter Arbitrary instance, because And/Or/Not predicate combinators are not scalable - the arbitrary Refined method for a complex expression cannot succeeded after 100 attempts.
Using SMT solver via sbv library as a fallback after 100 unsuccessful attempts should improve applicability of Arbitrary instance. Predicate class should add another method coupled with validate one for expressing constraint in symbolic form.
sbv with z3 is pretty quick in generating strings matching file path regex.

[raehik]

Sorry for my late response here.
@nikita-volkov I think instance Data a => Data (Refined p a) (that GHC derives automatically) is sensible.
I don't believe such instances are required on the predicates. (And by not including them, I don't see any downsides.) A quick test:

data Test = Test (Refined (LessThan 1) Int) deriving Data

didn't need me to define instance Data (LessThan n) to compile. Assuming you're relying on GHC's automatic Data instances, I don't see why you would need them. @yaitskov do you have any more info there? (I would test your library, but building is taking time.)

Regarding the Arbitrary instance for Refined-- yes, it would be great to have a more sophisticated solution. It would be very cool to interface with an SMT solver. We could provide SMT-based implementations for most of our relational (less than etc.) and logical (and/or) predicates. It'd be up to users to implement for their own predicates. Probably best as a standalone library, like how Arbitrary instances are often separated from their base definitions.

[yaitskov]

Sorry for my late response here. @nikita-volkov I think instance Data a => Data (Refined p a) (that GHC derives automatically) is sensible. I don't believe such instances are required on the predicates. (And by not including them, I don't see any downsides.) A quick test:

data Test = Test (Refined (LessThan 1) Int) deriving Data

didn't need me to define instance Data (LessThan n) to compile. Assuming you're relying on GHC's automatic Data instances, I don't see why you would need them. @yaitskov do you have any more info there? (I would test your library, but building is taking time.)

Now taking into fact that Refined data constructor is exposed in Refined.Unsafe.Type this PR seems redundant, but I tried today and I was not able to succeed.

Library location https://github.com/yaitskov/quick-process

Regarding the Arbitrary instance for Refined-- yes, it would be great to have a more sophisticated solution. It would be very cool to interface with an SMT solver. We could provide SMT-based implementations for most of our relational (less than etc.) and logical (and/or) predicates. It'd be up to users to implement for their own predicates. Probably best as a standalone library, like how Arbitrary instances are often separated from their base definitions.