Below you'll find my encoding of GHC.Generics with DataKinds. The most important part, for this discussion, is the treatment of meta-information. I don't think we need |sameDatatype|, in particular; why not just use |sameSymbol|?
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE OverlappingInstances #-}
module Test where
import GHC.TypeLits
import Data.Proxy ( Proxy(..) )
--------------------------------------------------------------------------------
-- Universe encoding
--------------------------------------------------------------------------------
data Un s = -- s is to always be set to *
-- Void (used for datatypes without constructors)
VV
-- Unit
| UU
-- Meta-data
| MD MetaData (Un s)
| MC MetaCons (Un s)
| MS MetaSel (Un s)
-- A parameter
| PAR
-- Constants (either other parameters or recursion into types of kind *)
| KK PRU s
-- Recursion into types of kind (* -> *)
| REC SO (s -> s)
-- Sum, product
| Un s :+: Un s
| Un s :**: Un s
-- Composition
| (s -> s) :.: Un s
--------------------------------------------------------------------------------
-- Meta-data
--------------------------------------------------------------------------------
-- Parameter, Recursive occurrence, or Unknown/other
data PRU = P | R SO | U
-- Self or Other
data SO = S | O
data MetaData = MetaData { dataName :: Symbol, dataModule :: Symbol }
data MetaCons = MetaCons { conName :: Symbol
, conFixity :: Fixity
, conIsRecord :: Bool }
data Fixity = Prefix | Infix Associativity Nat
data Associativity = LeftAssociative
| RightAssociative
| NotAssociative
deriving (Eq, Show, Ord, Read)
data MetaSel = MetaSel { selName :: Maybe Symbol }
--------------------------------------------------------------------------------
-- Interpretation (as a GADT)
--------------------------------------------------------------------------------
data In (u :: Un *) (p :: *) :: * where
-- No interpretation for VV, as it shouldn't map to any value
-- Unit
U1 :: In UU p
-- Datatype meta-data
D1 :: { unD1 :: In a p } -> In (MD md a) p
-- Constructor meta-data
C1 :: { unC1 :: In a p } -> In (MC mc a) p
-- Selector meta-data
S1 :: { unS1 :: In a p } -> In (MS ms a) p
-- The parameter
Par1 :: { unPar1 :: p } -> In PAR p
-- Constants
K1 :: { unK1 :: x} -> In (KK pru x) p
-- Recursion
Rec1 :: { unRec1 :: f p } -> In (REC i f) p
-- Sum
L1 :: In f p -> In (f :+: g) p
R1 :: In g p -> In (f :+: g) p
-- Product
(:*:) :: In f p -> In g p -> In (f :**: g) p
-- Composition
Comp1 :: { unComp1 :: f (In g p) } -> In (f :.: g) p
--------------------------------------------------------------------------------
-- Conversions to/from user datatypes
--------------------------------------------------------------------------------
class Generic (a :: *) where
type Rep a :: Un *
from :: a -> In (Rep a) p
to :: In (Rep a) p -> a
class Generic1 (f :: * -> *) where
type Rep1 f :: Un *
from1 :: f p -> In (Rep1 f) p
to1 :: In (Rep1 f) p -> f p
--------------------------------------------------------------------------------
-- Example encoding: lists (with some twisted meta-data for example purposes)
--------------------------------------------------------------------------------
instance Generic [a] where
type Rep [a] = MD ('MetaData "[]" "Prelude")
(MC ('MetaCons "[]" Prefix False) UU
:+: MC ('MetaCons ":" (Infix RightAssociative 5) False)
( MS ('MetaSel (Just "el")) (KK P a)
:**: MS ('MetaSel Nothing) (KK (R S) [a])))
from [] = D1 (L1 (C1 U1))
from (h:t) = D1 (R1 (C1 (S1 (K1 h) :*: S1 (K1 t))))
to (D1 (L1 (C1 U1))) = []
to (D1 (R1 (C1 (S1 (K1 h) :*: S1 (K1 t))))) = h:t
-- Should have meta-information as well, but the one above is enough for now
instance Generic1 [] where
type Rep1 [] = UU :+: (PAR :**: REC S [])
from1 [] = L1 U1
from1 (h:t) = R1 (Par1 h :*: Rec1 t)
to1 (L1 U1) = []
to1 (R1 (Par1 h :*: Rec1 t)) = h:t
--------------------------------------------------------------------------------
-- Show
--------------------------------------------------------------------------------
class GShow (r :: Un *) where
gshow :: In r p -> String
instance (Show' a) => GShow (KK pru a) where
gshow (K1 a) = show' a
instance GShow UU where
gshow U1 = ""
instance (GShow r) => GShow (MD md r) where
gshow (D1 x) = gshow x
-- We can now match meta-data properties at the type level
instance (KnownSymbol name) => GShow (MC ('MetaCons name Prefix isRec) UU) where
gshow (C1 x) = symbolVal (Proxy :: Proxy name)
instance (KnownSymbol name, GShow r)
=> GShow (MC ('MetaCons name Prefix isRec) r) where
gshow (C1 x) = "(" ++ symbolVal (Proxy :: Proxy name) ++ " " ++ gshow x ++ ")"
-- Note how we assume that the structure under an Infix MC must be a product.
-- This is not encoded in the universe, regrettably, and might lead to "missing
-- instance" errors if we're not careful.
instance (KnownSymbol name, GShow a, GShow b)
=> GShow (MC ('MetaCons name (Infix assoc fix) isRec) (a :**: b)) where
gshow (C1 (a :*: b)) = "(" ++ gshow a ++ " "
++ symbolVal (Proxy :: Proxy name) ++ " "
++ gshow b ++ ")"
instance (GShow r) => GShow (MS ('MetaSel Nothing) r) where
gshow (S1 x) = gshow x
instance (KnownSymbol name, GShow r)
=> GShow (MS ('MetaSel (Just name)) r) where
gshow (S1 x) = "{ " ++ symbolVal (Proxy :: Proxy name) ++ " = "
++ gshow x ++ " }"
instance (GShow a, GShow b) => GShow (a :+: b) where
gshow (L1 a) = gshow a
gshow (R1 b) = gshow b
instance (GShow a, GShow b) => GShow (a :**: b) where
gshow (a :*: b) = gshow a ++ " " ++ gshow b
-- User-facing class
class Show' (a :: *) where
show' :: a -> String
default show' :: (Generic a, GShow (Rep a)) => a -> String
show' = gshow . from
--------------------------------------------------------------------------------
-- Test
--------------------------------------------------------------------------------
instance Show' Int where show' = show
instance (Show' a) => Show' [a]
test1, test2 :: String
test1 = show' ([] :: [Int]) -- "[]"
test2 = show' [1,2::Int] -- "({ el = 1 } : ({ el = 2 } : []))"