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

Question

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

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

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

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

{-# LANGUAGE DeriveGeneric #-}

import qualified GHC.Generics as GHC
import Generics.SOP

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

instance Generic Foo

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

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