What promotes to (* :: BOX) ?

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
8 messages Options
Reply | Threaded
Open this post in threaded view
|

What promotes to (* :: BOX) ?

Gabor Greif-2
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


Reply | Threaded
Open this post in threaded view
|

What promotes to (* :: BOX) ?

José Pedro Magalhães
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
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/ghc-devs/attachments/20130402/fc70eb49/attachment-0001.htm>

Reply | Threaded
Open this post in threaded view
|

What promotes to (* :: BOX) ?

Richard Eisenberg-2
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>

Reply | Threaded
Open this post in threaded view
|

What promotes to (* :: BOX) ?

Iavor Diatchki
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/20130402/e7064068/attachment.htm>

Reply | Threaded
Open this post in threaded view
|

What promotes to (* :: BOX) ?

Simon Peyton Jones
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>

Reply | Threaded
Open this post in threaded view
|

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>

Reply | Threaded
Open this post in threaded view
|

What promotes to (* :: BOX) ?

Gabor Greif-2
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
>>
>>
>


Reply | Threaded
Open this post in threaded view
|

What promotes to (* :: BOX) ?

José Pedro Magalhães
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>