我怎样才能编写这个GEq实例? [英] How can I write this GEq instance?
问题描述
data Quux i xs其中Quux :: Quux(NP I xs)xs
newtype GTag ti = GTag {unTag :: NS(Quux i)(Code t)}
instance GEq(GTag t)where
- 我不知道该怎么做
geq(GTag(S x))(GTag(S y))=未定义
这是我对此的看法。就个人而言,我没有看到允许为具有0个或多个字段的总和类型派生标记类型,因此我将简化 Tup2List
。它的存在与正在处理的问题是正交的。
因此,我将按如下方式定义 GTag
:
type GTag t = GTag_(Code t)
newtype GTag_ ta = GTag {unGTag :: NS((:〜 :)'[a])t}
pattern P0 ::()=> (ys〜('[t]':xs))=> GTag_ys t
模式P0 = GTag(Z Refl)
模式P1 ::()=> (ys〜(x0':'[t]':xs))=> GTag_ys t
模式P1 = GTag(S(Z Refl))
模式P2 ::()=> (ys〜(x0':x1':'[t]':xs))=> GTag_ys t
pattern P2 = GTag(S(S(Z Refl)))
pattern P3 ::()=> (ys〜(x0':x1':x2':'[t]':xs))=> GTag_ys t
模式P3 = GTag(S(S(S(Z Refl))))
模式P4 ::()=> (ys〜(x0':x1':x2':x3':'[t]':xs))=> GTag_ys t
模式P4 = GTag(S(S(S(S(Z Refl)))))
主要区别在于定义 GTag _
而不会出现代码
。这将使递归更容易,因为您没有得到递归案例必须作为 Code
的应用程序来表达的要求。
如前所述,次要区别是使用(:〜:)'[a]
强制使用单参数构造函数,而不是更复杂 Tup2List
。
以下是原始示例的变体:
data SomeUserType = Foo Int |酒吧Char | Baz(Bool,String)
派生(GHC.Generic)
实例通用SomeUserType
Baz
的参数现在被明确地写成一对,以遵守单参数要求。
$ p
$ b $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $> $ ex $,ex2,ex3 :: DSum(GTag SomeUserType)也许
ex1 = P0 ==> 3
ex2 = P1 ==> 'x'
ex3 = P2 ==> (真,foo)
现在这些实例:
instance GShow(GTag_ t)where
gshowsPrec _n = go 0
where
go :: Int - > GTag_ t a - > ShowS
go k(GTag(Z Refl))= showString(P++ show k)
go k(GTag(S i))= go(k + 1)(GTag i)
实例All2(Compose Show f)t => ShowTag(GTag_t)f其中
showTaggedPrec(GTag(Z Refl))= showsPrec
showTaggedPrec(GTag(S i))= showTaggedPrec(GTag i)
instance GEq (GTag(S i))=(GTag(S j))= geq(GTag(t))其中
geq(GTag(Z Refl))(GTag(Z Refl))= Just Refl
geq )(GTag j)
geq _ _ = Nothing
instance All2(Compose Eq f)t => EqTag(GTag_t)f其中
eqTagged(GTag(Z Refl))(GTag(Z Refl))=(==)
eqTagged(GTag(S i))(GTag(S j)) = eqTagged(GTag i)(GTag j)
eqTagged _ _ = \ _ _ - >假
以及它们使用的一些示例:
GHCI> (ex1,ex2,ex3)
(P0:=> Just 3,P1:=> Just'x',P2:=> Just(True,foo))
GHCi> ex1 == ex1
True
GHCi> ex1 == ex2
False
I have datatypes Tup2List
and GTag
(from the answer to How can I produce a Tag type for any datatype for use with DSum, without Template Haskell?)
I want to write a GEq
instance for GTag t
, which I think requires also having one for Tup2List
. How can I write this instance?
My guess at why it doesn't work is because there's no such thing as a partial Refl
- you need to match the whole structure all at once for the compiler to give you the Refl, whereas I'm trying to just unwrap the outermost constructor and then recurse.
Here's my code, with undefined
filling in for the parts I don't know how to write.
{-# LANGUAGE GADTs #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE RankNTypes #-}
module Foo where
import Data.GADT.Compare
import Generics.SOP
import qualified GHC.Generics as GHC
data Tup2List :: * -> [*] -> * where
Tup0 :: Tup2List () '[]
Tup1 :: Tup2List x '[ x ]
TupS :: Tup2List r (x ': xs) -> Tup2List (a, r) (a ': x ': xs)
instance GEq (Tup2List t) where
geq Tup0 Tup0 = Just Refl
geq Tup1 Tup1 = Just Refl
geq (TupS x) (TupS y) =
case x `geq` y of
Just Refl -> Just Refl
Nothing -> Nothing
newtype GTag t i = GTag { unTag :: NS (Tup2List i) (Code t) }
instance GEq (GTag t) where
geq (GTag (Z x)) (GTag (Z y)) = undefined -- x `geq` y
geq (GTag (S _)) (GTag (Z _)) = Nothing
geq (GTag (Z _)) (GTag (S _)) = Nothing
geq (GTag (S x)) (GTag (S y)) = undefined -- x `geq` y
EDIT: I've changed my datatypes around, but i'm still facing the same core problem. The current definitions are
data Quux i xs where Quux :: Quux (NP I xs) xs
newtype GTag t i = GTag { unTag :: NS (Quux i) (Code t) }
instance GEq (GTag t) where
-- I don't know how to do this
geq (GTag (S x)) (GTag (S y)) = undefined
Here's my take on this. Personally, I don't see much point in allowing to derive a tag type for sum types which have 0 or more than one field, so I'm going to simplify Tup2List
away. Its presence is orthogonal to the question at hand.
So I'm going to define GTag
as follows:
type GTag t = GTag_ (Code t)
newtype GTag_ t a = GTag { unGTag :: NS ((:~:) '[a]) t }
pattern P0 :: () => (ys ~ ('[t] ': xs)) => GTag_ ys t
pattern P0 = GTag (Z Refl)
pattern P1 :: () => (ys ~ (x0 ': '[t] ': xs)) => GTag_ ys t
pattern P1 = GTag (S (Z Refl))
pattern P2 :: () => (ys ~ (x0 ': x1 ': '[t] ': xs)) => GTag_ ys t
pattern P2 = GTag (S (S (Z Refl)))
pattern P3 :: () => (ys ~ (x0 ': x1 ': x2 ': '[t] ': xs)) => GTag_ ys t
pattern P3 = GTag (S (S (S (Z Refl))))
pattern P4 :: () => (ys ~ (x0 ': x1 ': x2 ': x3 ': '[t] ': xs)) => GTag_ ys t
pattern P4 = GTag (S (S (S (S (Z Refl)))))
The main difference is to define GTag_
without an occurrence of Code
. This will make recursion easier, because you don't get a requirement that the recursive case has to be expressible as an application of Code
again.
The secondary difference, as mentioned before, is the use of (:~:) '[a]
to force single-argument constructors rather than the more complicated Tup2List
.
Here's a variant of your original example:
data SomeUserType = Foo Int | Bar Char | Baz (Bool, String)
deriving (GHC.Generic)
instance Generic SomeUserType
The argument of Baz
is now written a a pair explicitly, to adhere to the "single argument" requirement.
Example dependent sums:
ex1, ex2, ex3 :: DSum (GTag SomeUserType) Maybe
ex1 = P0 ==> 3
ex2 = P1 ==> 'x'
ex3 = P2 ==> (True, "foo")
Now the instances:
instance GShow (GTag_ t) where
gshowsPrec _n = go 0
where
go :: Int -> GTag_ t a -> ShowS
go k (GTag (Z Refl)) = showString ("P" ++ show k)
go k (GTag (S i)) = go (k + 1) (GTag i)
instance All2 (Compose Show f) t => ShowTag (GTag_ t) f where
showTaggedPrec (GTag (Z Refl)) = showsPrec
showTaggedPrec (GTag (S i)) = showTaggedPrec (GTag i)
instance GEq (GTag_ t) where
geq (GTag (Z Refl)) (GTag (Z Refl)) = Just Refl
geq (GTag (S i)) (GTag (S j)) = geq (GTag i) (GTag j)
geq _ _ = Nothing
instance All2 (Compose Eq f) t => EqTag (GTag_ t) f where
eqTagged (GTag (Z Refl)) (GTag (Z Refl)) = (==)
eqTagged (GTag (S i)) (GTag (S j)) = eqTagged (GTag i) (GTag j)
eqTagged _ _ = \ _ _ -> False
And some examples of their use:
GHCi> (ex1, ex2, ex3)
(P0 :=> Just 3,P1 :=> Just 'x',P2 :=> Just (True,"foo"))
GHCi> ex1 == ex1
True
GHCi> ex1 == ex2
False
这篇关于我怎样才能编写这个GEq实例?的文章就介绍到这了,希望我们推荐的答案对大家有所帮助,也希望大家多多支持IT屋!