What promotes to (* :: BOX) ?

[Iavor Diatchki]

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****
>
> ** **
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/ghc-devs/attachments/20130403/5dd6856c/attachment-0001.htm>