new-typeable, new cast?

[José Pedro Magalhães]

Hi,

On Mon, Jul 22, 2013 at 10:19 AM, Richard Eisenberg <eir at cis.upenn.edu>wrote:

> There seems to be a small tangle. The proposal includes deprecating gcast1
> and gcast2 in favor of the poly-kinded gcast. But, there is a small
> discrepancy between these. Here are the type signatures:
>
>  gcast :: forall a b c. (Typeable a, Typeable b) => c a -> Maybe (c b)
>> gcast1 :: forall c t t' a. (Typeable (t :: * -> *), Typeable t')
>>        => c (t a) -> Maybe (c (t' a))
>>
>
> The difference is that gcast1 does *not* require the variable `a` to be
> Typeable, whereas defining gcast1 = gcast does require this. Not requiring
> `a` to be Typeable seems correct to me, as the type signature of gcast1
> requires both uses of `a` to be the same. But, gcast isn't smart enough to
> know that. Here are some ideas of how to proceed:
>
> - Keep gcast1 and gcast2 undeprecated.
>

I'd say we should go for this first option, because the second one is
pretty bad.


Cheers,
Pedro


> - Require clients to add more Typeable constraints (for example, in
> Data.Data) to get their code to compile with gcast.
> - Come up with some other workaround, but none is striking me at the
> moment.
>
> Thoughts?
>
> Richard
>
>
> On 2013-07-22 09:44, Richard Eisenberg wrote:
>
>> I was waiting to respond to Shachaf's email saying "pushed", but
>> instead, I have to say "currently validating".
>>
>> Expect this by the end of the day. Sorry it's taken so long!
>>
>> Richard
>>
>> On 2013-07-22 09:23, José Pedro Magalhães wrote:
>>
>>> Thanks for bringing this up again. This was started in my data-proxy
>>> branch of base [1],
>>> but never really finished. We definitely want to have this in 7.8, and
>>> I think there's
>>>  only some minor finishing work to do (check if we have all the
>>> instances we want,
>>> document, etc.). Perhaps you can look through what's there already,
>>> and what you
>>> think is missing? I'm more than happy to accept contributing patches
>>> too :-)
>>>
>>> Thanks,
>>> Pedro
>>>
>>> On Sun, Jul 21, 2013 at 3:09 AM, Shachaf Ben-Kiki <shachaf at gmail.com>
>>> wrote:
>>>
>>>  On Mon, Mar 4, 2013 at 11:12 AM, José Pedro Magalhães
>>>> <jpm at cs.uu.nl> wrote:
>>>>
>>>>> Hi,
>>>>>
>>>>> On Mon, Mar 4, 2013 at 4:51 PM, Richard Eisenberg
>>>>>
>>>> <eir at cis.upenn.edu> wrote:
>>>>
>>>>>
>>>>>> Unless I'm missing something, this all looks very
>>>>>>
>>>>> straightforward. The
>>>>
>>>>> implementation is there, already, in the guise of (gcast Refl).
>>>>>>
>>>>> We would
>>>>
>>>>> just shuffle the definitions around a bit. Am I indeed missing
>>>>>>
>>>>> something?
>>>>
>>>>>
>>>>>
>>>>> I think that is the case indeed. Though I agree that it would be
>>>>>
>>>> a nice
>>>>
>>>>> addition to Data.Typeable.
>>>>>
>>>>>
>>>>>
>>>> This thread is a few months old now, but it looks like people were
>>>> generally in favor of adding (gcast Refl) to Data.Typeable. I've
>>>> used
>>>> it in real code in at least one place since then (where I just
>>>> defined
>>>> it locally). It doesn't look like it's actually been added, though
>>>> --
>>>> is it planned to go into HEAD eventually?
>>>>
>>>>     Shachaf
>>>>
>>>
>>>
>>>
>>> Links:
>>> ------
>>> [1] https://github.com/ghc/**packages-base/tree/data-proxy<https://github.com/ghc/packages-base/tree/data-proxy>
>>>
>>
>> ______________________________**_________________
>> Libraries mailing list
>> Libraries at haskell.org
>> http://www.haskell.org/**mailman/listinfo/libraries<http://www.haskell.org/mailman/listinfo/libraries>
>>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/libraries/attachments/20130722/be5fb361/attachment.htm>