new-typeable, new cast?

Richard Eisenberg eir at cis.upenn.edu
Tue Jul 23 10:59:32 CEST 2013 

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

More information about the Libraries mailing list