Gabor and all, 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|? Cheers, Pedro {-# 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 } : []))" On Wed, Jul 2, 2014 at 1:42 PM, Gabor Greif wrote:

[added Pedro and Richard to "to:"]

On 6/30/14, Simon Peyton Jones wrote:

...

| Yes I have a branch, and it works! A bunch of things is still missing | (notably record selectors), but I have a proof-of-concept with a gdiff | library hooked up to GHC.Generics, and by appealing to type-level | reasoning I can obtain a difference tree from True to False (which | looks good) by using the reflection (i.e. class Generic) only, no need | for TH or hand-coding. Comparing bigger trees (and then 'patch'ing | them) appears to be SMOP from here.

Do you have a wiki page explaining what "it" is (the thing that works).

Here is a wiki page

https://ghc.haskell.org/trac/ghc/wiki/GenericsPropositionalEquality

you all are invited to make suggestions, ask questions and generally beautify.

...

| instance Datatype (Dat "MyModule" "Foo") ... | | I get an 'orphan instance' warning. I believe that these are harmless,

The downside of orphan instances is that GHC must visit every .hi file

that

...

has an orphan instance, just in case it contains a relevant instance decl. That slows down *every* compilation, whether or not it uses the instance.

The best way to get rid of it is to declare something local that is "from this module". Something like

data MyModule_Foo instance DataType (Dat MyModule_Foo) where ...

Now MyModule_Foo is a data type from the module currently being compiled. That tells GHC which .hi file to look in, and means the instance isn't orphan.

Yes I see, I noted it in the discussion and came up with a conservative approach (to be implemented).

Furter opinions? Please add to the wiki.

Thanks and cheers,

Gabor

...

Simon

| so is there a way to suppress them? Since I never insert tyvars in the | instance head, there should never be any overlap too. | | Cheers, | | Gabor | | On 6/30/14, Simon Peyton Jones wrote: | > You'll need to give a lot more info than this before I can help

Gabor.

...

| > Currently I have only the vaguest idea about what you are trying to | > accomplish. Is there a wiki page that describes the design (user's eye | > view) in detail? | > | > I see you have a branch. If you are stuck, and give me repro | instructions, | > I can attempt to help. | > | > Simon | > | > | -----Original Message----- | > | From: ghc-devs [mailto:ghc-devs-bounces@haskell.org] On Behalf Of | Gabor | > | Greif | > | Sent: 27 June 2014 17:51 | > | To: ghc-devs | > | Subject: Resolved+new Q: TypeLits question, how to build a Type | > | Application with Symbol index | > | | > | I succeeded to solve all of them :-) | > | | > | But now I am blocked on on a panic | > | | > | "not in scope during type checking, but it passed the renamer". | > | | > | I suspect that while "deriving Generic" some instances are defined in | > | some empty TcEnv, which does not contain my definition in context. | > | | > | Is there a way to inject some type constructor into the TcEnv? | > | | > | Thanks, | > | | > | Gabor | > | | > | On 6/27/14, Gabor Greif wrote: | > | > Hello devs, | > | > | > | > I have | > | > | > | > {{{ | > | > data D (n :: Symbol) | > | > }}} | > | > | > | > in my module, and I want to obtain a type | > | > | > | > {{{ | > | > D "YAY!" | > | > }}} | > | > | > | > programmatically. Where can I find code that performs this (or | > | > something similar)? | > | > | > | > 1) I have to look up |D| in the current TyEnv (what if it is in a | > | > specific module?), | > | > 2) I have to build the type index (of kind Symbol), this involves | > | > FastString, looks non-trivial, | > | > 3) Apply 1) on 2), this is easy. | > | > | > | > Any hints welcome! | > | > | > | > Thanks and cheers, | > | > | > | > Gabor | > | > | > | > | > | > PS: some morsels I have so far: | > | > | > | > for 1) | > | > compiler/prelude/PrelNames.lhs:gHC_GENERICS = mkBaseModule | (fsLit | > | > "GHC.Generics") | > | > | > | _______________________________________________ | > | ghc-devs mailing list | > | ghc-devs@haskell.org | > | http://www.haskell.org/mailman/listinfo/ghc-devs | >

_______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://www.haskell.org/mailman/listinfo/ghc-devs