Updating an n-ary product from sop-core with a compatible sum

user_1364288 0
Viewed 48

I'm working with the sop-core library, and I want to write a function with the following type:

patch :: NS I xs -> NP Maybe xs -> NP Maybe xs

xs is a type-level list of types like '[Int,Char,Bool]. I is an identity functor. NS I xs is an n-ary sum type. NP Maybe xs is an n-ary product where each component may or may not exist.

patch should take the value from the n-ary sum and fill the corresponding slot of the n-ary product, overwriting it if it already exists. For example:

patched :: NP Maybe '[Int,Char,Bool]
patched = patch (Z (I 3)) (Nothing :* Nothing :* Nothing :* Nil)
-- patched == Just 3 :* Nothing :* Nothing :* Nil

I suspect the solution might involve the injections function, but I'm stumped.

type-level-computation algebraic-data-types haskell
1 Answers

The solution did not require injections after all, but the expand_NS function which converts a sum into a product by filling the non-matching components of the product with a default value.

The trick is to build a product of setters that we can apply to the original record using liftA2_NP. When we expand the sum, the non-matching components are filled with the identity function. But we overwrite the matching component with the value in the sum.

First we need this auxiliary type

newtype Mendo a = Mendo { getMendo :: Maybe a -> Maybe a }

and the code for patch would be:

patch :: forall xs. SListI xs => NS I xs -> NP Maybe xs -> NP Maybe xs
patch piece =
  let mendos :: NP Mendo xs -- product of setters
      mendos = expand_NS (Mendo id) (liftA_NS (\(I x) -> Mendo (\_ -> Just x)) piece)
   in liftA2_NP (\(Mendo f) x -> f x) mendos
user_13642880
Related