我该如何编写这个 GEq 实例？

Question

我有数据类型Tup2List 和GTag（来自How can I produce a Tag type for any datatype for use with DSum, without Template Haskell? 的答案）

我想为GTag t 编写一个GEq 实例，我认为这也需要为Tup2List 编写一个实例。这个实例怎么写？

我对它为什么不起作用的猜测是因为没有部分 Refl 这样的东西 - 你需要一次匹配整个结构以便编译器给你 Refl，而我正在尝试只需解开最外层的构造函数，然后递归。

这是我的代码，undefined 填写了我不知道如何编写的部分。

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

编辑：我已经改变了我的数据类型，但我仍然面临同样的核心问题。当前的定义是

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

Answer 1

这是我对此的看法。就个人而言，我认为允许为具有 0 个或多个字段的 sum 类型派生标签类型没有多大意义，因此我将简化 Tup2List 。它的存在与手头的问题是正交的。

所以我要定义GTag如下：

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

主要区别在于定义GTag_ 时不出现Code。这将使递归更容易，因为您没有要求递归案例必须再次表达为Code 的应用程序。

第二个区别，如前所述，是使用(:~:) '[a] 来强制单参数构造函数，而不是更复杂的Tup2List。

这是原始示例的变体：

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

instance Generic SomeUserType

Baz 的参数现在明确写成一对，以遵守“单一参数”的要求。

依赖总和示例：

ex1, ex2, ex3 :: DSum (GTag SomeUserType) Maybe
ex1 = P0 ==> 3
ex2 = P1 ==> 'x'
ex3 = P2 ==> (True, "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)

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

以及它们的一些使用示例：

GHCi> (ex1, ex2, ex3)
(P0 :=> Just 3,P1 :=> Just 'x',P2 :=> Just (True,"foo"))
GHCi> ex1 == ex1
True
GHCi> ex1 == ex2
False