Support for HKD?

[edsko]

For a client project I ended up writing the code below.. not sure if some form and/or subset of this should live in generics-sop. (#163 is somewhat related here, although I bypass the issue by having both IsAppOf and IsFlipAppOf and just have both as constraints, but it's a bit ugly).

import Data.Kind
import Data.SOP hiding (hsequence, hsequence')
import Data.SOP.Constraint
import Generics.SOP hiding (Code, to, from, hsequence, hsequence')
import Generics.SOP qualified as SOP

{-------------------------------------------------------------------------------
  Code
-------------------------------------------------------------------------------}

data Skolem (a :: Type)

type Code (a :: (Type -> Type) -> Type) = StripTypeArg (SOP.Code (a Skolem))

type family StripTypeArg (code :: [[Type]]) :: [[Type]] where
  StripTypeArg '[]         = '[]
  StripTypeArg (xs ': xss) = StripTypeArg' xs ': StripTypeArg xss

type family StripTypeArg' (prod :: [Type]) :: [Type] where
  StripTypeArg' '[]       = '[]
  StripTypeArg' (x ': xs) = StripSkolem x ': StripTypeArg' xs

type family StripSkolem (x :: Type) :: Type where
  StripSkolem (Skolem x) = x

{-------------------------------------------------------------------------------
  From/to generic representation
-------------------------------------------------------------------------------}

class    x ~ f y => IsAppOf f x y
instance x ~ f y => IsAppOf f x y

type AllIsAppOf a f = AllZip2 (IsAppOf f) (SOP.Code (a f)) (Code a)

from :: forall a f.
     ( Generic (a f)
     , AllIsAppOf a f
     )
  => a f -> SOP f (Code a)
from = SOP.htrans (Proxy @(IsAppOf f)) unI . SOP.from

class    y ~ f x => IsFlipAppOf f x y
instance y ~ f x => IsFlipAppOf f x y

type AllIsFlipAppOf a f = AllZip2 (IsFlipAppOf f) (Code a) (SOP.Code (a f))

to :: forall a f.
     ( Generic (a f)
     , AllIsFlipAppOf a f
     )
  => SOP f (Code a) -> a f
to = SOP.to . SOP.htrans (Proxy @(IsFlipAppOf f)) I

{-------------------------------------------------------------------------------
  Combinators
-------------------------------------------------------------------------------}

uninitialized :: forall a f.
     ( Generic (a f)
     , HasDatatypeInfo (a Skolem)
     , AllIsFlipAppOf a f
     , SOP.Code (a Skolem) ~ '[Head (SOP.Code (a Skolem)) ]
     )
  => ( forall x.
           ModuleName
        -> DatatypeName
        -> ConstructorName
        -> Maybe FieldName
        -> f x
     )
  -> a f
uninitialized mkF =
    to $ SOP $ Z $ auxData (datatypeInfo (Proxy @(a Skolem)))
  where
    auxData :: DatatypeInfo '[xs] -> NP f (StripTypeArg' xs)
    auxData (ADT     m d (c :* Nil) _) = auxConstr m d c
    auxData (Newtype m d c)            = auxConstr m d c

    auxConstr :: forall xs.
         ModuleName
      -> DatatypeName
      -> ConstructorInfo xs
      -> NP f (StripTypeArg' xs)
    auxConstr m d (Constructor c) = auxRecord @xs m d c (hpure (K Nothing))
    auxConstr m d (Infix c _ _)   = auxRecord @xs m d c (hpure (K Nothing))
    auxConstr m d (Record c fs)   = auxRecord @xs m d c (hmap getFieldName fs)

    auxRecord :: forall xs.
         ModuleName
      -> DatatypeName
      -> ConstructorName
      -> NP (K (Maybe FieldName)) xs
      -> NP f (StripTypeArg' xs)
    auxRecord _ _ _ Nil         = Nil
    auxRecord m d c (K f :* fs) = mkF m d c f :* auxRecord m d c fs

    getFieldName :: FieldInfo x -> K (Maybe FieldName) x
    getFieldName (FieldInfo n) = K (Just n)

hsequence ::
     ( Generic (a f)
     , Generic (a I)
     , AllIsAppOf a f
     , AllIsFlipAppOf a I
     , All SListI (Code a)
     , Applicative f
     )
  => a f -> f (a I)
hsequence = fmap to . SOP.hsequence . from

hsequence' ::
     ( Generic (a (f :.: g))
     , Generic (a g)
     , AllIsAppOf a (f :.: g)
     , AllIsFlipAppOf a g
     , All SListI (Code a)
     , Applicative f
     )
  => a (f :.: g) -> f (a g)
hsequence' = fmap to . SOP.hsequence' . from

[edsko]

With my rekindled love for QuantifiedConstraints, can actually make these function signatures a lot cleaner:

{-# LANGUAGE UndecidableSuperClasses #-}
-- | Thin layer around generics-sop to support HDK types
--
-- TODO: This should be merged to generics-sop.
--
-- Intended for qualified import.
module Network.GRPC.Util.HKD (
    -- * Translate to and from generic representation
    Code
  , from
  , to
    -- * Combinators
  , uninitialized
  , hsequence
  , hsequence'
  ) where

import Data.Kind
import Data.SOP hiding (hsequence, hsequence')
import Data.SOP.Constraint
import Generics.SOP hiding (Code, to, from, hsequence, hsequence')
import Generics.SOP qualified as SOP

{-------------------------------------------------------------------------------
  Code
-------------------------------------------------------------------------------}

data Skolem (a :: Type)

type Code (a :: (Type -> Type) -> Type) = StripTypeArg (SOP.Code (a Skolem))

type family StripTypeArg (code :: [[Type]]) :: [[Type]] where
  StripTypeArg '[]         = '[]
  StripTypeArg (xs ': xss) = StripTypeArg' xs ': StripTypeArg xss

type family StripTypeArg' (prod :: [Type]) :: [Type] where
  StripTypeArg' '[]       = '[]
  StripTypeArg' (x ': xs) = StripSkolem x ': StripTypeArg' xs

type family StripSkolem (x :: Type) :: Type where
  StripSkolem (Skolem x) = x

{-------------------------------------------------------------------------------
  From/to generic representation
-------------------------------------------------------------------------------}

class    x ~ f y => IsAppOf f x y
instance x ~ f y => IsAppOf f x y

class    y ~ f x => IsFlipAppOf f x y
instance y ~ f x => IsFlipAppOf f x y

class    ( Generic (a f)
         , All SListI (Code a)
         , AllZip2 (IsAppOf f) (SOP.Code (a f)) (Code a)
         , AllZip2 (IsFlipAppOf f) (Code a) (SOP.Code (a f))
         ) => AllIsAppOf a f
instance ( Generic (a f)
         , All SListI (Code a)
         , AllZip2 (IsAppOf f) (SOP.Code (a f)) (Code a)
         , AllZip2 (IsFlipAppOf f) (Code a) (SOP.Code (a f))
         ) => AllIsAppOf a f

type IsHKD a = forall f. AllIsAppOf a f

from :: forall a f. IsHKD a => a f -> SOP f (Code a)
from = SOP.htrans (Proxy @(IsAppOf f)) unI . SOP.from

to :: forall a f. IsHKD a => SOP f (Code a) -> a f
to = SOP.to . SOP.htrans (Proxy @(IsFlipAppOf f)) I

{-------------------------------------------------------------------------------
  Combinators
-------------------------------------------------------------------------------}

uninitialized :: forall a f.
     ( HasDatatypeInfo (a Skolem)
     , IsHKD a
     , SOP.Code (a Skolem) ~ '[Head (SOP.Code (a Skolem)) ]
     )
  => ( forall x.
           ModuleName
        -> DatatypeName
        -> ConstructorName
        -> Maybe FieldName
        -> f x
     )
  -> a f
uninitialized mkF =
    to $ SOP $ Z $ auxData (datatypeInfo (Proxy @(a Skolem)))
  where
    auxData :: DatatypeInfo '[xs] -> NP f (StripTypeArg' xs)
    auxData (ADT     m d (c :* Nil) _) = auxConstr m d c
    auxData (Newtype m d c)            = auxConstr m d c

    auxConstr :: forall xs.
         ModuleName
      -> DatatypeName
      -> ConstructorInfo xs
      -> NP f (StripTypeArg' xs)
    auxConstr m d (Constructor c) = auxRecord @xs m d c (hpure (K Nothing))
    auxConstr m d (Infix c _ _)   = auxRecord @xs m d c (hpure (K Nothing))
    auxConstr m d (Record c fs)   = auxRecord @xs m d c (hmap getFieldName fs)

    auxRecord :: forall xs.
         ModuleName
      -> DatatypeName
      -> ConstructorName
      -> NP (K (Maybe FieldName)) xs
      -> NP f (StripTypeArg' xs)
    auxRecord _ _ _ Nil         = Nil
    auxRecord m d c (K f :* fs) = mkF m d c f :* auxRecord m d c fs

    getFieldName :: FieldInfo x -> K (Maybe FieldName) x
    getFieldName (FieldInfo n) = K (Just n)

hsequence :: (IsHKD a, Applicative f) => a f -> f (a I)
hsequence = fmap to . SOP.hsequence . from

hsequence' :: (IsHKD a, Applicative f) => a (f :.: g) -> f (a g)
hsequence' = fmap to . SOP.hsequence' . from

[phadej]

It feels you want Generic1 or some kind of kind-generics-sop. The above look ad-hoc and hacky and stretching generics-sop beyond its capabilities

[kosmikus]

I haven't looked at this in detail yet, but some of my (unmerged) work on supporting Generic1 or GenericN is in the https://github.com/well-typed/generics-sop/tree/genericn branch. Perhaps this should be compared, and perhaps some form of it / parts of it should be merged. If it's needed occasionally, it's not necessarily great if everybody has to reinvent it for themselves.