Template Haskell없이 DSum과 함께 사용할 데이터 유형에 대한 태그 유형을 어떻게 만들 수 있습니까?

Question

내가 내부적으로 사용자의 데이터 유형을 조작 할 수 DSUM을 사용하는 일부 라이브러리 코드를 작성하려는

배경. DSum에는 단일 유형 인수가있는 '태그'유형이 필요합니다. 그러나 필자는 코드가 오래된 구형으로 작업하기를 원합니다. 그래서, 나는 사용자의 타입을 취하고 태그 타입을 자동으로 생성하려고합니다. 나는 여기에 매우 비슷한 질문을했습니다. How can I programatically produce this datatype from the other?, 좋은 대답을 얻었습니다. 그 대답은 주로 TH에 의존하여 최상위 수준의 선언을 만들 수 있습니다. 그러나 실제로는 최상위 선언에 대해서는 신경 쓰지 않으며 가능한 경우 TH를 피하기를 원합니다.

질문

[방법] 나는 몇 가지 일반적인 프로그래밍 기술, 어떤 임의의 합계 유형을 주어진 데이터 형식

data Magic t a ... 

, 예를 들어, 함께 쓸 수 있습니다

data SomeUserType = Foo Int | Bar Char | Baz Bool String 

Magic SomeUserType은 DSum과 함께 사용할 수있는 '태그'유형과 동일합니까? 내가 코멘트에서 언급 한대로, 이후 TH 생략 할 수 있습니다 모르겠어요

data TagSomeUserType a where 
    TagFoo :: TagSomeUserType Int 
    TagBar :: TagSomeUserType Char 
    TagBaz :: TagSomeUserType (Bool, String) 

Answer 1

여기에 언급 된 것과 달리, 이러한 유형을 정의하는 것은 완벽하게 의미가 있습니다 (실제로는 올바른 라이브러리 - generics-sop).

{-# LANGUAGE PatternSynonyms, PolyKinds, DeriveGeneriC#-} 

import Generics.SOP 
import qualified GHC.Generics as GHC 
import Data.Dependent.Sum 

data Tup2List :: * -> [*] -> * where 
    Tup0 :: Tup2List() '[] 
    Tup1 :: Tup2List x '[ x ] 
    TupS :: Tup2List r (x ': xs) -> Tup2List (a, r) (a ': x ': xs) 

newtype GTag t i = GTag { unTag :: NS (Tup2List i) (Code t) } 

유형 GTag 당신이 Magic을 부르는 : 기본적으로 모든 기계는 이미이 라이브러리에 의해 제공됩니다. 실제 '마법'은 유형 목록의 목록으로 유형의 제네릭 표현을 계산하는 Code 유형 모음에서 발생합니다. 유형 NS (Tup2List i) xs은 정확히 xs 중 하나 인 Tup2List i을 보유한다는 것을 의미합니다. 이는 인수 목록이 일부 튜플과 동형임을 증명하는 것입니다.당신이 필요로하는

모든 클래스를 유도 할 수있다 :

pattern TagFoo ::() => (x ~ Int) => GTag SomeUserType x 
pattern TagFoo = GTag (Z Tup1) 

pattern TagBar ::() => (x ~ Char) => GTag SomeUserType x 
pattern TagBar = GTag (S (Z Tup1)) 

pattern TagBaz ::() => (x ~ (Bool, String)) => GTag SomeUserType x 
pattern TagBaz = GTag (S (S (Z (TupS Tup1)))) 

및 간단한 테스트 :

fun0 :: GTag SomeUserType i -> i -> String 
fun0 TagFoo i = replicate i 'a' 
fun0 TagBar c = c : [] 
fun0 TagBaz (b,s) = (if b then show else id) s 

fun0' = \(t :& v) -> fun0 t v 

main = mapM_ (putStrLn . fun0' . toTagVal) 
      [ Foo 10, Bar 'q', Baz True "hello", Baz False "world" ] 

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

당신은이 유형에 대한 유효한 태그에 대한 몇 가지 패턴 동의어를 정의 할 수 있습니다

제네릭 형식 함수로 표현되므로 t보다 일반적인 연산을 작성할 수 있습니다 ags. 예를 들어, exists x . (GTag t x, x)는 Generic t에 대한 t에 동형 :

type GTagVal t = DSum (GTag t) I 

pattern (:&) :: forall (t :: * -> *).() => forall a. t a -> a -> DSum t I 
pattern t :& a = t :=> I a  

toTagValG_Con :: NP I xs -> (forall i . Tup2List i xs -> i -> r) -> r 
toTagValG_Con Nil k = k Tup0() 
toTagValG_Con (I x :* Nil) k = k Tup1 x 
toTagValG_Con (I x :* y :* ys) k = toTagValG_Con (y :* ys) (\tp vl -> k (TupS tp) (x, vl)) 

toTagValG :: NS (NP I) xss -> (forall i . NS (Tup2List i) xss -> i -> r) -> r 
toTagValG (Z x) k = toTagValG_Con x (k . Z) 
toTagValG (S q) k = toTagValG q (k . S) 

fromTagValG_Con :: i -> Tup2List i xs -> NP I xs 
fromTagValG_Con i Tup0 = case i of {() -> Nil } 
fromTagValG_Con x Tup1 = I x :* Nil 
fromTagValG_Con xs (TupS tg) = I (fst xs) :* fromTagValG_Con (snd xs) tg 

toTagVal :: Generic a => a -> GTagVal a 
toTagVal a = toTagValG (unSOP $ from a) ((:&) . GTag) 

fromTagVal :: Generic a => GTagVal a -> a 
fromTagVal (GTag tg :& vl) = to $ SOP $ hmap (fromTagValG_Con vl) tg 

필요 Tup2List을 위해, 그것은 당신이 태그로 두 개의 인수 ( Baz Bool String)의 생성자를 나타내는 단순히 이유로 필요에 관해서는

---

귀하의 예에서는 튜플이 (Bool, String) 이상입니다.

또한 이기종 목록으로 인수를 나타내거나 더 간단하게

newtype GTag t i = GTag { unTag :: NS ((:~:) i) (Code t) } 
type GTagVal t = DSum (GTag t) HList 

fun0 :: GTag SomeUserType i -> HList i -> String 
fun0 TagFoo (I i :* Nil) = replicate i 'a' 
fun0 ... 

그러나, 튜플 표현이 단항 튜플는 장점을 가지고

type HList = NP I -- from generics-sop 

data Tup2List i xs where Tup2List :: Tup2List (HList xs) xs 

로 구현할 수 튜플에있는 단일 값 (예 : (x,()) 대신)에 '투영'됩니다. 명백한 방법으로 arguements를 표현하면 fun0과 같은 함수는 생성자에 저장된 단일 값을 검색하기 위해 패턴 일치가 필요합니다.

Answer 2

, 당신은 여전히 ​​하루의 끝에 유형을 확인해야합니다. 벤자민 (Benjamin)이 말한 것처럼, 아마도 data family을 찾고있을 것입니다.

당신이 Magic이라고 부르는 경우, 나는 Tagged이라고 부를 것입니다.

{-# LANGUAGE TemplateHaskell, GADTs, TypeFamilies #-} 
module Test where 

import Data.Dependent.Sum 
import Data.Functor.Identity 
import Tag 

-- Some data types 
data SomeUserType1 = Foo Int | Bar String 
data SomeUserType2 = Fooo Int | Baar Char | Baaz Bool String 
data SomeAwkUserType = Foooo Int 

-- Data family for all Tagged things 
data family Tagged t a 

-- Generated data family instances 
makeTag ''SomeUserType1 ''Tagged 
makeTag ''SomeUserType2 ''Tagged 
makeTag ''SomeAwkUserType ''Tagged 

-- A sample DSum's use case 
toString :: DSum (Tagged SomeUserType1) Identity -> String 
toString (TagFoo :=> Identity int) = show int 
toString (TagBar :=> Identity str) = str 

이를 : 여기에

은 ( DSum을 포함하는 무언가에 모든 방법을 통해) tag.hs

{-# LANGUAGE TemplateHaskell #-} 

module Tag where 

import Language.Haskell.TH 

makeTag :: Name -> Name -> DecsQ 
makeTag name tag = do 
    -- Reify the data declaration to get the constructors. 
    -- Note we are forcing there to be no type variables... 
    (TyConI (DataD _ _ [] _ cons _)) <- reify name 

    pure [ DataInstD [] tag [(ConT name), (VarT (mkName "a"))] Nothing (tagCon <$> cons) [] ] 
    where 
    -- Given a constructor, construct the corresponding constructor for 
    -- Tag GADT 
    tagCon :: Con -> Con 
    tagCon (NormalC conName args) = 
    let tys = fmap snd args 
     tagType = foldl AppT (TupleT (length tys)) tys 
    in GadtC [mkName ("Tag" ++ nameBase conName)] [] 
      (AppT (AppT (ConT tag) (ConT name)) tagType) 

그리고, 샘플 사용 사례에 필요한 조정 된 코드 각 유형에 대해 data family 태그 인스턴스를 생성합니다. 궁금한 점이 있으면 알려주세요.