new-typeable, new cast?

Richard Eisenberg eir at cis.upenn.edu
Tue Jul 23 16:11:33 CEST 2013 

Well, there was another surprise. Haddock can't deal with Proxy for some 
reason. (It dies with the error "synifyKind". I looked but couldn't 
figure out what was going on there.) I've posted a bug report on the 
haddock Trac (http://trac.haskell.org/haddock/ticket/242), but 
validation currently fails on the branch (data-proxy) with this work in 
it. So, I can't merge with master.

At this point, I'm going to wait until the haddock folks fix that bug, 
then assuming all is well, I will merge.

Richard



On 2013-07-23 09:59, Richard Eisenberg wrote:
> I think that we really only need (eqT :: (Typeable a, Typeable b) =>
> Maybe (a :=: b)). All of the gcasts can be defined in terms of that
> function.
> 
> However, I concretely propose (and plan to do) this: Leave gcast1 and
> gcast2 in and undeprecated. Simon is right that there is an infinite
> family of gcasts, and there may be no great reason to have gcast1 and
> gcast2 and none of the others, but there also doesn't seem to be a
> compelling reason to remove them (or deprecate them) and break code.
> In any case, this debate doesn't seem to be a good reason to hold up
> wrapping the rest of these details up, because we can always revisit
> and add or remove functions in the coming weeks. I'm not trying to
> ramrod my ideas through here, just trying to favor action over
> inaction -- anyone can feel free to come back and make edits after I
> push.
> 
> Barring another surprise, I believe I'll push before lunch (in the UK).
> 
> Richard
> 
> On 2013-07-23 03:04, Edward Kmett wrote:
>> If we have gcast1 then can't the others just be applications of that
>> under various wrappers?
>> 
>> In practice we should be able to implement gcast2 by working on a
>> single argument with a product kind, and so on and so forth, but we
>> need at least gcast1 as a base case.
>> 
>> In theory this is the more fundamental operation, and gcast is
>> defineable in terms of gcast1 with a wrapper with a unit-kinded
>> argument, but I wouldn't want to invert the relationship.
>> 
>> This is based on the same trick that Conor uses to show that a single
>> (poly-kinded) type argument is enough for all of the indexed monad
>> machinery, no matter how complicated it gets.
>> 
>> TL;DR We only need gcast1, the others are window-dressing.
>> 
>> -Edward
>> 
>> On Mon, Jul 22, 2013 at 9:31 PM, Simon Peyton-Jones
>> <simonpj at microsoft.com> wrote:
>> 
>>> Harump.  There is *still* an infinite family going on here, isn't
>>> there?
>>> 
>>> gcast :: forall a b c. (Typeable a, Typeable b) => c a -> Maybe (c
>>> b)
>>> 
>>> but what about this
>>> 
>>> gcast_2 :: forall a b c d e. (Typeable a, Typeable b, Typeable d,
>>> Typeable e)
>>>              => c a b -> c d e
>>> 
>>> Then, as you point out, we have gcast1 and 2 (etc).  And there are
>>> more.  What about
>>> 
>>> gcast1' :: forall c t a a'. (Typeable a, Typeable a')
>>>        => c (t a) -> Maybe (c (t a'))
>>> 
>>> One could imagine all sorts of combinations of bits that stay the
>>> same (and hence do not need to be Typeable) and bits that change
>>> (and hence do need to be Typable).
>>> 
>>> As Edward says, all these functions can be polykinded, which makes
>>> them more useful, but there still seem too many of them.
>>> 
>>> I wonder if we could instead make a combinatory library that lets
>>> us build these functions easily.  It think we are going to offer a
>>> function that computes an equality witness:
>>> 
>>> mkEqWit :: (Typable a, Typeable b) => Maybe (EQ a b)
>>> 
>>> Now we need to be able to compose witnesses:
>>> 
>>> appEqWit :: Eq a b -> Eq c d -> Eq (a c) (b d)
>>> reflEqWit :: Eq a a
>>> 
>>> Now, I think you can make all those other casts.
>>> 
>>> Would that do the job better?
>>> 
>>> Simon
>>> 
>>> |  -----Original Message-----
>>> |  From: Richard Eisenberg [mailto:eir at cis.upenn.edu]
>>> |  Sent: 22 July 2013 10:20
>>> |  To: José Pedro Magalhães
>>> |  Cc: Dimitrios Vytiniotis; Simon Peyton-Jones; Stephanie
>>> Weirich;
>>> |  josepedromagalhaes at gmail.com; libraries at haskell.org; Conor
>>> McBride
>>> |  Subject: Re: new-typeable, new cast?
>>> |
>>> 
>>> |  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.
>>> |  - 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 [1]
>>> |  >
>>> |  > _______________________________________________
>>> |  > Libraries mailing list
>>> |  > Libraries at haskell.org
>>> |  > http://www.haskell.org/mailman/listinfo/libraries [2]
>>> 
>>> _______________________________________________
>>> Libraries mailing list
>>> Libraries at haskell.org
>>> http://www.haskell.org/mailman/listinfo/libraries [2]
>> 
>> 
>> 
>> Links:
>> ------
>> [1] https://github.com/ghc/packages-base/tree/data-proxy
>> [2] http://www.haskell.org/mailman/listinfo/libraries
> 
> _______________________________________________
> Libraries mailing list
> Libraries at haskell.org
> http://www.haskell.org/mailman/listinfo/libraries

More information about the Libraries mailing list