我該如何編寫這個GEq實例？

Question

我有數據類型Tup2List和GTag（從答案How can I produce a Tag type for any datatype for use with DSum, without Template Haskell?）

我想寫一個GEq實例GTag t，我認爲還需要有一個爲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個或多個字段的總和類型導出標籤類型的很多要點，所以我將簡化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