How can I produce a Tag type for any datatype for

问题:

background

I want to write some library code, which internally uses DSum to manipulate a user's datatype. DSum requires a 'tag' type that has a single type argument. However I want my code to work with just any old concrete type. So, I'd like to just take the user's type and automatically produce the tag type. I've asked a very similar question here How can I programatically produce this datatype from the other?, and gotten a great answer. That answer relies on TH, mainly so that it can create top-level declarations. However, I actually don't care about the top-level declaration, and I'd prefer to avoid the TH if possible.

question

[How] can I write, with some generic programming technique, a datatype

data Magic t a ...

where given some arbitrary sum type, e.g.

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

Magic SomeUserType is equivalent to this 'tag' type that can be used with DSum?

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

回答1:

Unlike some here have claimed, it is perfectly sensible (and in fact quite straightforward, with the correct library - generics-sop) to define such a type. Essentially all the machinery is provided by this library already:

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

The type GTag is what you call Magic. The actual 'magic' happens in the Code type family, which compute the generic representation of a type, as a list of lists of types. The type NS (Tup2List i) xs means that for precisely one of xs, Tup2List i holds - this is simply a proof that a list of arguments is isomorphic to some tuple.

All the classes you need can be derived:

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

You can define some pattern synonyms for the tags valid for this type:

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

and a simple test:

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" ] 

Since this is expressed in terms of a generic type function, you can write generic operations over tags. For example, exists x . (GTag t x, x) is isomorphic to t for any Generic 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 

---

As for the need for Tup2List, it is needed for the simply reason that you represent a constructor of two arguments (Baz Bool String) as a tag over a tuple of (Bool, String) in your example.

You could also implement it as

type HList = NP I -- from generics-sop 

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

which represents the arguments as a heterogeneous list, or even more simply

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

However, the tuple representation does have the advantage that unary tuples are 'projected' to the single value which is in the tuple (i.e., instead of (x, ())). If you represent arguements in the obvious way, functions such as fun0 must pattern match to retrieve the single value stored in a constructor.

回答2:

I'm not sure you can dispense with the TH since, as noted in the comments, you still need to make a type at the end of the day. As Benjamin notes, you are probably looking for a data family.

What you call Magic, I will refer to as Tagged.

Here is the adjusted code you will need for 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)

And, a sample use case (all the way through to something involving DSum):

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

This ends up generating data family tag instances for each type. Let me know if you have any questions.