add Predicate1, Refined1 for functor predicates

[raehik]

Draft for discussion and visibility. Based off https://github.com/raehik/refined/tree/typeable-constraints-tweak .

This allows us to define refinements over functors, where we are prohibited from accessing the internal type. Importantly, Refined1 p f a has safe instances for Functor and Traversable (given that f has the appropriate instance). These can simplify transforming refined types of certain forms.

In other words: usually when you have a Refined, you can't change it without re-asserting the predicate. But for a Refined1, you're welcome to change the internal elements as you like. You just can't touch the functor itself. So you may have a Refined1 [] p a, which is an [a] with a functor predicate p asserted. You may transform this to a Refined1 [] p b. But you may not add or remove elements or change the functor without re-asserting the predicate.

Some predicates were already functor predicates, with instances like Foldable t => Predicate p (t a). These are moved to Predicate1 e.g. Foldable t => Predicate1 p t. Original instances are maintained.

See #94 for earlier discussion.

Non-breaking change.

[raehik]

re @chessai

As is, this is a fairly small change, but I haven't added many unsafe helpers or utils. I appreciate they might mean a bunch of unwanted maintenance. What do you think?

[raehik]

My libs are sad not being updated due to this missing definition, so I'm releasing this branch as refined1 on Hackage. Eager to upstream parts or the whole when it's convenient.

[chessai]

This is still marked as draft, not sure if that's accurate.

I'm still sorting out my opinions on this. I'll need to ask some questions soon.

[raehik]

No worries. I've kept this as a draft because it's based off #98 (because I was using the branch as an override for this package). It's missing some potential unsafe utils, but I consider it ready regardless (this is an extension and they could be added as required).

[raehik]

Bump: Got round to cleaning up my code, this is being used in binrep here via my refined1 library fork, branch https://github.com/raehik/refined/tree/refined1-hackage

[raehik]

bump @chessai . tl;dr this works and I think it is useful and relevant, but probably experimental until we fill out more utilities.

I'm unmarking draft, but note that this PR is based off of #98 .

[raehik]

bump @chessai since I'm likely going to use this again soon (refined gives me a very clean way to design binary data schema and work with them without all the limitations)

[raehik]

bump @chessai I still believe this is well-founded and useful. rerefined's implementation feels natural to use, and adds minimal extra definitions. It alleviates one of the more irritating parts of using refinement types, which is not being able to do any transformations on a refined value. Transforming the a of an f a where the refinement is on the f is legal, so should be permitted (which Refined1 does, via Functor and Traversable instances).

[chessai]

Hey @raehik. How have you been finding using this code?

[chessai]

Can you rebase on top of current trunk? This looks mergeable to me. I thought there might be something cleaner, but the perfect is the enemy of the good.

[raehik]

Rebased onto master.

Apologies, I don't have much code or any small examples that use this. The main usage remains in Binrep.Type.Prefix.Count, where I define a foldable with a maximum size. Such a type has a sound Functor instance, but if defined with Refined I have to write it manually with unsafe refines. Refined1 gives me that Functor instance, so I can continue defining everything with refined/rerefined (and the library is much more simple thanks to it).

[raehik]

You're right in this being a little ugly. rerefined pretty much duplicates a bunch of definitions between Refined and Refined1. I can't think of a better approach either-- worse, I know that this is a common pattern (e.g. Generic1, To/FromJSON1), so my brain stops thinking past that. But the ugliness is limited to the internals, end use of Refined1 is nice and easy.

[chessai]

Thanks for this work :)

I'm sorry it took so long to merge. I let ideals stall me out.