new-typeable, new cast?

[Edward Kmett]

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
> |  >
> |  > _______________________________________________
> |  > Libraries mailing list
> |  > Libraries at haskell.org
> |  > http://www.haskell.org/mailman/listinfo/libraries
>
> _______________________________________________
> Libraries mailing list
> Libraries at haskell.org
> http://www.haskell.org/mailman/listinfo/libraries
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/libraries/attachments/20130722/969e96b0/attachment.htm>