Hi Jan, A few questions came up this morning while speaking Andres Loeh about injective type families: 1. Should this feature be placed behind a LANGUAGE pragma? Afterall, functional dependencies feel very similar and in this case we require a pragma. Now would be the last opportunity to change this. 2. Could you perhaps add some text to better motivate the feature in the users guide? Referring to the paper for the details of semantics of the feature and its implementation is fine, but expecting a new user to refer to the paper to even know *why* they might want to use it seems a bit unfriendly. Thanks! Cheers, - Ben
Ben,
1. Should this feature be placed behind a LANGUAGE pragma? No, I don't think it should. I consider it a tiny addition to TypeFamilies that is not worth having its separate pragma. Injective TFs are fully backwards compatible, so no existing code will be broken.
2. Could you perhaps add some text to better motivate the feature in the users guide? Done. Tell me whether you like the new version.
BTW do we still have nightly builds of User's Guide? Janek
Referring to the paper for the details of semantics of the feature and its implementation is fine, but expecting a new user to refer to the paper to even know *why* they might want to use it seems a bit unfriendly.
Thanks!
Cheers,
- Ben
--- Politechnika Łódzka Lodz University of Technology Treść tej wiadomości zawiera informacje przeznaczone tylko dla adresata. Jeżeli nie jesteście Państwo jej adresatem, bądź otrzymaliście ją przez pomyłkę prosimy o powiadomienie o tym nadawcy oraz trwałe jej usunięcie. This email contains information intended solely for the use of the individual to whom it is addressed. If you are not the intended recipient or if you have received this message in error, please notify the sender and delete it from your system.
Jan Stolarek
Ben,
1. Should this feature be placed behind a LANGUAGE pragma?
No, I don't think it should. I consider it a tiny addition to TypeFamilies that is not worth having its separate pragma. Injective TFs are fully backwards compatible, so no existing code will be broken.
That being said, it does claim new syntax and consequently would be rather difficult to back out if we realize that this implementation isn't the right direction. I don't have a strong opinion here, just playing devil's advocate.
2. Could you perhaps add some text to better motivate the feature in the users guide? Done. Tell me whether you like the new version.
Definitely better. Thanks for the quick turnaround!
BTW do we still have nightly builds of User's Guide?
I have a script that I periodically run to push the documentation from my test builds here: http://downloads.haskell.org/~ghc/master/users-guide// It's updated pretty close to daily. Cheers, - Ben
Hi.
No, I don't think it should. I consider it a tiny addition to TypeFamilies that is not worth having its separate pragma. Injective TFs are fully backwards compatible, so no existing code will be broken.
That being said, it does claim new syntax and consequently would be rather difficult to back out if we realize that this implementation isn't the right direction. I don't have a strong opinion here, just playing devil's advocate.
I think it should be a new language extension. Forward compatibility on its own is not a sufficient argument. Aren't e.g. GADTs forward compatible? Or functional dependencies? Or flexible instances? Yet all of these also have separate language extensions. If I actually want to write backward-compatible type family code using GHC-8.0, I'd prefer to be able to enable TypeFamilies yet not InjectiveTypeFamilies, and have GHC check that I am in the common subset. Also, I think it would be nice to be able to track how many packages will make use of TypeFamilies and InjectiveTypeFamilies separately from each other. Cheers, Andres
If I actually want to write backward-compatible type family code using GHC-8.0, I'd prefer to be able to enable TypeFamilies yet not InjectiveTypeFamilies, and have GHC check that I am in the common subset. Good point. I wonder if others agree.
Janek --- Politechnika Łódzka Lodz University of Technology Treść tej wiadomości zawiera informacje przeznaczone tylko dla adresata. Jeżeli nie jesteście Państwo jej adresatem, bądź otrzymaliście ją przez pomyłkę prosimy o powiadomienie o tym nadawcy oraz trwałe jej usunięcie. This email contains information intended solely for the use of the individual to whom it is addressed. If you are not the intended recipient or if you have received this message in error, please notify the sender and delete it from your system.
| > If I actually want to write backward-compatible type family code | using | > GHC-8.0, I'd prefer to be able to enable TypeFamilies yet not | > InjectiveTypeFamilies, and have GHC check that I am in the common | subset. | Good point. I wonder if others agree. Yes I agree (see my last email). But I think the same flag should deal with the richer form of improvement in the new branch, eg type family F a b = r | r a -> b, r b -> a Is "InjectiveTypeFamilies" a good name for this? Or "TypeFamilyDependencies"? Or what? Simon
Is "InjectiveTypeFamilies" a good name for this? Or "TypeFamilyDependencies"? Or what? My vote for "InjectiveTypeFamilies".
Janek --- Politechnika Łódzka Lodz University of Technology Treść tej wiadomości zawiera informacje przeznaczone tylko dla adresata. Jeżeli nie jesteście Państwo jej adresatem, bądź otrzymaliście ją przez pomyłkę prosimy o powiadomienie o tym nadawcy oraz trwałe jej usunięcie. This email contains information intended solely for the use of the individual to whom it is addressed. If you are not the intended recipient or if you have received this message in error, please notify the sender and delete it from your system.
I'm joining this conversation late, but I favor TypeFamilyDependencies over InjectiveTypeFamilies. We use the annotations for things other than injectivity! For example,
type family Plus a b = r | r a -> b, r b -> a
is not injective under any common understanding of the word. And the argument-to-argument dependencies Simon has been musing about are even further from the meaning of "injective".
Richard
On Jan 8, 2016, at 6:43 AM, Jan Stolarek
Is "InjectiveTypeFamilies" a good name for this? Or "TypeFamilyDependencies"? Or what? My vote for "InjectiveTypeFamilies".
Janek
--- Politechnika Łódzka Lodz University of Technology
Treść tej wiadomości zawiera informacje przeznaczone tylko dla adresata. Jeżeli nie jesteście Państwo jej adresatem, bądź otrzymaliście ją przez pomyłkę prosimy o powiadomienie o tym nadawcy oraz trwałe jej usunięcie.
This email contains information intended solely for the use of the individual to whom it is addressed. If you are not the intended recipient or if you have received this message in error, please notify the sender and delete it from your system. _______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
I agree!
| -----Original Message-----
| From: Richard Eisenberg [mailto:eir@cis.upenn.edu]
| Sent: 11 January 2016 16:35
| To: Jan Stolarek
Simon Peyton Jones
I agree!
Currently InjectiveTypeFamilies is in the tree but it's not too late to change it. Of course, this means that we need to decide what to do about the -rc1 release. I finished the builds earlier today but have been sitting on them to check over things when I feel less ill. Given the number of rather serious issues still outstanding I was a bit reluctant to even go ahead with the builds, but thought in the name of release early, release often it would be best just to get something out there, however unperfect. Perhaps I'll just wait until the meeting tomorrow before doing any further on the rc front. Cheers, - Ben
I'm joining this conversation late, but I favor TypeFamilyDependencies over InjectiveTypeFamilies. We use the annotations for things other than injectivity! For example,
type family Plus a b = r | r a -> b, r b -> a
is not injective under any common understanding of the word. But that is not implemented yet and thus will not make it into GHC 8.0. Following earlier argumentation, once we have generalized injectivity we should put it into a separate extension. So I'd say we stick with InjectiveTypeFamilies for currently implemented features and put the new ones in TypeFamilyDependencies.
That said, I don't like the idea that every addition to a language extension means creating a separate language extension. Janek --- Politechnika Łódzka Lodz University of Technology Treść tej wiadomości zawiera informacje przeznaczone tylko dla adresata. Jeżeli nie jesteście Państwo jej adresatem, bądź otrzymaliście ją przez pomyłkę prosimy o powiadomienie o tym nadawcy oraz trwałe jej usunięcie. This email contains information intended solely for the use of the individual to whom it is addressed. If you are not the intended recipient or if you have received this message in error, please notify the sender and delete it from your system.
I'd prefer to use TypeFamilyDependencies right now, and keep using that same flag (not a new one) when we extend what "dependencies" means.
Simon
| -----Original Message-----
| From: Jan Stolarek [mailto:jan.stolarek@p.lodz.pl]
| Sent: 12 January 2016 08:44
| To: Richard Eisenberg
| >> 1. Should this feature be placed behind a LANGUAGE pragma? | > | > No, I don't think it should. I consider it a tiny addition to | > TypeFamilies that is not worth having its separate pragma. Injective | > TFs are fully backwards compatible, so no existing code will be | > broken. | > | That being said, it does claim new syntax and consequently would be | rather difficult to back out if we realize that this implementation | isn't the right direction. I don't have a strong opinion here, just | playing devil's advocate. On a branch we are working on a fundep-like extension of injectivity, which is a rather bigger feature. Personally I think it might be better for there to be a LANGUAGE pragma to signal that we are using it (both the current r -> a form, and the new piece). Simon
participants (5)
-
Andres Löh -
Ben Gamari -
Jan Stolarek -
Richard Eisenberg -
Simon Peyton Jones