我怎样才能编写这个GEq实例？

本文介绍了我怎样才能编写这个GEq实例？的处理方法，对大家解决问题具有一定的参考价值，需要的朋友们下面随着小编来一起学习吧！ 问题描述 29岁程序员，3月因学历无情被辞！ 我有数据类型 Tup2List 和 GTag （从 我想写一个 GEq 实例 GTag t ，我认为还需要 Tup2List 。我怎么能写这个实例？ 我为什么不工作的猜测是因为没有这样的事情作为部分 Refl - 你需要一次性为整个结构匹配编译器给你的Refl，而我试图只展开最外层的构造函数，然后递归。 这里是我的代码，其中未定义填写了我不知道如何编写的部分。 { - ＃LANGUAGE RankNTypes＃ - } 模块Foo其中 导入Data.GADT.Compare 导入Generics.SOP 导入合格的GHC.Generics as GHC data Tup2List :: * - > [*] - > *其中 Tup0 :: Tup2List（）'[] Tup1 :: Tup2List x'[x] TupS :: Tup2List r（x'：xs） - > Tup2List（a，r）（a'：x'：xs） 实例GEq（Tup2List t）其中 geq Tup0 Tup0 =只是Refl geq Tup1 Tup1 = Just Refl geq（TupS x）（TupS y）= case x`geq` y of Just Refl - > Just Refl Nothing - >没有 newtype GTag ti = GTag {unTag :: NS（Tup2List i）（Code t）} instance GEq（GTag t）其中 geq（GTag （GTag（Z_））（GTag（Z_））=没有 geq（GTag（Z_x））（GTag（Z_y））=未定义 - x`geq` y geq （GTag（S x））=未定义 - x`geq` y 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 whereimport Data.GADT.Compareimport Generics.SOPimport qualified GHC.Generics as GHCdata 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 -> Nothingnewtype 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` yEDIT: I've changed my datatypes around, but i'm still facing the same core problem. The current definitions aredata Quux i xs where Quux :: Quux (NP I xs) xsnewtype 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 tpattern P0 = GTag (Z Refl)pattern P1 :: () => (ys ~ (x0 ': '[t] ': xs)) => GTag_ ys tpattern P1 = GTag (S (Z Refl))pattern P2 :: () => (ys ~ (x0 ': x1 ': '[t] ': xs)) => GTag_ ys tpattern P2 = GTag (S (S (Z Refl)))pattern P3 :: () => (ys ~ (x0 ': x1 ': x2 ': '[t] ': xs)) => GTag_ ys tpattern P3 = GTag (S (S (S (Z Refl))))pattern P4 :: () => (ys ~ (x0 ': x1 ': x2 ': x3 ': '[t] ': xs)) => GTag_ ys tpattern 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 SomeUserTypeThe 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) Maybeex1 = P0 ==> 3ex2 = 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 _ _ = Nothinginstance 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 _ _ = \ _ _ -> FalseAnd some examples of their use:GHCi> (ex1, ex2, ex3)(P0 :=> Just 3,P1 :=> Just 'x',P2 :=> Just (True,"foo"))GHCi> ex1 == ex1TrueGHCi> ex1 == ex2False 这篇关于我怎样才能编写这个GEq实例？的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持！ 上岸，阿里云！