GenericsPropositionalEquality [Was: Resolved+new Q: TypeLits question, how to build a Type Application with Symbol index]
José Pedro Magalhães
jpm at cs.uu.nl
Thu Jul 3 08:57:37 UTC 2014
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 <ggreif at gmail.com> wrote:
> [added Pedro and Richard to "to:"]
>
> On 6/30/14, Simon Peyton Jones <simonpj at microsoft.com> 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 <simonpj at microsoft.com> 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 at 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 <ggreif at gmail.com> 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 at haskell.org
> > | > | http://www.haskell.org/mailman/listinfo/ghc-devs
> > | >
> >
> _______________________________________________
> ghc-devs mailing list
> ghc-devs at haskell.org
> http://www.haskell.org/mailman/listinfo/ghc-devs
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/ghc-devs/attachments/20140703/c83e7c45/attachment-0001.html>
More information about the ghc-devs
mailing list