我怎样才能生成任何数据类型的标签类型与DSum一起使用，没有模板Haskell？ [英] How can I produce a Tag type for any datatype for use with DSum, without Template Haskell?
问题描述
问题
我可以用一些泛型编程技术写出一个数据类型
$ 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）
与此处声称的不同，它非常明智（实际上非常简单，正确的库< - c $ c> 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）同构于tp>
类型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 之类的函数必须进行模式匹配以检索存储在构造函数中的单个值。
background
I 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 datatype
data Magic t a ...
where given some arbitrary sum type, e.g.
data SomeUserType = Foo Int | Bar Char | Baz Bool String
Magic 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.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) }
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 SomeUserType
You 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 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
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) xs
which represents the arguments as a heterogeneous list, or even more simply
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 ...
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？的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！
