Création d'une valeur de constructeur de somme à l'aide de `generics-sop`.

Question

Sur generics-sop Si l'on veut créer une valeur de constructeur de somme, quelle est la manière idiomatique de créer génériquement une valeur de constructeur de somme ? donné à la fois sa position (index) et la valeur du produit de ses args ?

Par exemple, considérez,

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

Comment définissez-vous mkSumGeneric ?

---

Par https://github.com/kosmikus/SSGEP/blob/master/LectureNotes.pdf J'ai pensé que les types d'injection pourraient être utiles ici, mais apparemment cela n'est utile que pour construire tous les constructeurs de somme, ou pour construire une liste de somme homogène (à réduire).

---

Une approche naïve consiste à définir une classe de type comme ci-dessous, mais j'ai le sentiment qu'il existe une meilleure méthode.

-- `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 : J'ai fait MkSum (voir ci-dessous), mais quelque chose me dit qu'il y a une façon plus idiomatique de faire tout cela en utilisant generics-sop combinateurs. Qu'est-ce que ce serait ?

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 : En adaptant la réponse d'Eitan ci-dessous (qui ne fonctionne pas pour les types de non-produits), j'ai simplifié MkSum plus comme :

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

quelle est la manière idiomatique de créer génériquement un constructeur de somme étant donné à la fois sa position (indice) et la valeur du produit de ses args ?

Je pourrais essayer quelque chose comme ça :

>>> :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 Plus généralement, abstraction faite de l'identité I pour toute interprétation f :: k -> Type

>>> :{
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 as a. Summand n as a => a -> NS I as
summandI = summand @n . I

summandGeneric
  :: forall n a b 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