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