¿Cómo puedo producir un tipo de etiqueta para cualquier tipo de datos para usar con DSum, sin Template Haskell?

generic-programming

Question

fondo

Quiero escribir un código de biblioteca, que internamente utiliza DSum para manipular el tipo de datos de un usuario. DSum requiere un tipo de ''etiqueta'' que tiene un argumento de tipo único. Sin embargo, quiero que mi código funcione con cualquier tipo de concreto antiguo. Entonces, me gustaría simplemente tomar el tipo de usuario y producir automáticamente el tipo de etiqueta. He hecho una pregunta muy similar aquí. ¿Cómo puedo producir programáticamente este tipo de datos desde el otro? y obtuve una gran respuesta. Esa respuesta se basa en TH, principalmente para que pueda crear declaraciones de alto nivel. Sin embargo, en realidad no me importa la declaración de nivel superior, y preferiría evitar el TH si es posible.

pregunta

[Cómo] puedo escribir, con alguna técnica de programación genérica, un tipo de datos

data Magic t a ...

donde se da algún tipo de suma arbitraria, por ejemplo

data SomeUserType = Foo Int | Bar Char | Baz Bool String

Magic SomeUserType es equivalente a este tipo de ''etiqueta'' que se puede usar con DSum?

data TagSomeUserType a where
  TagFoo :: TagSomeUserType Int
  TagBar :: TagSomeUserType Char
  TagBaz :: TagSomeUserType (Bool, String)

Answer 1

A diferencia de lo que algunos han afirmado, es perfectamente sensato (y de hecho bastante sencillo, con la biblioteca correcta - generics-sop ) definir dicho tipo. Esencialmente toda la maquinaria es provista por esta biblioteca ya:

{-# LANGUAGE PatternSynonyms, PolyKinds, DeriveGeneric #-} 

import Generics.SOP 
import qualified GHC.Generics as GHC 
import Data.Dependent.Sum

data Tup2List :: * -> [*] -> * where 
  Tup0 :: Tup2List () ''[] 
  Tup1 :: Tup2List x ''[ x ] 
  TupS :: Tup2List r (x '': xs) -> Tup2List (a, r) (a '': x '': xs) 

newtype GTag t i = GTag { unTag :: NS (Tup2List i) (Code t) }

El tipo GTag es lo que llamas Magic . La ''magia'' real ocurre en la familia de tipos de Code , que calcula la representación genérica de un tipo, como una lista de listas de tipos. El tipo NS (Tup2List i) xs significa que, precisamente para uno de xs , Tup2List i tiene, esto es simplemente una prueba de que una lista de argumentos es isomorfa a alguna tupla.

Todas las clases que necesita pueden derivarse:

data SomeUserType = Foo Int | Bar Char | Baz Bool String 
  deriving (GHC.Generic, Show) 
instance Generic SomeUserType

Puede definir algunos sinónimos de patrones para las etiquetas válidas para este tipo:

pattern TagFoo :: () => (x ~ Int) => GTag SomeUserType x 
pattern TagFoo = GTag (Z Tup1) 

pattern TagBar :: () => (x ~ Char) => GTag SomeUserType x 
pattern TagBar = GTag (S (Z Tup1)) 

pattern TagBaz :: () => (x ~ (Bool, String)) => GTag SomeUserType x 
pattern TagBaz = GTag (S (S (Z (TupS Tup1))))

y una prueba simple:

fun0 :: GTag SomeUserType i -> i -> String 
fun0 TagFoo i = replicate i ''a'' 
fun0 TagBar c = c : [] 
fun0 TagBaz (b,s) = (if b then show else id) s 

fun0'' = /(t :& v) -> fun0 t v 

main = mapM_ (putStrLn . fun0'' . toTagVal) 
          [ Foo 10, Bar ''q'', Baz True "hello", Baz False "world" ] 

Como esto se expresa en términos de una función de tipo genérico, puede escribir operaciones genéricas sobre etiquetas. Por ejemplo, exists x . (GTag tx, x) exists x . (GTag tx, x) es isomorfo a t para cualquier Generic t :

type GTagVal t = DSum (GTag t) I 

pattern (:&) :: forall (t :: * -> *). () => forall a. t a -> a -> DSum t I
pattern t :& a = t :=> I a     

toTagValG_Con :: NP I xs -> (forall i . Tup2List i xs -> i -> r) -> r 
toTagValG_Con Nil k = k Tup0 () 
toTagValG_Con (I x :* Nil) k = k Tup1 x
toTagValG_Con (I x :* y :* ys) k = toTagValG_Con (y :* ys) (/tp vl -> k (TupS tp) (x, vl))

toTagValG :: NS (NP I) xss -> (forall i . NS (Tup2List i) xss -> i -> r) -> r 
toTagValG (Z x) k = toTagValG_Con x (k . Z)
toTagValG (S q) k = toTagValG q (k . S)

fromTagValG_Con :: i -> Tup2List i xs -> NP I xs 
fromTagValG_Con i Tup0 = case i of { () -> Nil } 
fromTagValG_Con x Tup1 = I x :* Nil 
fromTagValG_Con xs (TupS tg) = I (fst xs) :* fromTagValG_Con (snd xs) tg 

toTagVal :: Generic a => a -> GTagVal a 
toTagVal a = toTagValG (unSOP $ from a) ((:&) . GTag)

fromTagVal :: Generic a => GTagVal a -> a 
fromTagVal (GTag tg :& vl) = to $ SOP $ hmap (fromTagValG_Con vl) tg 

En cuanto a la necesidad de Tup2List , es necesario por el simple motivo de que representa un constructor de dos argumentos ( Baz Bool String ) como una etiqueta sobre una tupla de (Bool, String) en su ejemplo.

También podría implementarlo como

type HList = NP I -- from generics-sop 

data Tup2List i xs where Tup2List :: Tup2List (HList xs) xs

que representa los argumentos como una lista heterogénea, o incluso más simple

newtype GTag t i = GTag { unTag :: NS ((:~:) i) (Code t) }
type GTagVal t = DSum (GTag t) HList  

fun0 :: GTag SomeUserType i -> HList i -> String 
fun0 TagFoo (I i :* Nil) = replicate i ''a'' 
fun0 ...

Sin embargo, la representación de la tupla tiene la ventaja de que las tuplas únicas se ''proyectan'' al único valor que está en la tupla (es decir, en lugar de (x, ()) ). Si representa argumentaciones de la manera obvia, funciones como fun0 deben coincidir con el patrón para recuperar el valor único almacenado en un constructor.

Answer 2

No estoy seguro de que pueda prescindir de TH ya que, como se señala en los comentarios, aún necesita hacer un tipo al final del día. Como señala Benjamin, probablemente esté buscando una data family .

Lo que llamas Magic , me referiré a Tagged .

Aquí está el código ajustado que necesitará para tag.hs

{-# LANGUAGE TemplateHaskell #-}

module Tag where

import Language.Haskell.TH

makeTag :: Name -> Name -> DecsQ
makeTag name tag = do
    -- Reify the data declaration to get the constructors.
    -- Note we are forcing there to be no type variables...
    (TyConI (DataD _ _ [] _ cons _)) <- reify name

    pure [ DataInstD [] tag [(ConT name), (VarT (mkName "a"))] Nothing (tagCon <$> cons) [] ]
  where
  -- Given a constructor, construct the corresponding constructor for
  -- Tag GADT
  tagCon :: Con -> Con
  tagCon (NormalC conName args) =
    let tys = fmap snd args
        tagType = foldl AppT (TupleT (length tys)) tys
    in GadtC [mkName ("Tag" ++ nameBase conName)] []
             (AppT (AppT (ConT tag) (ConT name)) tagType)

Y, un caso de uso de muestra (hasta llegar a algo relacionado con DSum ):

{-# LANGUAGE TemplateHaskell, GADTs, TypeFamilies #-}
module Test where

import Data.Dependent.Sum
import Data.Functor.Identity
import Tag

-- Some data types
data SomeUserType1 = Foo Int | Bar String
data SomeUserType2 = Fooo Int | Baar Char | Baaz Bool String
data SomeAwkUserType = Foooo Int

-- Data family for all Tagged things
data family Tagged t a

-- Generated data family instances
makeTag ''''SomeUserType1 ''''Tagged
makeTag ''''SomeUserType2 ''''Tagged
makeTag ''''SomeAwkUserType ''''Tagged

--  A sample DSum''s use case
toString :: DSum (Tagged SomeUserType1) Identity -> String
toString (TagFoo :=> Identity int) = show int
toString (TagBar :=> Identity str) = str

Esto termina generando instancias de etiqueta de data family para cada tipo. Hazme saber si tienes alguna pregunta.