Written a helper: wrapper that combines refined+unrefined views over a type into a single newtype

[raehik]

Hi, first off I want to say cheers for the library! I like that refined allows me to take the "parse, don't validate" concept (really about retaining a proof of validation) to the extreme and apply it even to cases where I can't/don't want to change the underlying type.

For a recent project where I didn't want to redefine a data type, I wrote an extension that lets me switch between refined and unrefined "views" without rewrapping in a separate newtype. In context it produced a nice pattern (was able to define a binary schema in the types and predicates), didn't add too much cruft, and is a good candidate for Generic stuff if I knew how to write that.

If you don't mind: is this something you've thought of before? Is it something you'd consider throwing into refined or think is worthwhile as an extra lib? I'm asking because refined is half-pattern, half-library, and this idea feels like even more of a coding pattern, so maybe it's a poor fit for this library. I'll probably get round to publishing it eventually regardless, but wanted to know if you might have any insights!

The module is Refined.WithRefine (I'm rubbish at naming things). The main definitions:

-- | A wrapper over a type @a@ with a predicate @p@, and a type-level "switch"
--   indicating whether the predicate is enforced or not.
newtype WithRefine (ps :: PredicateStatus) p a = WithRefine { unWithRefine :: a }

-- | Is the associated predicate currently enforced or not?
data PredicateStatus
  = Enforced   -- ^ value is read-only
  | Unenforced -- ^ value is read-write

---

-- | Some data type that has a specific binary schema.
--
-- I parse/serialize as binary using @Entry 'Enforced ByteString@.
-- For JSON I relax the predicates, and use @Entry 'Unenforced Text@ instead.
-- This is used inside another type as a null-padded list, also done via predicates.
data Entry (ps :: PredicateStatus) a = Entry
  { entryIndex  :: Word32
  , entryType   :: EntryType
  , entryName   :: WithRefine ps (NullPadTo 64) a
  , entryScript :: WithRefine ps (NullPadTo 32) a
  }

[chessai]

I will offer thoughts on this soon. One note when reviewing your linked code: you probably don't want to newtype-derive Generic. Generic should almost always be stock-derived.

[raehik]

One note when reviewing your linked code: you probably don't want to newtype-derive Generic. Generic should almost always be stock-derived.

Thank you, I didn't know about or notice that!

[chessai]

The problem is that Generic is used to track precise information about a type, somewhat nominally, i.e. Rep Int ~ Rep (Sum Int) should not hold.

[raehik]

While splitting out big projects into libraries, I've uploaded this to Hackage as refined-with.

[raehik]

A small patch to the core of refined actually lets me do the same without writing lots of extras:

-- previous:
newtype Refined (p :: k) x = Refined x

-- change:
{-# LANGUAGE TypeSynonymInstances #-}
newtype WithRefine (v :: Validation) (p :: k) x
data Validation = Validated | Unvalidated -- (I'm bad at naming)
type Refined p x = WithRefine 'Validated p x

Then adding a couple of functions to use the new definition. Code that uses the original Refined p x works the same (apparently). I'm not certain this is a good idea, but it's useful for solving my problem!

[raehik]

I eventually figured out the pattern I was aiming for and spun it out as its own library at https://github.com/raehik/strongweak . Instead of a newtype, "switchable" fields are wrapped in a type family:

type family SW (s :: Strength) a :: Type where
    SW 'Strong a = a
    SW 'Weak   a = Weak a

type family Weak (a :: Type) :: Type
type instance Weak (Refined p a) = a

Then with typeclasses for strengthening and weakening & some generics, I get the "dual" representations from a single definition that I wanted, plus no WithRefine or Refined wrappers for the weak representation. So, I'll close this issue. Thank you for the help & the fantastic library! (I'd still appreciate polykinded predicates!)