Re: Type Annotations in the Presence of Injective Type Families, Bidirectional Pattern Synonyms, and Data Kinds

Sure, here it is. https://gitlab.haskell.org/ghc/ghc/issues/16614 On Mon, Apr 29, 2019 at 11:46 PM Matthew Pickering < matthewtpicker...@gmail.com> wrote: > Please can you open a bug report anyway? It is easier to discuss it > there than on the mailing list. > > Matt > > On Tue, Apr 30, 2019 at

Re: Type Annotations in the Presence of Injective Type Families, Bidirectional Pattern Synonyms, and Data Kinds

Please can you open a bug report anyway? It is easier to discuss it there than on the mailing list. Matt On Tue, Apr 30, 2019 at 5:25 AM Travis Whitaker wrote: > > Hello GHC Devs, > > I've found a case in which annotating a bidirectional pattern synonym with a > type signature causes the

Type Annotations in the Presence of Injective Type Families, Bidirectional Pattern Synonyms, and Data Kinds

Hello GHC Devs, I've found a case in which annotating a bidirectional pattern synonym with a type signature causes the typechecker to reject an otherwise typeable program. Before filing a bug report I want to check that I'm thinking about this correctly. Consider this module: {-# LANGUAGE

Re: Potentially confusing syntax for injective type families

> I don't have a solution and I hate bike-shedding. I just made this > message to make sure the fact had been considered before release. Yes, I bumped into this issue quite early. After some discussion it was decided that this potential ambiguity is an acceptable trade-off. Janek Dnia

Re: Potentially confusing syntax for injective type families

When this was first discussed a bunch of alternatives were tossed around, mostly involving new keywords, or putting a conditional result keyword in place. Here you can pick the name of the result type, so it doesn't pick any naming conventions for you. My understanding is that the current syntax

Re: Potentially confusing syntax for injective type families

> 2. Without the infectivity annotation, this declares an associate type > synonym default. This isn't valid because Ht is not declared as an > associated type before hand and r is not mentioned on the LHS. > > class Hcl a b where > type Ht a b = r Indeed, this is invalid and GHC rejects this,

Re: Potentially confusing syntax for injective type families

I guess my point is that the most natural parsing of class Hcl a b where type Ht a b = r | r -> a b is (type Ht a b = r) (| r -> a b) rather than (type Ht a b) (= r | r -> a b). A concrete example, in the case of functional dependencies, the vertical bar is used to signal what we expect

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

Injective type families

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

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: [commit: ghc] wip/T10832-generalised-injectivity: Generalized injective type families (332bc0d)

...@git.haskell.org | Sent: 23 December 2015 14:36 | To: ghc-comm...@haskell.org | Subject: [commit: ghc] wip/T10832-generalised-injectivity: Generalized | injective type families (332bc0d) | | Repository : ssh://g...@git.haskell.org/ghc | | On branch : wip/T10832-generalised-injectivity | Link

RE: D202: Injective type families

. Simon From: nore...@phabricator.haskell.org [nore...@phabricator.haskell.org] Sent: 22 October 2014 14:18 To: Simon Peyton Jones Subject: [Differential] [Updated, 486 lines] D202: Injective type families jstolarek updated this revision to Diff 961. jstolarek

Re: D202: Injective type families

I now know how to use 'arc patch' to get a Phab ticket onto my disk. But if I edit the code, can I make a git commit and upload it back to D202? That would be akin to sharing a branch with (in this case Jan) the author. How do I do that? It is often more direct than making comments. Not

RE: D202: Injective type families

they are. So what do I do? Simon | -Original Message- | From: nore...@phabricator.haskell.org | [mailto:nore...@phabricator.haskell.org] | Sent: 18 September 2014 09:35 | To: Simon Peyton Jones | Subject: [Differential] [Commented On] D202: Injective type families | | jstolarek added

Re: D202: Injective type families

: nore...@phabricator.haskell.org | [mailto:nore...@phabricator.haskell.org] | Sent: 18 September 2014 09:35 | To: Simon Peyton Jones | Subject: [Differential] [Commented On] D202: Injective type families | | jstolarek added a comment. | | I made two important adjustments

Injective type families

Hi all, I'd like to take a stab at implementing injective type families (#6018). My plan of attack looks like this: 1. Implement injective type families that are: a) injective in all arguments b) only admit RHS that is a concrete type or a type variable introduced by the LHS

Re: Injective type families

on the LHS. That doesn't seem to be included in a tight reading of your proposal. Thanks for taking this on! Richard On Jul 10, 2014, at 10:37 AM, Jan Stolarek jan.stola...@p.lodz.pl wrote: Hi all, I'd like to take a stab at implementing injective type families (#6018). My plan of attack

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

, I'd like to take a stab at implementing injective type families (#6018). My plan of attack looks like this: 1. Implement injective type families that are: a) injective in all arguments b) only admit RHS that is a concrete type or a type variable introduced by the LHS or a recursive

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