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 |
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 |
Free forum by Nabble | Edit this page |