Построение n-арного произведения со всеми значениями простого типа суммы

Question

Я работаю с библиотекой generics-sop. Я хочу написать значение со следующим типом:

values :: forall r. IsEnumType r => NP (K r) (Code r)

То есть для типов суммы, чьи конструкторы не имеют аргументов (IsEnumType) Я хочу производить н-арый продукт (NP), который содержит соответствующее значение конструктора в каждой точке.

Например, для типа

{-# LANGUAGE DeriveGeneric #-}

import qualified GHC.Generics as GHC
import Generics.SOP

data Foo = Bar
         | Baz
         deriving (GHC.Generic)

instance Generic Foo

Я хочу производить н-арый продукт

K Bar :* K Baz :* Nil 

Я считаю, что решение будет включать в себя преобразование n-арного продукта, несущего общие представления каждого конструктора, поэтому я написал это:

values :: forall r. IsEnumType r => NP (K r) (Code r)
values = liftA_NP (mapKK (to . SOP))  _

С помощью liftA_NP а также mapKK, Но я не уверен, как создавать общие представления сами.

Answer 1

Вы можете использовать существующие injections или же apInjs* функции.

С

apInjs'_NP :: SListI xs => NP f xs -> NP (K (NS f xs)) xs

Вы должны предоставить продукт аргументов функции, где в нашем общем случае каждый из компонентов будет применен к одному из конструкторов базового типа данных.

Но поскольку мы предполагаем тип перечисления, ни один из этих конструкторов не имеет аргументов, и мы можем предоставить пустой список аргументов везде!

values :: forall r . IsEnumType r => NP (K r) (Code r)
values =
  map_NP
    (mapKK (to . SOP))
    (apInjs'_NP
      (cpure_NP (Proxy @((~) '[])) Nil)
    )

Answer 2

Может быть, есть более простой способ сделать это, но мне удалось определить values используя вспомогательный класс типов POSN это в основном выполняет индукцию по спискам на уровне типов пустых списков на уровне типов:

values :: forall r c. (Generic r, Code r ~ c, POSN c) => NP (K r) c
values = liftA_NP (mapKK (to . SOP)) posn

-- products of sums of nil
class POSN xss where
    posn :: NP (K (NS (NP I) xss)) xss   

instance POSN '[] where
    posn = Nil

instance (SListI2 xss, POSN xss) => POSN ('[] ': xss) where
    posn = let previous = posn @xss
            in K (Z Nil) :* liftA_NP (mapKK S) previous

Внутренний NPс всегда Nilпотому что они соответствуют аргументам каждого конструктора, и никогда не бывает никаких аргументов.

Шаг индукции "добавляет один" к каждой из сумм остальной части списка, добавляет "ноль" в начало.

Пример использования:

ghci> :set -XTypeApplications
ghci> values @Foo
K Bar :* K Baz :* Nil