我怎样才能生成任何数据类型的标签类型与DSum一起使用，没有模板Haskell？

本文介绍了我怎样才能生成任何数据类型的标签类型与DSum一起使用，没有模板Haskell？的处理方法，对大家解决问题具有一定的参考价值，需要的朋友们下面随着小编来一起学习吧！ 问题描述 我想写一些库代码，它在内部使用DSum来操作用户的数据类型。 DSum需要一个具有单一类型参数的标签类型。不过，我希望我的代码只使用任何旧的具体类型。所以，我想只取用户的类型并自动生成标签类型。我在这里问了一个非常类似的问题我怎样才能以编程方式从另一个产生这种数据类型？，并得到了一个很好的答案。该答案依赖于TH，主要是为了能够创建顶级声明。然而，我其实并不关心顶层声明，如果可能，我宁愿避免使用TH。 问题 我可以用一些泛型编程技术写出一个数据类型 $ b pre $ data magic ta ... 其中给出了一些任意的和类型，例如 data SomeUserType = Foo Int |酒吧Char | Baz Bool字符串 Magic SomeUserType 相当于这个'tag'类型可以与DSum一起使用吗？ data TagSomeUserType a其中 TagFoo :: TagSomeUserType Int TagBar :: TagSomeUserType Char TagBaz :: TagSomeUserType（Bool，String） 解决方案与此处声称的不同，它非常明智（实际上非​​常简单，正确的库 generics-sop ）定义这种类型。基本上所有的机器都是由这个库提供的： { - ＃LANGUAGE PatternSynonyms，PolyKinds，DeriveGeneric＃ - } 导入Generics.SOP 导入合格的GHC.Generics作为GHC 导入Data.Dependent.Sum data Tup2List :: * - > [*] - > *其中 Tup0 :: Tup2List（）'[] Tup1 :: Tup2List x'[x] TupS :: Tup2List r（x'：xs） - > Tup2List（a，r）（a'：x'：xs） newtype GTag ti = GTag {unTag :: NS（Tup2List i）（Code t）} $ b 类型 GTag 就是你所说的 Magic code>。实际的'魔术'发生在 Code 类型族中，它将类型的通用表示形式列为类型列表。类型 NS（Tup2List i）xs 表示对于 xs ， Tup2List i 成立 - 这只是一个证明，表明参数列表同构于某个元组。 您需要的所有类都可以派生出来： data SomeUserType = Foo Int |酒吧Char | Baz Bool String （GHC.Generic，Show）实例Generic SomeUserType 您可以为有效的标签定义一些模式同义词： pattern TagFoo ::（）=> （x〜Int）=> GTag SomeUserType x 模式TagFoo = GTag（Z Tup1） 模式TagBar ::（）=> （x〜Char）=> GTag SomeUserType x 模式TagBar = GTag（S（Z Tup1）） 模式TagBaz ::（）=> （x〜（Bool，String））=> GTag SomeUserType x pattern TagBaz = GTag（S（S（Z（TupS Tup1）））） 和一个简单的测试： fun0 :: GTag SomeUserType i - >我 - >字符串 fun0 TagFoo i =复制我'a' fun0 TagBar c = c：[] fun0 TagBaz（b，s）=（如果b然后显示其他id）s fun0'= \（t：& v） - > fun0 tv main = mapM_（putStrLn。fun0'.toTagVal） [Foo 10，Bar'q'，Baz Truehello，Baz Falseworld] 由于这是用通用类型函数表示的，因此您可以在标签上编写通用操作。例如，存在x。 （GTag tx，x）同构于 t p> 类型GTagVal t = DSum（GTag t）I 模式（：&）:: forall t :: * - > *）。 （）=>全部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，v1）） toTagValG :: NS（NP I）xss - > （全部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 = {（） - > 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 - 来自泛型-sop data Tup2List i xs其中Tup2List :: Tup2List（HList xs）xs 它将参数表示为异构列表，或者甚至更简单 pre $ newtype GTag ti = 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）=复制我'a' fun0 ... 但是，元组表示确实具有一元元组被投影到元组中的单个值的优点（即，代替（x，（）））。如果以显而易见的方式表示参数，则诸如 fun0 之类的函数必须进行模式匹配以检索存储在构造函数中的单个值。 backgroundI want to write some library code, which internally uses DSum to manipulate a user's datatype. DSum requires a 'tag' type that has a single type argument. However I want my code to work with just any old concrete type. So, I'd like to just take the user's type and automatically produce the tag type. I've asked a very similar question here How can I programatically produce this datatype from the other?, and gotten a great answer. That answer relies on TH, mainly so that it can create top-level declarations. However, I actually don't care about the top-level declaration, and I'd prefer to avoid the TH if possible.question[How] can I write, with some generic programming technique, a datatypedata Magic t a ...where given some arbitrary sum type, e.g.data SomeUserType = Foo Int | Bar Char | Baz Bool StringMagic SomeUserType is equivalent to this 'tag' type that can be used with DSum?data TagSomeUserType a where TagFoo :: TagSomeUserType Int TagBar :: TagSomeUserType Char TagBaz :: TagSomeUserType (Bool, String) 解决方案 Unlike some here have claimed, it is perfectly sensible (and in fact quite straightforward, with the correct library - generics-sop) to define such a type. Essentially all the machinery is provided by this library already: {-# LANGUAGE PatternSynonyms, PolyKinds, DeriveGeneric #-} import Generics.SOP import qualified GHC.Generics as GHC import Data.Dependent.Sumdata 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) }The type GTag is what you call Magic. The actual 'magic' happens in the Code type family, which compute the generic representation of a type, as a list of lists of types. The type NS (Tup2List i) xs means that for precisely one of xs, Tup2List i holds - this is simply a proof that a list of arguments is isomorphic to some tuple. All the classes you need can be derived: data SomeUserType = Foo Int | Bar Char | Baz Bool String deriving (GHC.Generic, Show) instance Generic SomeUserTypeYou can define some pattern synonyms for the tags valid for this type: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))))and a simple test: 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" ] Since this is expressed in terms of a generic type function, you can write generic operations over tags. For example, exists x . (GTag t x, x) is isomorphic to t for any Generic t: type GTagVal t = DSum (GTag t) I pattern (:&) :: forall (t :: * -> *). () => forall a. t a -> a -> DSum t Ipattern 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 xtoTagValG_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 As for the need for Tup2List, it is needed for the simply reason that you represent a constructor of two arguments (Baz Bool String) as a tag over a tuple of (Bool, String) in your example. You could also implement it as type HList = NP I -- from generics-sop data Tup2List i xs where Tup2List :: Tup2List (HList xs) xswhich represents the arguments as a heterogeneous list, or even more simplynewtype 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 ...However, the tuple representation does have the advantage that unary tuples are 'projected' to the single value which is in the tuple (i.e., instead of (x, ())). If you represent arguements in the obvious way, functions such as fun0 must pattern match to retrieve the single value stored in a constructor. 这篇关于我怎样才能生成任何数据类型的标签类型与DSum一起使用，没有模板Haskell？的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持！