new-typeable, new cast?
Richard Eisenberg
eir at cis.upenn.edu
Wed Jul 24 14:18:28 CEST 2013
Of course -- that worked. I was very muddled in my thinking yesterday,
figuring that the error was legitimate.
Thanks,
Richard
On 2013-07-23 20:11, Simon Peyton-Jones wrote:
> 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