generics-sop: lifting a polymorphic action into a product

Question

Using the generics-sop library, I have the following function:

f :: (Applicative m) => (forall b. m (ref b)) -> m (NP I '[ref x1, ref x2])
f act =
  sequence_NP (act :* act :* Nil)

How would I generalize this to a n-product i.e. with act in every position, polymorphic to the return type?

The relevant definitions are:

data NP :: (k -> Type) -> [k] -> Type where
  Nil  :: NP f '[]
  (:*) :: f x -> NP f xs -> NP f (x ': xs)

sequence_NP :: (SListI xs, Applicative f) => NP f xs -> f (NP I xs)

The obvious approach is to use pure_NP

pure_NP :: forall f xs. SListI xs => (forall a. f a) -> NP f xs

as follows:

f :: (Applicative m, _) => (forall b. m (ref b)) -> m (NP I refs)
f act =
  sequence_NP (pure_NP act)

but this doesn't compile:

• Could not deduce: a ~ ref b0
  from the context: (Applicative m, All Top refs)
    bound by the inferred type of
               f :: (Applicative m, All Top refs) =>
                    (forall b. m (ref b)) -> m (NP I refs)
    at /home/ari/fcm-deepref-experiment/test/QuickCheck.hs:(163,1)-(164,27)
  ‘a’ is a rigid type variable bound by
    a type expected by the context:
      forall a. m a
    at /home/ari/fcm-deepref-experiment/test/QuickCheck.hs:164:24-26
  Expected type: m a
    Actual type: m (ref b0)
• In the first argument of ‘pure_NP’, namely ‘act’
  In the first argument of ‘sequence_NP’, namely ‘(pure_NP act)’
  In the expression: sequence_NP (pure_NP act)
• Relevant bindings include
    act :: forall b. m (ref b)
      (bound at /home/ari/fcm-deepref-experiment/test/QuickCheck.hs:163:3)
    f :: (forall b. m (ref b)) -> m (NP I refs)
      (bound at /home/ari/fcm-deepref-experiment/test/QuickCheck.hs:163:1)

because it expects all the acts to be of the same type, but they're not: it has a polymorphic type.

I'm assuming I should be using cpure_NP,

cpure_NP :: forall c xs proxy f. All c xs => proxy c -> (forall a. c a => f a) -> NP f xs

the constrained version pf pure_NP, but I can't work out how to set up the constraint.

Answer 1

{-# LANGUAGE FlexibleContexts, FlexibleInstances, DataKinds, MultiParamTypeClasses, RankNTypes, ScopedTypeVariables, TypeApplications #-}

import Data.Proxy
import Data.SOP
import Data.SOP.NP

f :: forall m ref xs. (Applicative m, All (C ref) xs) => (forall b. m (ref b)) -> m (NP I xs)
f act = sequence_NP (cpure_NP (Proxy @(C ref)) act)

-- C ref a: "there exists b such that (a ~ ref b)"
-- We can actually define b using the following type family:
type family Snd a where
  Snd (f a) = a

class (a ~ ref (Snd a)) => C ref a
instance (a ~ ref (Snd a)) => C ref a


-- Example
f2 :: Applicative m => (forall b. m (ref b)) -> m (NP I '[ref a1, ref a2])
f2 = f

---

Another more rudimentary solution is the following one, with explicit recursion instead of SOP combinators (whose purpose is to make that recursion reusable, but it's easier to understand this implementation if you're unfamiliar with SOP).

{-# LANGUAGE FlexibleContexts, FlexibleInstances, DataKinds, MultiParamTypeClasses, RankNTypes, ScopedTypeVariables, TypeApplications, TypeOperators, PolyKinds #-}

import Control.Applicative
import Generics.SOP

class Iter ref xs where
  iter :: Applicative m => (forall b. m (ref b)) -> m (NP I xs)

instance Iter ref '[] where
  iter _ = pure Nil

instance Iter ref xs => Iter ref (ref b ': xs) where
  iter act = liftA2 (:*) (I <$> act) (iter act)

f2 :: Applicative m => (forall b. m (ref b)) -> m (NP I '[ref a1, ref a2])
f2 = iter