new-typeable, new cast?
Edward Kmett
ekmett at gmail.com
Tue Jul 23 04:04:25 CEST 2013
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>
More information about the Libraries
mailing list