이 GEq 인스턴스를 작성하려면 어떻게해야합니까?

Question

나는 나는 또한 Tup2List 하나를 가지고 필요 생각 나는 GTag t에 대한 GEq 인스턴스를 작성하려는 Tup2List 및 GTag

(How can I produce a Tag type for any datatype for use with DSum, without Template Haskell?에 대한 대답에서) 데이터 유형을 가지고있다. 이 인스턴스를 작성하려면 어떻게해야합니까?

왜 부분적으로 그런 것이 없기 때문에 내 생각 엔 맞습니다. 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))))) 

가장 큰 차이점은 Code의 발생없이 GTag_을 정의하는 것입니다. 재귀 케이스는 다시 Code의 응용 프로그램으로 표현할 수 있어야한다는 요구 사항을 얻지 못하기 때문에 재귀를 쉽게 만듭니다.

앞서 언급했듯이 두 번째 차이점은 더 복잡한 Tup2List보다는 단일 인수 생성자를 강요하기 위해 (:~:) '[a]을 사용하는 것입니다. Baz의 인수는 이제 "하나의 인자"의 요구 사항을 준수하기 위해 명시 적으로 쌍을 작성

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

instance Generic SomeUserType 

:

여기에 원래의 예의 변형입니다.

예 의존 합계 :

이제

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