Refined1 p f x for refinements on functor types

[raehik]

I have the following predicate which asserts that the number of elements in some Foldable f => f a can be safely represented by the given type:

data CountPrefix pfx
type CountPrefixed pfx = Refined (CountPrefix pfx)

instance (KnownNat (Max pfx), Foldable f, Typeable pfx)
  => Predicate (CountPrefix pfx) (f a) where
    validate p a
      | Foldable.length a <= natValInt @(Max pfx) = Nothing
      | otherwise = throwRefineOtherException (typeRep p) $
          "thing too big for length prefix type"

This works nicely. However, I find myself writing a bunch of boilerplate Functor/Traversable instances for newtypes over instantiations of f a, which inevitably include doing a reallyUnsafeRefine at the end. This is safe, because I assert the predicate using Foldable f -- it's not really a predicate on a at all.

We could define another refinement type for Type -> Type-kinded types, where a can't be accessed:

newtype Refined1 (p :: k) f a = Refined1 { unRefined1 :: f a }
    deriving (Functor, Foldable) via f
    deriving stock Traversable

class Predicate1 p f where validate1 :: Proxy p -> f a -> Bool

unrefine1 :: Refined1 p f a -> f a
unrefine1 = unRefined1

unsafeRefine1 :: f a -> Refined1 p f a
unsafeRefine1 = Refined1

refine1 :: forall p f a. Predicate1 p f => f a -> Maybe (Refined1 p f a)
refine1 fa = if validate1 (Proxy @p) fa then Just (Refined1 fa) else Nothing

Now I can get refinements on functors & list-likes with less boilerplate and no reallyUnsafeRefine.

What do you think? Is this useful, enough to add to the library?

[raehik]

SizeGreaterThan, SizeLessThan and SizeEqualTo all have a Predicate1. (The Predicate instance can be recovered as validate = validate1.) Ascending and Descending don't, because they operate on the values inside.

[raehik]

Testing over at https://github.com/raehik/refined/tree/refined1 .

[chessai]

It honestly feels like you could do something with Existentials and/or Quantified constraints here, without a new class and type.

[raehik]

I think that would work for defining Predicate1s. But it doesn't allow me to recover Functor/Traversable for types refined with such predicates. I still have to derive it myself each time using reallyUnsafeRefine and frantically reminding myself "the predicate has no access to a".

Would type Refined p = Refined1 p Identity with a few tweaked definitions work? (I feel it won't, but worth a mention.)

I'm not sure how I would solve this with existentials. Also, the new class and type are fairly lightweight (the various coercions are the most work). I had an inkling that Aeson did something similar with FromJSON1, so felt empowered.

[raehik]

I don't have a good MWE for this, but it did fix my issue. Given a type

newtype AW32Pairs f a = AW32Pairs
  { unAW32Pairs :: CountPrefixed Word8 [] (f a) }

I can now safely derive Functor and Traversables like

instance Functor f => Functor (AW32Pairs f) where
    fmap f = AW32Pairs . fmap (fmap f) . unAW32Pairs

(I didn't check this, adapted from a different type.)

This is certainly useful for code which works with refinement types for parsing/serializing (which they are really good for).

I'm not sure how I'd do this another way-- I think I need a concrete type like Refined1 so I can give it the relevant instances that Refined can't have. It would be nice not to repeat all the constructors and destructors though. This is at the bottom of a stack of libs I write, so I might for now release it as an extension lib.

[chessai]

I'd need time to sit down and think about this and your other ideas. This does seem useful though.

[chessai]

I think we can add some kind of namespace like Refined.Experimental.*, where we can add this. I'd like to iterate on a design. I've been holding off because I couldn't think of a good one.

[raehik]

I think we can add some kind of namespace like Refined.Experimental.*, where we can add this.

That would be neat. I would have a suggestion for such a namespace: a predicate simplifier. I wrote a naive one for rerefined at Rerefined.Simplify. It can reduce Boolean identity laws and do a tiny bit of local reasoning about numeric relational predicates. One could use it to catch trivially-simplifiable predicates at compilation, which are probably better avoided.