使用“generics-sop”创建求和构造函数值

Question

在 中，给定其位置（索引）及其参数的generics-sop乘积值，一般创建求和构造函数值的惯用方法是什么？

例如考虑，

-- This can be any arbitrary type.
data Prop = Name String | Age Int | City String
  deriving stock (GHC.Generic)
  deriving anyclass (Generic)

-- Manually creating a sum constructor value (3rd constructor)
mkCityPropManual :: SOP I (Code Prop)
mkCityPropManual = from $ City "Chennai"

mkCityPropGeneric :: SOP I (Code Prop)
mkCityPropGeneric = SOP $ mkSumGeneric $ I ("Chennai" :: String) :* Nil

-- Generically creating it, independent of type in question
mkSumGeneric :: _
mkSumGeneric = undefined

你如何定义mkSumGeneric？

---

根据https://github.com/kosmikus/SSGEP/blob/master/LectureNotes.pdf我认为注入类型在这里可能有用，但这显然只适用于构造所有求和构造函数，或构建同质求和列表（以会塌陷）。

---

一种幼稚的方法是定义一个类型类，如下所示，但我感觉有更好的方法。

-- `XS` is known to be in `Code (a s)` per the class constraint this function is in
-- For complete code, see: https://github.com/Plutonomicon/plutarch/commit/a6343c99ba11390cc9dfa9c73c600a9d04cdf08c#diff-84126a8c05d2752f0764676cdcd6b10d826c154a6d4797b4334937e8a8e831f2R212-R230
  mkSOP :: NP I '[xs] -> SOP I (Code (a s))
  mkSOP = SOP . mkSum' @sx @'[xs] @rest

class MkSum (before :: [[Type]]) (x :: [Type]) (xs :: [[Type]]) where
  mkSum' :: NP I x -> NS (NP I) (Append (Reverse before) (x ': xs))

instance MkSum '[] x xs where
  mkSum' = Z
instance MkSum '[p1] x xs where
  mkSum' = S . Z
instance MkSum '[p1, p2] x xs where
  mkSum' = S . S . Z
instance MkSum '[p1, p2, p3] x xs where
  mkSum' = S . S . S . Z
instance MkSum '[p1, p2, p3, p4] x xs where
  mkSum' = S . S . S . S . Z
instance MkSum '[p1, p2, p3, p4, p5] x xs where
  mkSum' = S . S . S . S . S . Z
instance MkSum '[p1, p2, p3, p4, p5, p6] x xs where
  mkSum' = S . S . S . S . S . S . Z

---

编辑：我已经做了MkSum一般化（见下文），但有些东西告诉我，有一种更惯用的方法可以使用generics-sop组合器来完成这一切。那会是什么？

class MkSum (idx :: Fin n) xss where
  mkSum :: NP I (TypeAt idx xss) -> NS (NP I) xss

instance MkSum 'FZ (xs ': xss) where
  mkSum = Z
instance MkSum idx xss => MkSum ( 'FS idx) (xs ': xss) where
  mkSum v = S $ mkSum @_ @idx @xss v

type family Length xs :: N.Nat where
  Length '[] = 'N.Z
  Length (x ': xs) = 'N.S (Length xs)

class Tail' (idx :: Fin n) (xss :: [[k]]) where
  type Tail idx xss :: [[k]]

instance Tail' 'FZ xss where
  type Tail 'FZ xss = xss

instance Tail' idx xs => Tail' ( 'FS idx) (x ': xs) where
  type Tail ( 'FS idx) (x ': xs) = Tail idx xs
instance Tail' idx xs => Tail' ( 'FS idx) '[] where
  type Tail ( 'FS idx) '[] = TypeError ( 'Text "Tail: index out of bounds")

class TypeAt' (idx :: Fin n) (xs :: [[k]]) where
  type TypeAt idx xs :: [k]

instance TypeAt' 'FZ (x ': xs) where
  type TypeAt 'FZ (x ': xs) = x

instance TypeAt' ( 'FS idx) (x ': xs) where
  type TypeAt ( 'FS idx) (x ': xs) = TypeAt idx XS

---

编辑：改编下面 Eitan 的答案（不适用于非产品类型），我MkSum进一步简化为：

{- |
Infrastructure to create a single sum constructor given its type index and value.

- `mkSum @0 @(Code a) x` creates the first sum constructor;
- `mkSum @1 @(Code a) x` creates the second sum constructor;
- etc.

It is type-checked that the `x` here matches the type of nth constructor of `a`.
-}
class MkSum (idx :: Nat) (xss :: [[Type]]) where
  mkSum :: NP I (IndexList idx xss) -> NS (NP I) xss

instance {-# OVERLAPPING #-} MkSum 0 (xs ': xss) where
  mkSum = Z

instance
  {-# OVERLAPPABLE #-}
  ( MkSum (idx - 1) xss
  , IndexList idx (xs ': xss) ~ IndexList (idx - 1) xss
  ) =>
  MkSum idx (xs ': xss)
  where
  mkSum x = S $ mkSum @(idx - 1) @xss x

-- | Indexing type-level lists
type family IndexList (n :: Nat) (l :: [k]) :: k where
  IndexList 0 (x ': _) = x
  IndexList n (x : xs) = IndexList (n - 1) xs

Answer 1

给定其位置（索引）及其参数的乘积值，一般创建求和构造函数值的惯用方法是什么？

我可能会尝试这样的事情：

>>> :set -XKindSignatures -XDataKinds -XTypeOperators -XTypeApplications -XScopedTypeVariables -XAllowAmbiguousTypes
>>> :set -XFlexibleContexts -XFlexibleInstances -XMultiParamTypeClasses -XFunctionalDependencies -XUndecidableInstances

>>> import Data.Kind
>>> import Generics.SOP
>>> import GHC.TypeLits

>>> :{
class Summand (n :: Nat) as a | n as -> a where
  summand :: a -> NS I as
instance {-# OVERLAPPING #-}
  Summand 0 (a ': as) a where
    summand = Z . I
instance {-# OVERLAPPABLE #-}
  Summand (n-1) as a => Summand n (b ': as) a where
    summand = S . summand @(n-1)
:}

>>> :{
[ summand @0 "0"
, summand @1 1
, summand @2 2
] :: [NS I '[String, Double, Int]]
:}
[Z (I "0"),S (Z (I 1.0)),S (S (Z (I 2)))]

编辑I更一般地说，抽象出任何解释的身份f :: k -> Type

:set -XPolyKinds -XDataKinds -XTypeOperators -XTypeApplications -XScopedTypeVariables -XAllowAmbiguousTypes -XGADTs
:set -XFlexibleContexts -XFlexibleInstances -XMultiParamTypeClasses -XFunctionalDependencies -XUndecidableInstances
:set -XDerivingStrategies -XDeriveGeneric -XDeriveAnyClass


>>> :{
class Summand (n :: Nat) as a | n as -> a where
  summand :: f a -> NS f as
instance {-# OVERLAPPING #-}
  Summand 0 (a ': as) a where
    summand = Z
instance {-# OVERLAPPABLE #-}
  Summand (n-1) as a => Summand n (b ': as) a where
    summand = S . summand @(n-1)

summandI :: forall n a as. Summand n as a => a -> NS I as
summandI = summand @n . I

summandGeneric
  :: forall n b a as
   . (IsProductType a as, Generic b, Summand n (Code b) as)
  => a -> b
summandGeneric = to . SOP . summand @n . productTypeFrom
:}

>>> data Foo = Bar {bar1 :: Char, bar2 :: Int} | Baz deriving stock (Show, GHC.Generic) deriving anyclass (Generic)
>>> summandGeneric @0 ('1',2) :: Foo
Bar {bar1 = '1', bar2 = 2}
>>> summandGeneric @1 () :: Foo
Baz

>>> :{
data Prop = Name String | Age Int | City String
  deriving stock (Show, GHC.Generic)
  deriving anyclass (Generic)
:}
>>> summandGeneric @1 @Prop (I 30)
Age 30
>>> summandGeneric @0 @Prop (I "John")
Name "John"