<div dir="ltr"><span style="font-family:arial,sans-serif;font-size:13px">Gabor and all,</span><div style="font-family:arial,sans-serif;font-size:13px"><br></div><div style="font-family:arial,sans-serif;font-size:13px">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|?</div>
<div style="font-family:arial,sans-serif;font-size:13px"><br></div><div style="font-family:arial,sans-serif;font-size:13px"><br></div><div style="font-family:arial,sans-serif;font-size:13px">Cheers,</div><div style="font-family:arial,sans-serif;font-size:13px">
Pedro</div><div style="font-family:arial,sans-serif;font-size:13px"><br></div><div style="font-family:arial,sans-serif;font-size:13px"><div><font face="courier new, monospace">{-# LANGUAGE TypeFamilies #-}</font></div>
<div><font face="courier new, monospace">{-# LANGUAGE GADTs #-}</font></div><div><font face="courier new, monospace">{-# LANGUAGE ScopedTypeVariables #-}</font></div><div><font face="courier new, monospace">{-# LANGUAGE DataKinds #-}</font></div>
<div><font face="courier new, monospace">{-# LANGUAGE PolyKinds #-}</font></div><div><font face="courier new, monospace">{-# LANGUAGE TypeOperators #-}</font></div><div><font face="courier new, monospace">{-# LANGUAGE DefaultSignatures #-}</font></div>
<div><font face="courier new, monospace">{-# LANGUAGE FlexibleContexts #-}</font></div><div><font face="courier new, monospace">{-# LANGUAGE FlexibleInstances #-}</font></div><div><font face="courier new, monospace">{-# LANGUAGE OverlappingInstances #-}</font></div>
<div><font face="courier new, monospace"><br></font></div><div><font face="courier new, monospace">module Test where</font></div><div><font face="courier new, monospace"><br></font></div><div><font face="courier new, monospace">import GHC.TypeLits</font></div>
<div><font face="courier new, monospace">import Data.Proxy ( Proxy(..) )</font></div><div><font face="courier new, monospace"><br></font></div><div><font face="courier new, monospace"><br></font></div><div><font face="courier new, monospace">--------------------------------------------------------------------------------</font></div>
<div><font face="courier new, monospace">-- Universe encoding</font></div><div><font face="courier new, monospace">--------------------------------------------------------------------------------</font></div><div><font face="courier new, monospace"><br>
</font></div><div><font face="courier new, monospace">data Un s = -- s is to always be set to *</font></div><div><font face="courier new, monospace"> -- Void (used for datatypes without constructors)</font></div><div><font face="courier new, monospace"> VV</font></div>
<div><font face="courier new, monospace"> </font></div><div><font face="courier new, monospace"> -- Unit</font></div><div><font face="courier new, monospace"> | UU</font></div><div><font face="courier new, monospace"><br>
</font></div><div><font face="courier new, monospace"> -- Meta-data</font></div><div><font face="courier new, monospace"> | MD MetaData (Un s)</font></div><div><font face="courier new, monospace"> | MC MetaCons (Un s)</font></div>
<div><font face="courier new, monospace"> | MS MetaSel (Un s)</font></div><div><font face="courier new, monospace"> </font></div><div><font face="courier new, monospace"> -- A parameter</font></div><div><font face="courier new, monospace"> | PAR</font></div>
<div><font face="courier new, monospace"> </font></div><div><font face="courier new, monospace"> -- Constants (either other parameters or recursion into types of kind *)</font></div><div><font face="courier new, monospace"> | KK PRU s</font></div>
<div><font face="courier new, monospace"><br></font></div><div><font face="courier new, monospace"> -- Recursion into types of kind (* -> *)</font></div><div><font face="courier new, monospace"> | REC SO (s -> s)</font></div>
<div><font face="courier new, monospace"> </font></div><div><font face="courier new, monospace"> -- Sum, product</font></div><div><font face="courier new, monospace"> | Un s :+: Un s</font></div><div><font face="courier new, monospace"> | Un s :**: Un s</font></div>
<div><font face="courier new, monospace"><br></font></div><div><font face="courier new, monospace"> -- Composition</font></div><div><font face="courier new, monospace"> | (s -> s) :.: Un s</font></div><div><font face="courier new, monospace"><br>
</font></div><div><font face="courier new, monospace"><br></font></div><div><font face="courier new, monospace">--------------------------------------------------------------------------------</font></div><div><font face="courier new, monospace">-- Meta-data</font></div>
<div><font face="courier new, monospace">--------------------------------------------------------------------------------</font></div><div><font face="courier new, monospace"><br></font></div><div><font face="courier new, monospace">-- Parameter, Recursive occurrence, or Unknown/other</font></div>
<div><font face="courier new, monospace">data PRU = P | R SO | U</font></div><div><font face="courier new, monospace"><br></font></div><div><font face="courier new, monospace">-- Self or Other</font></div><div><font face="courier new, monospace">data SO = S | O</font></div>
<div><font face="courier new, monospace"><br></font></div><div><font face="courier new, monospace">data MetaData = MetaData { dataName :: Symbol, dataModule :: Symbol }</font></div><div><font face="courier new, monospace"><br>
</font></div><div><font face="courier new, monospace">data MetaCons = MetaCons { conName :: Symbol</font></div><div><font face="courier new, monospace"> , conFixity :: Fixity</font></div><div>
<font face="courier new, monospace"> , conIsRecord :: Bool }</font></div><div><font face="courier new, monospace"><br></font></div><div><font face="courier new, monospace">data Fixity = Prefix | Infix Associativity Nat</font></div>
<div><font face="courier new, monospace"><br></font></div><div><font face="courier new, monospace">data Associativity = LeftAssociative </font></div><div><font face="courier new, monospace"> | RightAssociative</font></div>
<div><font face="courier new, monospace"> | NotAssociative</font></div><div><font face="courier new, monospace"> deriving (Eq, Show, Ord, Read)</font></div><div><font face="courier new, monospace"><br>
</font></div><div><font face="courier new, monospace">data MetaSel = MetaSel { selName :: Maybe Symbol }</font></div><div><font face="courier new, monospace"><br></font></div><div><font face="courier new, monospace">--------------------------------------------------------------------------------</font></div>
<div><font face="courier new, monospace">-- Interpretation (as a GADT)</font></div><div><font face="courier new, monospace">--------------------------------------------------------------------------------</font></div><div>
<font face="courier new, monospace"><br></font></div><div><font face="courier new, monospace">data In (u :: Un *) (p :: *) :: * where</font></div><div><font face="courier new, monospace"><br></font></div><div><font face="courier new, monospace"> -- No interpretation for VV, as it shouldn't map to any value</font></div>
<div><font face="courier new, monospace"> </font></div><div><font face="courier new, monospace"> -- Unit</font></div><div><font face="courier new, monospace"> U1 :: In UU p</font></div><div><font face="courier new, monospace"> </font></div>
<div><font face="courier new, monospace"> -- Datatype meta-data</font></div><div><font face="courier new, monospace"> D1 :: { unD1 :: In a p } -> In (MD md a) p</font></div><div><font face="courier new, monospace"><br>
</font></div><div><font face="courier new, monospace"> -- Constructor meta-data</font></div><div><font face="courier new, monospace"> C1 :: { unC1 :: In a p } -> In (MC mc a) p</font></div><div><font face="courier new, monospace"><br>
</font></div><div><font face="courier new, monospace"> -- Selector meta-data</font></div><div><font face="courier new, monospace"> S1 :: { unS1 :: In a p } -> In (MS ms a) p</font></div><div><font face="courier new, monospace"><br>
</font></div><div><font face="courier new, monospace"> -- The parameter</font></div><div><font face="courier new, monospace"> Par1 :: { unPar1 :: p } -> In PAR p</font></div><div><font face="courier new, monospace"> </font></div>
<div><font face="courier new, monospace"> -- Constants</font></div><div><font face="courier new, monospace"> K1 :: { unK1 :: x} -> In (KK pru x) p</font></div><div><font face="courier new, monospace"><br></font></div>
<div><font face="courier new, monospace"> -- Recursion</font></div><div><font face="courier new, monospace"> Rec1 :: { unRec1 :: f p } -> In (REC i f) p</font></div><div><font face="courier new, monospace"> </font></div>
<div><font face="courier new, monospace"> -- Sum</font></div><div><font face="courier new, monospace"> L1 :: In f p -> In (f :+: g) p</font></div><div><font face="courier new, monospace"> R1 :: In g p -> In (f :+: g) p</font></div>
<div><font face="courier new, monospace"><br></font></div><div><font face="courier new, monospace"> -- Product</font></div><div><font face="courier new, monospace"> (:*:) :: In f p -> In g p -> In (f :**: g) p</font></div>
<div><font face="courier new, monospace"><br></font></div><div><font face="courier new, monospace"> -- Composition</font></div><div><font face="courier new, monospace"> Comp1 :: { unComp1 :: f (In g p) } -> In (f :.: g) p</font></div>
<div><font face="courier new, monospace"><br></font></div><div><font face="courier new, monospace"><br></font></div><div><font face="courier new, monospace">--------------------------------------------------------------------------------</font></div>
<div><font face="courier new, monospace">-- Conversions to/from user datatypes</font></div><div><font face="courier new, monospace">--------------------------------------------------------------------------------</font></div>
<div><font face="courier new, monospace"><br></font></div><div><font face="courier new, monospace">class Generic (a :: *) where</font></div><div><font face="courier new, monospace"> type Rep a :: Un *</font></div><div><font face="courier new, monospace"><br>
</font></div><div><font face="courier new, monospace"> from :: a -> In (Rep a) p</font></div><div><font face="courier new, monospace"> to :: In (Rep a) p -> a</font></div><div><font face="courier new, monospace"><br>
</font></div><div><font face="courier new, monospace"><br></font></div><div><font face="courier new, monospace">class Generic1 (f :: * -> *) where</font></div><div><font face="courier new, monospace"> type Rep1 f :: Un *</font></div>
<div><font face="courier new, monospace"><br></font></div><div><font face="courier new, monospace"> from1 :: f p -> In (Rep1 f) p</font></div><div><font face="courier new, monospace"> to1 :: In (Rep1 f) p -> f p</font></div>
<div><font face="courier new, monospace"><br></font></div><div><font face="courier new, monospace">--------------------------------------------------------------------------------</font></div><div><font face="courier new, monospace">-- Example encoding: lists (with some twisted meta-data for example purposes)</font></div>
<div><font face="courier new, monospace">--------------------------------------------------------------------------------</font></div><div><font face="courier new, monospace"><br></font></div><div><font face="courier new, monospace">instance Generic [a] where</font></div>
<div><font face="courier new, monospace"> type Rep [a] = MD ('MetaData "[]" "Prelude")</font></div><div><font face="courier new, monospace"> (MC ('MetaCons "[]" Prefix False) UU</font></div>
<div><font face="courier new, monospace"> :+: MC ('MetaCons ":" (Infix RightAssociative 5) False) </font></div><div><font face="courier new, monospace"> ( MS ('MetaSel (Just "el")) (KK P a)</font></div>
<div><font face="courier new, monospace"> :**: MS ('MetaSel Nothing) (KK (R S) [a])))</font></div><div><font face="courier new, monospace"><br></font></div><div><font face="courier new, monospace"> from [] = D1 (L1 (C1 U1))</font></div>
<div><font face="courier new, monospace"> from (h:t) = D1 (R1 (C1 (S1 (K1 h) :*: S1 (K1 t))))</font></div><div><font face="courier new, monospace"><br></font></div><div><font face="courier new, monospace"> to (D1 (L1 (C1 U1))) = []</font></div>
<div><font face="courier new, monospace"> to (D1 (R1 (C1 (S1 (K1 h) :*: S1 (K1 t))))) = h:t</font></div><div><font face="courier new, monospace"><br></font></div><div><font face="courier new, monospace">-- Should have meta-information as well, but the one above is enough for now</font></div>
<div><font face="courier new, monospace">instance Generic1 [] where</font></div><div><font face="courier new, monospace"> type Rep1 [] = UU :+: (PAR :**: REC S [])</font></div><div><font face="courier new, monospace"><br>
</font></div><div><font face="courier new, monospace"> from1 [] = L1 U1</font></div><div><font face="courier new, monospace"> from1 (h:t) = R1 (Par1 h :*: Rec1 t)</font></div><div><font face="courier new, monospace"><br>
</font></div><div><font face="courier new, monospace"> to1 (L1 U1) = []</font></div><div><font face="courier new, monospace"> to1 (R1 (Par1 h :*: Rec1 t)) = h:t</font></div><div><font face="courier new, monospace"><br>
</font></div><div><font face="courier new, monospace">--------------------------------------------------------------------------------</font></div><div><font face="courier new, monospace">-- Show</font></div><div><font face="courier new, monospace">--------------------------------------------------------------------------------</font></div>
<div><font face="courier new, monospace"><br></font></div><div><font face="courier new, monospace">class GShow (r :: Un *) where</font></div><div><font face="courier new, monospace"> gshow :: In r p -> String</font></div>
<div><font face="courier new, monospace"><br></font></div><div><font face="courier new, monospace">instance (Show' a) => GShow (KK pru a) where</font></div><div><font face="courier new, monospace"> gshow (K1 a) = show' a</font></div>
<div><font face="courier new, monospace"><br></font></div><div><font face="courier new, monospace">instance GShow UU where</font></div><div><font face="courier new, monospace"> gshow U1 = ""</font></div><div><font face="courier new, monospace"><br>
</font></div><div><font face="courier new, monospace">instance (GShow r) => GShow (MD md r) where</font></div><div><font face="courier new, monospace"> gshow (D1 x) = gshow x</font></div><div><font face="courier new, monospace"><br>
</font></div><div><font face="courier new, monospace">-- We can now match meta-data properties at the type level</font></div><div><font face="courier new, monospace">instance (KnownSymbol name) => GShow (MC ('MetaCons name Prefix isRec) UU) where</font></div>
<div><font face="courier new, monospace"> gshow (C1 x) = symbolVal (Proxy :: Proxy name)</font></div><div><font face="courier new, monospace"><br></font></div><div><font face="courier new, monospace">instance (KnownSymbol name, GShow r)</font></div>
<div><font face="courier new, monospace"> => GShow (MC ('MetaCons name Prefix isRec) r) where</font></div><div><font face="courier new, monospace"> gshow (C1 x) = "(" ++ symbolVal (Proxy :: Proxy name) ++ " " ++ gshow x ++ ")"</font></div>
<div><font face="courier new, monospace"><br></font></div><div><font face="courier new, monospace">-- Note how we assume that the structure under an Infix MC must be a product.</font></div><div><font face="courier new, monospace">-- This is not encoded in the universe, regrettably, and might lead to "missing</font></div>
<div><font face="courier new, monospace">-- instance" errors if we're not careful.</font></div><div><font face="courier new, monospace">instance (KnownSymbol name, GShow a, GShow b)</font></div><div><font face="courier new, monospace"> => GShow (MC ('MetaCons name (Infix assoc fix) isRec) (a :**: b)) where</font></div>
<div><font face="courier new, monospace"> gshow (C1 (a :*: b)) = "(" ++ gshow a ++ " "</font></div><div><font face="courier new, monospace"> ++ symbolVal (Proxy :: Proxy name) ++ " "</font></div>
<div><font face="courier new, monospace"> ++ gshow b ++ ")"</font></div><div><font face="courier new, monospace"><br></font></div><div><font face="courier new, monospace">instance (GShow r) => GShow (MS ('MetaSel Nothing) r) where</font></div>
<div><font face="courier new, monospace"> gshow (S1 x) = gshow x</font></div><div><font face="courier new, monospace"><br></font></div><div><font face="courier new, monospace">instance (KnownSymbol name, GShow r)</font></div>
<div><font face="courier new, monospace"> => GShow (MS ('MetaSel (Just name)) r) where</font></div><div><font face="courier new, monospace"> gshow (S1 x) = "{ " ++ symbolVal (Proxy :: Proxy name) ++ " = "</font></div>
<div><font face="courier new, monospace"> ++ gshow x ++ " }"</font></div><div><font face="courier new, monospace"><br></font></div><div><font face="courier new, monospace">instance (GShow a, GShow b) => GShow (a :+: b) where</font></div>
<div><font face="courier new, monospace"> gshow (L1 a) = gshow a</font></div><div><font face="courier new, monospace"> gshow (R1 b) = gshow b</font></div><div><font face="courier new, monospace"><br></font></div><div><font face="courier new, monospace">instance (GShow a, GShow b) => GShow (a :**: b) where</font></div>
<div><font face="courier new, monospace"> gshow (a :*: b) = gshow a ++ " " ++ gshow b</font></div><div><font face="courier new, monospace"><br></font></div><div><font face="courier new, monospace">-- User-facing class</font></div>
<div><font face="courier new, monospace">class Show' (a :: *) where</font></div><div><font face="courier new, monospace"> show' :: a -> String</font></div><div><font face="courier new, monospace"><br></font></div>
<div><font face="courier new, monospace"> default show' :: (Generic a, GShow (Rep a)) => a -> String</font></div><div><font face="courier new, monospace"> show' = gshow . from</font></div><div><font face="courier new, monospace"><br>
</font></div><div><font face="courier new, monospace">--------------------------------------------------------------------------------</font></div><div><font face="courier new, monospace">-- Test</font></div><div><font face="courier new, monospace">--------------------------------------------------------------------------------</font></div>
<div><font face="courier new, monospace"><br></font></div><div><font face="courier new, monospace">instance Show' Int where show' = show</font></div><div><font face="courier new, monospace">instance (Show' a) => Show' [a]</font></div>
<div><font face="courier new, monospace"><br></font></div><div><font face="courier new, monospace">test1, test2 :: String</font></div><div><font face="courier new, monospace">test1 = show' ([] :: [Int]) -- "[]"</font></div>
<div><font face="courier new, monospace">test2 = show' [1,2::Int] -- "({ el = 1 } : ({ el = 2 } : []))"</font></div></div></div><div class="gmail_extra"><br><br><div class="gmail_quote">On Wed, Jul 2, 2014 at 1:42 PM, Gabor Greif <span dir="ltr"><<a href="mailto:ggreif@gmail.com" target="_blank">ggreif@gmail.com</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">[added Pedro and Richard to "to:"]<br>
<br>
On 6/30/14, Simon Peyton Jones <<a href="mailto:simonpj@microsoft.com">simonpj@microsoft.com</a>> wrote:<br>
> | Yes I have a branch, and it works! A bunch of things is still missing<br>
> | (notably record selectors), but I have a proof-of-concept with a gdiff<br>
> | library hooked up to GHC.Generics, and by appealing to type-level<br>
> | reasoning I can obtain a difference tree from True to False (which<br>
> | looks good) by using the reflection (i.e. class Generic) only, no need<br>
> | for TH or hand-coding. Comparing bigger trees (and then 'patch'ing<br>
> | them) appears to be SMOP from here.<br>
><br>
> Do you have a wiki page explaining what "it" is (the thing that works).<br>
<br>
Here is a wiki page<br>
<br>
<a href="https://ghc.haskell.org/trac/ghc/wiki/GenericsPropositionalEquality" target="_blank">https://ghc.haskell.org/trac/ghc/wiki/GenericsPropositionalEquality</a><br>
<br>
you all are invited to make suggestions, ask questions and generally beautify.<br>
<br>
><br>
> | instance Datatype (Dat "MyModule" "Foo") ...<br>
> |<br>
> | I get an 'orphan instance' warning. I believe that these are harmless,<br>
><br>
> The downside of orphan instances is that GHC must visit every .hi file that<br>
> has an orphan instance, just in case it contains a relevant instance decl.<br>
> That slows down *every* compilation, whether or not it uses the instance.<br>
><br>
> The best way to get rid of it is to declare something local that is "from<br>
> this module". Something like<br>
><br>
> data MyModule_Foo<br>
> instance DataType (Dat MyModule_Foo) where ...<br>
><br>
> Now MyModule_Foo is a data type from the module currently being compiled.<br>
> That tells GHC which .hi file to look in, and means the instance isn't<br>
> orphan.<br>
<br>
Yes I see, I noted it in the discussion and came up with a<br>
conservative approach (to be implemented).<br>
<br>
Furter opinions? Please add to the wiki.<br>
<br>
Thanks and cheers,<br>
<br>
Gabor<br>
<br>
><br>
> Simon<br>
><br>
> | so is there a way to suppress them? Since I never insert tyvars in the<br>
> | instance head, there should never be any overlap too.<br>
> |<br>
> | Cheers,<br>
> |<br>
> | Gabor<br>
> |<br>
> | On 6/30/14, Simon Peyton Jones <<a href="mailto:simonpj@microsoft.com">simonpj@microsoft.com</a>> wrote:<br>
> | > You'll need to give a lot more info than this before I can help Gabor.<br>
> | > Currently I have only the vaguest idea about what you are trying to<br>
> | > accomplish. Is there a wiki page that describes the design (user's eye<br>
> | > view) in detail?<br>
> | ><br>
> | > I see you have a branch. If you are stuck, and give me repro<br>
> | instructions,<br>
> | > I can attempt to help.<br>
> | ><br>
> | > Simon<br>
> | ><br>
> | > | -----Original Message-----<br>
> | > | From: ghc-devs [mailto:<a href="mailto:ghc-devs-bounces@haskell.org">ghc-devs-bounces@haskell.org</a>] On Behalf Of<br>
> | Gabor<br>
> | > | Greif<br>
> | > | Sent: 27 June 2014 17:51<br>
> | > | To: ghc-devs<br>
> | > | Subject: Resolved+new Q: TypeLits question, how to build a Type<br>
> | > | Application with Symbol index<br>
> | > |<br>
> | > | I succeeded to solve all of them :-)<br>
> | > |<br>
> | > | But now I am blocked on on a panic<br>
> | > |<br>
> | > | "not in scope during type checking, but it passed the renamer".<br>
> | > |<br>
> | > | I suspect that while "deriving Generic" some instances are defined in<br>
> | > | some empty TcEnv, which does not contain my definition in context.<br>
> | > |<br>
> | > | Is there a way to inject some type constructor into the TcEnv?<br>
> | > |<br>
> | > | Thanks,<br>
> | > |<br>
> | > | Gabor<br>
> | > |<br>
> | > | On 6/27/14, Gabor Greif <<a href="mailto:ggreif@gmail.com">ggreif@gmail.com</a>> wrote:<br>
> | > | > Hello devs,<br>
> | > | ><br>
> | > | > I have<br>
> | > | ><br>
> | > | > {{{<br>
> | > | > data D (n :: Symbol)<br>
> | > | > }}}<br>
> | > | ><br>
> | > | > in my module, and I want to obtain a type<br>
> | > | ><br>
> | > | > {{{<br>
> | > | > D "YAY!"<br>
> | > | > }}}<br>
> | > | ><br>
> | > | > programmatically. Where can I find code that performs this (or<br>
> | > | > something similar)?<br>
> | > | ><br>
> | > | > 1) I have to look up |D| in the current TyEnv (what if it is in a<br>
> | > | > specific module?),<br>
> | > | > 2) I have to build the type index (of kind Symbol), this involves<br>
> | > | > FastString, looks non-trivial,<br>
> | > | > 3) Apply 1) on 2), this is easy.<br>
> | > | ><br>
> | > | > Any hints welcome!<br>
> | > | ><br>
> | > | > Thanks and cheers,<br>
> | > | ><br>
> | > | > Gabor<br>
> | > | ><br>
> | > | ><br>
> | > | > PS: some morsels I have so far:<br>
> | > | ><br>
> | > | > for 1)<br>
> | > | > compiler/prelude/PrelNames.lhs:gHC_GENERICS = mkBaseModule<br>
> | (fsLit<br>
> | > | > "GHC.Generics")<br>
> | > | ><br>
> | > | _______________________________________________<br>
> | > | ghc-devs mailing list<br>
> | > | <a href="mailto:ghc-devs@haskell.org">ghc-devs@haskell.org</a><br>
> | > | <a href="http://www.haskell.org/mailman/listinfo/ghc-devs" target="_blank">http://www.haskell.org/mailman/listinfo/ghc-devs</a><br>
> | ><br>
><br>
_______________________________________________<br>
ghc-devs mailing list<br>
<a href="mailto:ghc-devs@haskell.org">ghc-devs@haskell.org</a><br>
<a href="http://www.haskell.org/mailman/listinfo/ghc-devs" target="_blank">http://www.haskell.org/mailman/listinfo/ghc-devs</a><br>
</blockquote></div><br></div>