new-typeable, new cast?
Simon Peyton-Jones
simonpj at microsoft.com
Tue Jul 23 21:11:13 CEST 2013
I'd suggest using "WithinType" as the argument to synifyType that's currently an error call in Haddock.Convert line 356
Simon
| -----Original Message-----
| From: Richard Eisenberg [mailto:eir at cis.upenn.edu]
| Sent: 23 July 2013 15:12
| To: Edward Kmett
| Cc: José Pedro Magalhães; Dimitrios Vytiniotis; Simon Peyton-Jones; Stephanie
| Weirich; josepedromagalhaes at gmail.com; libraries at haskell.org; Conor McBride
| Subject: Re: new-typeable, new cast?
|
| 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 ghc-devs
mailing list