在没有模板 Haskell 的情况下,如何为任何数据类型生成用于 DSum 的标记类型?

How can I produce a Tag type for any datatype for use with DSum, without Template Haskell?

背景

我想写一些库代码,它在内部使用 DSum 来操作用户的数据类型。 DSum 需要具有单个类型参数的 'tag' 类型。但是我希望我的代码只适用于任何旧的具体类型。所以,我只想获取用户类型并自动生成标签类型。我在这里 问了一个非常相似的问题,并得到了很好的答案。该答案依赖于 TH,主要是为了创建顶级声明。但是,我实际上并不关心顶级声明,如果可能的话,我宁愿避免使用 TH。

问题

[如何]使用一些通用编程技术编写数据类型

data Magic t a ...

其中给出了一些任意的总和类型,例如

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

Magic SomeUserType 等同于可以与 DSum 一起使用的 'tag' 类型?

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

我不确定您是否可以省去 TH,因为如评论中所述,您仍然需要在一天结束时打字。正如本杰明所说,您可能正在寻找 data family

你所谓的Magic,我就称之为Tagged

这是 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)

还有一个示例用例(一直到涉及 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

这最终会为每种类型生成 data family 个标记实例。如果您有任何问题,请告诉我。

不像这里的一些人声称的那样,定义这样一个类型是完全明智的(实际上非​​常简单,使用正确的库 - generics-sop)。这个库已经提供了基本上所有的机器:

{-# 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) }

类型GTag就是你所说的Magic。实际的 'magic' 发生在 Code 类型族中,它计算类型的通用表示,作为类型列表的列表。类型 NS (Tup2List i) xs 意味着对于 xs 中的一个,Tup2List i 成立 - 这只是一个参数列表与某个元组同构的证明。

你需要的类都可以导出:

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

您可以为对该类型有效的标签定义一些模式同义词:

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))))

和一个简单的测试:

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" ] 

由于这是用通用类型函数表示的,因此您可以在标记上编写通用操作。例如,对于任何 Generic texists x . (GTag t x, x) 同构于 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 

至于需要 Tup2List,需要它的原因很简单,因为您将两个参数 (Baz Bool String) 的构造函数表示为 (Bool, String) 元组上的标记在你的例子中。

您也可以将其实现为

type HList = NP I -- from generics-sop 

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

将参数表示为异构列表,或者更简单

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 ...

然而,元组表示确实有一个优点,即一元元组是 'projected' 到元组中的单个值(即,而不是 (x, ()))。如果您以明显的方式表示争论,fun0 等函数必须进行模式匹配才能检索存储在构造函数中的单个值。