new-typeable, new cast?

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
2 messages Options
Reply | Threaded
Open this post in threaded view
|

new-typeable, new cast?

Simon Peyton Jones
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


Reply | Threaded
Open this post in threaded view
|

new-typeable, new cast?

Richard Eisenberg-2
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