Hi devs!
I guess I found a gap in the promotion mechanism: > data Prom1 = Symic Symbol gets promoted to to a kind (Prom1 :: BOX) with (Symic "AAA" :: Prom1). So far so good. But how can I define by promotion (Prom2 :: BOX) with (Typic Int :: Prom2) ? I'd like to write > data Prom2 = Typic Type but haven't found such a beast in TypeLits. So my question is basically, which type-level identifier promotes to (* :: BOX) when mentioned in a `data` definition? I am thankful for any hints! Cheers, Gabor |
Hi Gabor,
See http://hackage.haskell.org/trac/ghc/wiki/GhcKinds/KindsWithoutData Comments on that discussion are welcome. Cheers, Pedro On Tue, Apr 2, 2013 at 2:51 PM, Gabor Greif <ggreif at gmail.com> wrote: > Hi devs! > > I guess I found a gap in the promotion mechanism: > > > data Prom1 = Symic Symbol > > gets promoted to to a kind (Prom1 :: BOX) with (Symic "AAA" :: Prom1). > So far so good. > > But how can I define by promotion (Prom2 :: BOX) with (Typic Int :: Prom2) > ? > > I'd like to write > > > data Prom2 = Typic Type > > but haven't found such a beast in TypeLits. So my question is > basically, which type-level identifier promotes to (* :: BOX) when > mentioned in a `data` definition? > > I am thankful for any hints! > > Cheers, > > Gabor > > _______________________________________________ > ghc-devs mailing list > ghc-devs at haskell.org > http://www.haskell.org/mailman/listinfo/ghc-devs > An HTML attachment was scrubbed... URL: <http://www.haskell.org/pipermail/ghc-devs/attachments/20130402/fc70eb49/attachment-0001.htm> |
For more immediate satisfaction (i.e., before we get around to updating GHC in the manner suggested on the wiki page), you have to use a parameterized type and then specialize it to *:
> data Prom2 a = Typic a Now, we have (Prom2 * :: BOX) with (Typic Int :: Prom2 *). Unfortunately, we have no kind synonyms, so you have to insert the * parameter every time you want to use the Prom2 kind. As Pedro suggests, this is a known weakness of the current system. Richard On Apr 2, 2013, at 8:55 AM, Jos? Pedro Magalh?es <jpm at cs.uu.nl> wrote: > Hi Gabor, > > See http://hackage.haskell.org/trac/ghc/wiki/GhcKinds/KindsWithoutData > Comments on that discussion are welcome. > > > Cheers, > Pedro > > On Tue, Apr 2, 2013 at 2:51 PM, Gabor Greif <ggreif at gmail.com> wrote: > Hi devs! > > I guess I found a gap in the promotion mechanism: > > > data Prom1 = Symic Symbol > > gets promoted to to a kind (Prom1 :: BOX) with (Symic "AAA" :: Prom1). > So far so good. > > But how can I define by promotion (Prom2 :: BOX) with (Typic Int :: Prom2) ? > > I'd like to write > > > data Prom2 = Typic Type > > but haven't found such a beast in TypeLits. So my question is > basically, which type-level identifier promotes to (* :: BOX) when > mentioned in a `data` definition? > > I am thankful for any hints! > > Cheers, > > Gabor > > _______________________________________________ > 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/20130402/b6ab9a89/attachment.htm> |
Hello,
I've been using an existential quantifier for this. It looks weird (and I think we should fix this as discussed) but it is the current workaround: data MyKind = forall star. T star -- T :: * -> MyKind -Iavor On Tue, Apr 2, 2013 at 7:11 AM, Richard Eisenberg <eir at cis.upenn.edu> wrote: > For more immediate satisfaction (i.e., before we get around to updating > GHC in the manner suggested on the wiki page), you have to use a > parameterized type and then specialize it to *: > > > data Prom2 a = Typic a > > Now, we have (Prom2 * :: BOX) with (Typic Int :: Prom2 *). > > Unfortunately, we have no kind synonyms, so you have to insert the * > parameter every time you want to use the Prom2 kind. As Pedro suggests, > this is a known weakness of the current system. > > Richard > > On Apr 2, 2013, at 8:55 AM, Jos? Pedro Magalh?es <jpm at cs.uu.nl> wrote: > > Hi Gabor, > > See http://hackage.haskell.org/trac/ghc/wiki/GhcKinds/KindsWithoutData > Comments on that discussion are welcome. > > > Cheers, > Pedro > > On Tue, Apr 2, 2013 at 2:51 PM, Gabor Greif <ggreif at gmail.com> wrote: > >> Hi devs! >> >> I guess I found a gap in the promotion mechanism: >> >> > data Prom1 = Symic Symbol >> >> gets promoted to to a kind (Prom1 :: BOX) with (Symic "AAA" :: Prom1). >> So far so good. >> >> But how can I define by promotion (Prom2 :: BOX) with (Typic Int :: >> Prom2) ? >> >> I'd like to write >> >> > data Prom2 = Typic Type >> >> but haven't found such a beast in TypeLits. So my question is >> basically, which type-level identifier promotes to (* :: BOX) when >> mentioned in a `data` definition? >> >> I am thankful for any hints! >> >> Cheers, >> >> Gabor >> >> _______________________________________________ >> 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 > > > > _______________________________________________ > ghc-devs mailing list > ghc-devs at haskell.org > http://www.haskell.org/mailman/listinfo/ghc-devs > > An HTML attachment was scrubbed... URL: <http://www.haskell.org/pipermail/ghc-devs/attachments/20130402/e7064068/attachment.htm> |
For the record, I?m good with going ahead with ?Solution 2? on
http://hackage.haskell.org/trac/ghc/wiki/GhcKinds/KindsWithoutData if anyone wants to execute on it. Simon From: ghc-devs-bounces at haskell.org [mailto:ghc-devs-bounces at haskell.org] On Behalf Of Iavor Diatchki Sent: 02 April 2013 17:49 To: Richard Eisenberg Cc: Jos? Pedro Magalh?es; ghc-devs Subject: Re: What promotes to (* :: BOX) ? Hello, I've been using an existential quantifier for this. It looks weird (and I think we should fix this as discussed) but it is the current workaround: data MyKind = forall star. T star -- T :: * -> MyKind -Iavor On Tue, Apr 2, 2013 at 7:11 AM, Richard Eisenberg <eir at cis.upenn.edu<mailto:eir at cis.upenn.edu>> wrote: For more immediate satisfaction (i.e., before we get around to updating GHC in the manner suggested on the wiki page), you have to use a parameterized type and then specialize it to *: > data Prom2 a = Typic a Now, we have (Prom2 * :: BOX) with (Typic Int :: Prom2 *). Unfortunately, we have no kind synonyms, so you have to insert the * parameter every time you want to use the Prom2 kind. As Pedro suggests, this is a known weakness of the current system. Richard On Apr 2, 2013, at 8:55 AM, Jos? Pedro Magalh?es <jpm at cs.uu.nl<mailto:jpm at cs.uu.nl>> wrote: Hi Gabor, See http://hackage.haskell.org/trac/ghc/wiki/GhcKinds/KindsWithoutData Comments on that discussion are welcome. Cheers, Pedro On Tue, Apr 2, 2013 at 2:51 PM, Gabor Greif <ggreif at gmail.com<mailto:ggreif at gmail.com>> wrote: Hi devs! I guess I found a gap in the promotion mechanism: > data Prom1 = Symic Symbol gets promoted to to a kind (Prom1 :: BOX) with (Symic "AAA" :: Prom1). So far so good. But how can I define by promotion (Prom2 :: BOX) with (Typic Int :: Prom2) ? I'd like to write > data Prom2 = Typic Type but haven't found such a beast in TypeLits. So my question is basically, which type-level identifier promotes to (* :: BOX) when mentioned in a `data` definition? I am thankful for any hints! Cheers, Gabor _______________________________________________ ghc-devs mailing list ghc-devs at haskell.org<mailto:ghc-devs at haskell.org> http://www.haskell.org/mailman/listinfo/ghc-devs _______________________________________________ ghc-devs mailing list ghc-devs at haskell.org<mailto:ghc-devs at haskell.org> http://www.haskell.org/mailman/listinfo/ghc-devs _______________________________________________ ghc-devs mailing list ghc-devs at haskell.org<mailto: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/20130403/7ed8374e/attachment-0001.htm> |
Hi guys,
I'll have a go at implementing 'data kind'. I've been a bit busy lately but things are getting back to normal, and a colleague of mine is willing to help too, so hopefully we can get it done. -Iavor On Wed, Apr 3, 2013 at 4:24 AM, Simon Peyton-Jones <simonpj at microsoft.com>wrote: > For the record, I?m good with going ahead with ?Solution 2? on **** > > ** ** > > http://hackage.haskell.org/trac/ghc/wiki/GhcKinds/KindsWithoutData**** > > ** ** > > if anyone wants to execute on it.**** > > > Simon**** > > ** ** > > *From:* ghc-devs-bounces at haskell.org [mailto:ghc-devs-bounces at haskell.org] > *On Behalf Of *Iavor Diatchki > *Sent:* 02 April 2013 17:49 > *To:* Richard Eisenberg > *Cc:* Jos? Pedro Magalh?es; ghc-devs > *Subject:* Re: What promotes to (* :: BOX) ?**** > > ** ** > > Hello,**** > > ** ** > > I've been using an existential quantifier for this. It**** > > looks weird (and I think we should fix this as discussed) but it is the > current workaround:**** > > ** ** > > data MyKind = forall star. T star**** > > ** ** > > -- T :: * -> MyKind**** > > ** ** > > -Iavor**** > > ** ** > > ** ** > > ** ** > > On Tue, Apr 2, 2013 at 7:11 AM, Richard Eisenberg <eir at cis.upenn.edu> > wrote:**** > > For more immediate satisfaction (i.e., before we get around to updating > GHC in the manner suggested on the wiki page), you have to use a > parameterized type and then specialize it to *:**** > > ** ** > > > data Prom2 a = Typic a**** > > ** ** > > Now, we have (Prom2 * :: BOX) with (Typic Int :: Prom2 *).**** > > ** ** > > Unfortunately, we have no kind synonyms, so you have to insert the * > parameter every time you want to use the Prom2 kind. As Pedro suggests, > this is a known weakness of the current system.**** > > ** ** > > Richard**** > > ** ** > > On Apr 2, 2013, at 8:55 AM, Jos? Pedro Magalh?es <jpm at cs.uu.nl> wrote:**** > > > > **** > > Hi Gabor, > > See http://hackage.haskell.org/trac/ghc/wiki/GhcKinds/KindsWithoutData > Comments on that discussion are welcome. > > > Cheers, > Pedro**** > > On Tue, Apr 2, 2013 at 2:51 PM, Gabor Greif <ggreif at gmail.com> wrote:**** > > Hi devs! > > I guess I found a gap in the promotion mechanism: > > > data Prom1 = Symic Symbol > > gets promoted to to a kind (Prom1 :: BOX) with (Symic "AAA" :: Prom1). > So far so good. > > But how can I define by promotion (Prom2 :: BOX) with (Typic Int :: Prom2) > ? > > I'd like to write > > > data Prom2 = Typic Type > > but haven't found such a beast in TypeLits. So my question is > basically, which type-level identifier promotes to (* :: BOX) when > mentioned in a `data` definition? > > I am thankful for any hints! > > Cheers, > > Gabor > > _______________________________________________ > 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**** > > ** ** > > > _______________________________________________ > ghc-devs mailing list > ghc-devs at haskell.org > http://www.haskell.org/mailman/listinfo/ghc-devs**** > > ** ** > An HTML attachment was scrubbed... URL: <http://www.haskell.org/pipermail/ghc-devs/attachments/20130403/5dd6856c/attachment-0001.htm> |
In reply to this post by Iavor Diatchki
On 4/2/13, Iavor Diatchki <iavor.diatchki at gmail.com> wrote:
> Hello, > > I've been using an existential quantifier for this. It > looks weird (and I think we should fix this as discussed) but it is the > current workaround: > > data MyKind = forall star. T star > > -- T :: * -> MyKind Hi Iavor, thanks for the tip, this works nicely. I only have to restrict (t :: T *) everywhere a MyKind is needed, to get what I want. I tried Richard's solution too (with a universally quantified extra parameter). It appeared to work too, but it needed much more extra annotations. I believe a kind synonym would have helped, but we do not have those, right? Cheers, Gabor > > -Iavor > > > > > On Tue, Apr 2, 2013 at 7:11 AM, Richard Eisenberg <eir at cis.upenn.edu> > wrote: > >> For more immediate satisfaction (i.e., before we get around to updating >> GHC in the manner suggested on the wiki page), you have to use a >> parameterized type and then specialize it to *: >> >> > data Prom2 a = Typic a >> >> Now, we have (Prom2 * :: BOX) with (Typic Int :: Prom2 *). >> >> Unfortunately, we have no kind synonyms, so you have to insert the * >> parameter every time you want to use the Prom2 kind. As Pedro suggests, >> this is a known weakness of the current system. >> >> Richard >> >> On Apr 2, 2013, at 8:55 AM, Jos? Pedro Magalh?es <jpm at cs.uu.nl> wrote: >> >> Hi Gabor, >> >> See http://hackage.haskell.org/trac/ghc/wiki/GhcKinds/KindsWithoutData >> Comments on that discussion are welcome. >> >> >> Cheers, >> Pedro >> >> On Tue, Apr 2, 2013 at 2:51 PM, Gabor Greif <ggreif at gmail.com> wrote: >> >>> Hi devs! >>> >>> I guess I found a gap in the promotion mechanism: >>> >>> > data Prom1 = Symic Symbol >>> >>> gets promoted to to a kind (Prom1 :: BOX) with (Symic "AAA" :: Prom1). >>> So far so good. >>> >>> But how can I define by promotion (Prom2 :: BOX) with (Typic Int :: >>> Prom2) ? >>> >>> I'd like to write >>> >>> > data Prom2 = Typic Type >>> >>> but haven't found such a beast in TypeLits. So my question is >>> basically, which type-level identifier promotes to (* :: BOX) when >>> mentioned in a `data` definition? >>> >>> I am thankful for any hints! >>> >>> Cheers, >>> >>> Gabor >>> >>> _______________________________________________ >>> 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 >> >> >> >> _______________________________________________ >> ghc-devs mailing list >> ghc-devs at haskell.org >> http://www.haskell.org/mailman/listinfo/ghc-devs >> >> > |
On Wed, Apr 24, 2013 at 3:41 PM, Gabor Greif <ggreif at gmail.com> wrote:
> I believe a kind synonym would have helped, but we do not > have those, right? > Not yet, no. Cheers, Pedro -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://www.haskell.org/pipermail/ghc-devs/attachments/20130424/4b424612/attachment.htm> |
Free forum by Nabble | Edit this page |