Creating a sum constructor value using `generics-sop`

Question

In generics-sop, what is the idiomatic way to generically create a sum constructor value given both its position (index) and the product value of its args?

For example consider,

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

How do you define mkSumGeneric?

---

Per https://github.com/kosmikus/SSGEP/blob/master/LectureNotes.pdf I figured the injection types might be useful here, but that's apparently only useful for either constructing all sum constructors, or building a homogenous sum list (to be collapsed).

---

A naive approach is to define a type-class like below, but I have a feeling there is a better way.

-- `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

---

EDIT: I've made MkSum general (see below), but something tells me that there is a more idiomatic way to do this all using generics-sop combinators. What would that be?

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

---

EDIT: Adapting Eitan's answer below (which doesn't work for non-product types), I've simplified MkSum further as:

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

what is the idiomatic way to generically create a sum constructor value given both its position (index) and the product value of its args?

I might try something like this:

>>> :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)))]

---

EDIT More generally, abstract out the identity I for any interpretation 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"