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

Question

使用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-产品，即每个位置都有 act，多态为 return 类型？

相关定义为：

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，但我不知道如何设置约束。

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

另一个更基本的解决方案是下面的解决方案，它使用显式递归而不是 SOP 组合器（其目的是使该递归可重用，但如果您不熟悉 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

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

generics-sop: lifting a polymorphic action into a product

haskell

metaprogramming

existential-type

ghc-generics