generics-sop：将多态动作提升到产品中

问题描述

使用 generics-sop 库，我有以下功能：

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

我如何将其推广到 n-product，即在每个位置都有 act，多态返回类型？

相关定义是：

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)

显而易见的方法是使用 pure_NP

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

如下：

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

但这不能编译：

• 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)

因为它希望所有的 act 都是相同的类型，但它们不是：它有一个多态类型。

我假设我应该使用 cpure_NP，

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

约束版本 pf pure_NP，但我不知道如何设置约束。

解决方法

{-# 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

---

另一个更基本的解决方案是以下解决方案，使用显式递归而不是 SOP 组合器（其目的是使递归可重用，但如果您不熟悉 SOP，则更容易理解此实现）。

{-# LANGUAGE FlexibleContexts,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