Constructing a n-ary product with all the values of a simple sum type

Question

I'm working with the generics-sop library. I want to write a value with the following type:

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

That is, for sum types whose constructors don't have any arguments (IsEnumType) I want to produce an n-ary product (NP) which contains the corresponding constructor value at each point.

For example, for the type

{-# LANGUAGE DeriveGeneric #-}

import qualified GHC.Generics as GHC
import Generics.SOP

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

instance Generic Foo

I want to produce the n-ary product

K Bar :* K Baz :* Nil 

I believe the solution will involve transforming an n-ary product carrying generic representations of each constructor, so I wrote this:

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

Using liftA_NP and mapKK. But I'm not sure how to produce the generic representations themselves.

Answer 1

You can use the existing injections or apInjs* functions.

With

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

you have to supply a product of function arguments where, in our generic case, each of the components will be applied to one of the constructors of the underlying datatype.

But because we are assuming an enumeration type, none of these constructors have any arguments, and we can supply the empty list of arguments everywhere!

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

Answer 2

Maybe there is a simpler way to do it, but I managed to define values by using an auxiliary typeclass POSN that basically performs induction over type-level lists of empty type-level lists:

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

The inner NPs are always Nil, because they correspond to the arguments of each constructor, and there are never any arguments.

The inductive step "adds one" to each of the sums of the rest of the list, the prepends a "zero" at the head.

An example of use:

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