Data kind syntax
Trevor Elliott
trevor at galois.com
Fri Sep 13 17:01:06 UTC 2013
Hi Simon,
I'm free to talk now, do you mind doing a google hangout instead? I'm
having trouble getting skype installed on linux.
Thanks!
--trevor
On Fri 13 Sep 2013 08:22:18 AM PDT, Simon Peyton-Jones wrote:
> Trevor
>
> Thanks for working on the data-kind stuff. I've had a terribly crammed week, so I have only just looked at it properly.
>
> The first thing I look for is a wiki page articulating the design you have chosen. I think it's this:
> http://ghc.haskell.org/trac/ghc/wiki/GhcKinds/KindsWithoutData
> Is that it? By which I mean, are there really *zero* wrinkles, dark corners?
>
> Second, I'm not so happy about introducing a whole new constructor, KindDecl, in TyClDecl; plus associated clobber like a new data type TyConDecl. That brings lots of new code to treat those new declarations.
>
> All that new code makes sense for things that differ radically -- for example a class declaration is very different to a data type declaration. BUT this 'data kind' stuff is really very very similar to an ordinary data type declaration! You just treat a very restricted form.
>
> Moreover, it won't be long before Stephanie and Richard are seeking GADTs at the kind level, and then you'll have to expand it, duplicating yet more code.
>
> One way to recover the commonality would be to really treat it as a data type declaration, but to restrict what is actually brought into scope (just as 'data type' will do). But then what about the use of '*' in data kind?
> data kind T = A * | B T T
> Well, that's really just a parsing issue! The parser can parse it as a kind, so that it understands the star correctly. But having parsed it, we can treat it largely like an ordinary data type declaration, can't we?
>
> What do you think? Want to Skype? Sadly I'm out Mon/Tues.
>
> Simon
>
>
>
> | -----Original Message-----
> | From: ghc-commits [mailto:ghc-commits-bounces at haskell.org] On Behalf Of
> | git at git.haskell.org
> | Sent: 09 September 2013 04:54
> | To: ghc-commits at haskell.org
> | Subject: [commit: ghc] data-kind-syntax: Fix how we're using roles with
> | `data kind` declarations (13d4096)
> |
> | Repository : ssh://git@git.haskell.org/ghc
> |
> | On branch : data-kind-syntax
> | Link :
> | http://ghc.haskell.org/trac/ghc/changeset/13d4096e0668e9f80a8601122affc6
> | 4f8be295de/ghc
> |
> | >---------------------------------------------------------------
> |
> | commit 13d4096e0668e9f80a8601122affc64f8be295de
> | Author: Trevor Elliott <trevor at galois.com>
> | Date: Sun Sep 8 17:46:48 2013 -0700
> |
> | Fix how we're using roles with `data kind` declarations
> |
> |
> | >---------------------------------------------------------------
> |
> | 13d4096e0668e9f80a8601122affc64f8be295de
> | compiler/iface/IfaceSyn.lhs | 11 +++++++----
> | compiler/iface/MkIface.lhs | 3 ++-
> | compiler/iface/TcIface.lhs | 5 +++--
> | compiler/typecheck/TcTyClsDecls.lhs | 15 ++++++++-------
> | compiler/types/TyCon.lhs | 8 ++++----
> | 5 files changed, 24 insertions(+), 18 deletions(-)
> |
> | diff --git a/compiler/iface/IfaceSyn.lhs b/compiler/iface/IfaceSyn.lhs
> | index b12906b..ca772ac 100644
> | --- a/compiler/iface/IfaceSyn.lhs
> | +++ b/compiler/iface/IfaceSyn.lhs
> | @@ -436,19 +436,22 @@ instance Binary IfaceBang where
> |
> | data IfaceTyConDecl
> | = IfTyCon {
> | - ifTyConOcc :: OccName, -- constructor name
> | - ifTyConArgKs :: [IfaceKind] -- constructor argument kinds
> | + ifTyConOcc :: OccName, -- constructor name
> | + ifTyConArgKs :: [IfaceKind], -- constructor argument kinds
> | + ifTyConRoles :: [Role] -- constructor argument roles
> | }
> |
> | instance Binary IfaceTyConDecl where
> | - put_ bh (IfTyCon a1 a2) = do
> | + put_ bh (IfTyCon a1 a2 a3) = do
> | put_ bh (occNameFS a1)
> | put_ bh a2
> | + put_ bh a3
> | get bh = do
> | a1 <- get bh
> | a2 <- get bh
> | + a3 <- get bh
> | occ <- return $! mkOccNameFS tcName a1
> | - return (IfTyCon occ a2)
> | + return (IfTyCon occ a2 a3)
> |
> | data IfaceClsInst
> | = IfaceClsInst { ifInstCls :: IfExtName, -- See
> | comments with
> | diff --git a/compiler/iface/MkIface.lhs b/compiler/iface/MkIface.lhs
> | index 6764c91..3fff2b8 100644
> | --- a/compiler/iface/MkIface.lhs
> | +++ b/compiler/iface/MkIface.lhs
> | @@ -1566,7 +1566,8 @@ tyConToIfaceDecl env tycon
> |
> | ifaceTyConDecl ty_con
> | = IfTyCon { ifTyConOcc = getOccName (tyConName ty_con),
> | - ifTyConArgKs = map (tidyToIfaceType emptyTidyEnv)
> | args }
> | + ifTyConArgKs = map (tidyToIfaceType emptyTidyEnv)
> | args,
> | + ifTyConRoles = tyConRoles ty_con }
> | where
> | (args,_) = splitFunTys (tyConKind ty_con)
> |
> | diff --git a/compiler/iface/TcIface.lhs b/compiler/iface/TcIface.lhs
> | index d6b6a55..2d18a74 100644
> | --- a/compiler/iface/TcIface.lhs
> | +++ b/compiler/iface/TcIface.lhs
> | @@ -668,11 +668,12 @@ tcIfaceDataCons tycon_name tycon _ if_cons
> | ; return (HsUnpack (Just co)) }
> |
> | tcIfaceTyConDecl :: Kind -> KCon -> IfaceTyConDecl -> IfL TyCon
> | -tcIfaceTyConDecl kind kcon IfTyCon { ifTyConOcc = occ_name,
> | ifTyConArgKs = args }
> | +tcIfaceTyConDecl kind kcon IfTyCon { ifTyConOcc = occ_name,
> | ifTyConArgKs = args,
> | + ifTyConRoles = roles }
> | = do name <- lookupIfaceTop occ_name
> | -- See the comment in tc_con_decl of tcIfaceDataCons for why
> | forkM
> | kinds <- forkM pp_name (mapM tcIfaceKind args)
> | - return (mkDataKindTyCon kcon name (mkFunTys kinds kind))
> | + return (mkDataKindTyCon kcon name (mkFunTys kinds kind) roles)
> | where
> | pp_name = ptext (sLit "Type constructor") <+> ppr occ_name
> |
> | diff --git a/compiler/typecheck/TcTyClsDecls.lhs
> | b/compiler/typecheck/TcTyClsDecls.lhs
> | index 99a3584..d348e8b 100644
> | --- a/compiler/typecheck/TcTyClsDecls.lhs
> | +++ b/compiler/typecheck/TcTyClsDecls.lhs
> | @@ -118,7 +118,7 @@ tcTyAndClassDecls boot_details tyclds_s
> | -- remaining groups are typecheck in the extended global
> | env
> |
> | tcTyClGroup :: ModDetails -> TyClGroup Name -> TcM TcGblEnv
> | -tcTyClGroup boot_details decls
> | +tcTyClGroup _boot_details decls
> | | all (isKindDecl . unLoc) decls
> | = do (kcons, _) <- fixM $ \ ~(_, conss) -> do
> | let rec_info = panic "tcTyClGroup" "rec_info"
> | @@ -820,13 +820,12 @@ mkKindCon _rec_info tycons KindDecl { tcdLName =
> | L _ kind_name
> | kind_name
> | sKind
> | kvars
> | - [] -- XXX roles here?
> | + (replicate (length kvars) Nominal) -- no interesting kind
> | equality
> | Nothing
> | []
> | (DataKindTyCon tycons)
> | NoParentTyCon
> | - -- TODO, make the rec_info work
> | - NonRecursive --(rti_is_rec rec_info kind_name)
> | + NonRecursive -- XXX is this OK?
> | False
> | NotPromotable
> | where
> | @@ -838,8 +837,8 @@ mkKindCon _ _ _ =
> | panic "mkKindCon" "non 'data kind' declaration"
> |
> | tcKindDecl :: RecTyInfo -> TyClDecl Name -> TcM [TyCon]
> | -tcKindDecl rec_info KindDecl { tcdLName = L _ kind_name, tcdKVars =
> | lknames
> | - , tcdTypeCons = cons }
> | +tcKindDecl _rec_info KindDecl { tcdLName = L _ kind_name, tcdKVars =
> | lknames
> | + , tcdTypeCons = cons }
> | = do traceTc "tcKindDecl" (ppr kind_name)
> |
> | ~(ATyCon kcon) <- tcLookupGlobal kind_name
> | @@ -1394,7 +1393,9 @@ tcTyConDecl kvars kind TyConDecl { tycon_name =
> | name, tycon_details = details }
> | RecCon {} -> panic "tcTyConDecl" "unexpected record
> | constructor"
> | let (kcon,_) = splitTyConApp kind
> | con_kind = mkPiKinds kvars (mkFunTys ks kind)
> | - return (mkDataKindTyCon kcon (unLoc name) con_kind)
> | + roles = replicate (length kvars) Nominal
> | + ++ replicate (length ks) Representational
> | + return (mkDataKindTyCon kcon (unLoc name) con_kind roles)
> |
> |
> | \end{code}
> | diff --git a/compiler/types/TyCon.lhs b/compiler/types/TyCon.lhs
> | index 8ccbcc9..9308713 100644
> | --- a/compiler/types/TyCon.lhs
> | +++ b/compiler/types/TyCon.lhs
> | @@ -1087,13 +1087,13 @@ mkPromotedDataCon con name unique kind roles
> |
> | -- | Construct a type constructor for a type introduced by a 'data
> | kind'
> | -- declaration.
> | -mkDataKindTyCon :: TyCon -> Name -> Kind -> TyCon
> | -mkDataKindTyCon kc name kind
> | +mkDataKindTyCon :: TyCon -> Name -> Kind -> [Role] -> TyCon
> | +mkDataKindTyCon kc name kind roles
> | = PromotedDataCon {
> | tyConName = name,
> | tyConUnique = nameUnique name,
> | - tyConArity = 0,
> | - tc_roles = [], -- XXX is this correct?
> | + tyConArity = length roles,
> | + tc_roles = roles,
> | tc_kind = kind,
> | parentTyCon = kc
> | }
> |
> |
> | _______________________________________________
> | ghc-commits mailing list
> | ghc-commits at haskell.org
> | http://www.haskell.org/mailman/listinfo/ghc-commits
>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 2311 bytes
Desc: S/MIME Cryptographic Signature
URL: <http://www.haskell.org/pipermail/ghc-devs/attachments/20130913/9c0213e1/attachment.bin>
More information about the ghc-devs
mailing list