Re: Injective type families

> 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

RE: Injective type families

senberg <e...@cis.upenn.edu> | Cc: Simon Peyton Jones <simo...@microsoft.com>; GHC developers | Subject: Re: Injective type families | | > I'm joining this conversation late, but I favor TypeFamilyDependencies over | > InjectiveTypeFamilies. We use the annotations for things other than

RE: Injective type families

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

Re: Injective type families

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

RE: Injective type families

I agree! | -Original Message- | From: Richard Eisenberg [mailto:e...@cis.upenn.edu] | Sent: 11 January 2016 16:35 | To: Jan Stolarek <jan.stola...@p.lodz.pl> | Cc: Simon Peyton Jones <simo...@microsoft.com>; GHC developers | Subject: Re: Injective type families | |

Re: Injective type families

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

Re: Injective type families

Jan Stolarek writes: > 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

Re: Injective type families

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 >

Re: Injective type families

> 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

Re: Injective type families

> 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

RE: Injective type families

| > 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

RE: Injective type families

| >> 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. |

Re: Injective type families

I'm not convinced I have very good taste where it comes to concrete syntax, but I will say that the `injective` keyword below is redundant -- it can be inferred from the presence of the `|`. Also, by restriction (b), I imagine you also allow things like `Maybe a`, where `a` is a variable bound

Re: Injective type families

On Thu, Jul 10, 2014 at 9:37 PM, Jan Stolarek jan.stola...@p.lodz.pl wrote: 1. Standard injective type family (all parameters uniquely determined by the RHS): injective type family F a b c | a b c snip 2. Type family injective only in some parameters (ie. only some parameters uniquely

Re: Injective type families

Jan, this is great! Thanks for attacking this issue. Regarding result, I do not like the idea to introduce arbitrary words with special meanings. What if somebody writes injective type family F a result c | result - a result c it will be totally confusing. One could write like this:

Re: Injective type families

* Kim-Ee Yeoh k...@atamo.com [2014-07-10 23:40:44+0700] On Thu, Jul 10, 2014 at 9:37 PM, Jan Stolarek jan.stola...@p.lodz.pl wrote: 1. Standard injective type family (all parameters uniquely determined by the RHS): injective type family F a b c | a b c snip 2. Type family

Re: Injective type families

On Fri, Jul 11, 2014 at 3:27 AM, Roman Cheplyaka r...@ro-che.info wrote: The result of any function is always determined by that function's parameters. Injectivity means that the *parameters* are determined by the result. So I think Jan's definition is correct. What's correct could still

Re: Injective type families

On 07/10/2014 02:34 PM, Gabor Greif wrote: Jan, this is great! Thanks for attacking this issue. Regarding result, I do not like the idea to introduce arbitrary words with special meanings. What if somebody writes injective type family F a result c | result - a result c it will be