
Hi committee, Csongor Kiss has proposed -XUnsaturatedTypeFamilies. Proposal: https://github.com/kcsongor/ghc-proposals/blob/unsaturated-type-families/pro... ICFP'19 paper: https://www.microsoft.com/en-us/research/uploads/prod/2019/03/unsaturated-ty... Discussion: https://github.com/ghc-proposals/ghc-proposals/pull/242 The central idea is to allow type functions (both type families and type synonyms) to appear unsaturated. (Currently, all type functions are required syntactically to be applied to all parameters they are declared with.) This poses a problem for type inference, as detailed in both the proposal and the paper. The key question: if we have (f a ~ g b), can we conclude (f ~ g) and (a ~ b)? Not if either of f or g is a type function. This proposal thus describes a mechanism to introduce a new flavor of arrow, such that we can identify type functions by their kind. Specifically, we have regular types like Maybe :: Type -> @M Type (where the M stands for "matchable"), but type functions like F :: Type -> @U Type (where the U stands for "unmatchable"). Unmatchable applications can not be decomposed during type inference. Much of the proposal is concerned with backward-compatibility: most users will not want to write @M or @U after each of their arrows, so the proposal describes ways of defaulting this behavior to match (most) programmers' expectations. The proposal also includes matchability polymorphism, the ability to abstract over a matchability parameter. Pros: + This proposal greatly increases the expressiveness of Haskell's type system. + With this proposal, we can finally do proper functional programming in types, rather than just in terms. + This proposal is a key ingredient toward having dependent types, as unsaturated functions are commonplace in terms, and thus should also be supported in types. (Allowing unsaturated functions in types was a key difference between Adam Gundry's proposal for dependent types https://adam.gundry.co.uk/pub/thesis/, which requires a notion of a subset of the type and term languages shared in common, and mine, which makes no distinction between terms and types.) + There is a prototype implementation. + The ideas are backed up by peer-reviewed research. + Despite focusing on type families, this work applies equally to ordinary functions which might be used in types once we have stronger support for dependent types. Cons: - This adds a new dimension of complexity to our kind system, by separating out matchable and unmatchable arrows. - The rules for defaulting appear convenient in practice, but are somewhat arbitrary. - The rules for defaulting care about context -- does an arrow appear in the type of a term or the type of a type? These rules thus go against the spirit of #378, which advocates for not accepting features that distinguish between types and terms. Recommendation: With reservations, I recommend acceptance. I think that the power to use higher-order programming should not be restricted to terms, and allowing unsaturated functions at compile time is necessary in order to have convenient dependent types. However, I am concerned about the extra complexity of matchability. A key open question for me is how much matchability is apparent to users -- even ones using some higher-order type-level programming. If matchability is pervasive, then I would lean against. But my expectation is that matchability fades into the background -- much like levity polymorphism (unless you want it). Open question: What to do about syntax? The proposed syntax is sensible. However, #370 suggests an alternative syntax that might be more forward-thinking. Richard

I often wish I could use unsaturated type families. Where I can see that
going fairly mainstream in the medium term is in the
higher-kinded-data-type sort of idiom. Whereby one parameterises the type
of a record (say) by a family `f :: * -> *` and vary the family to great
effect.
For instance, it would make the types in the multiplate library [
https://hackage.haskell.org/package/multiplate ] quite a bit more palatable.
Like Richard, I want to advance a prudent: yes. As far as alternatives go,
I'm in favour of never inferring matchability polymorphism [ alternative 6,
currently ].
That being said this is a proposal which touches the arrow, which makes it
a fairly large proposal. So it does need more careful eyes to anticipate
issues. The proposal is, in particular, not fully backwards compatible (it
involves promotion of data constructors which take functions as arguments,
it's hard to avoid it). So please, give this one a good reading. Let's make
sure we are happy with it.
On Fri, Nov 20, 2020 at 8:36 PM Richard Eisenberg
Hi committee,
Csongor Kiss has proposed -XUnsaturatedTypeFamilies.
Proposal: https://github.com/kcsongor/ghc-proposals/blob/unsaturated-type-families/pro... ICFP'19 paper: https://www.microsoft.com/en-us/research/uploads/prod/2019/03/unsaturated-ty... Discussion: https://github.com/ghc-proposals/ghc-proposals/pull/242
The central idea is to allow type functions (both type families and type synonyms) to appear unsaturated. (Currently, all type functions are required syntactically to be applied to all parameters they are declared with.) This poses a problem for type inference, as detailed in both the proposal and the paper. The key question: if we have (f a ~ g b), can we conclude (f ~ g) and (a ~ b)? Not if either of f or g is a type function. This proposal thus describes a mechanism to introduce a new flavor of arrow, such that we can identify type functions by their kind. Specifically, we have regular types like Maybe :: Type -> @M Type (where the M stands for "matchable"), but type functions like F :: Type -> @U Type (where the U stands for "unmatchable"). Unmatchable applications can not be decomposed during type inference.
Much of the proposal is concerned with backward-compatibility: most users will not want to write @M or @U after each of their arrows, so the proposal describes ways of defaulting this behavior to match (most) programmers' expectations.
The proposal also includes matchability polymorphism, the ability to abstract over a matchability parameter.
Pros: + This proposal greatly increases the expressiveness of Haskell's type system. + With this proposal, we can finally do proper functional programming in types, rather than just in terms. + This proposal is a key ingredient toward having dependent types, as unsaturated functions are commonplace in terms, and thus should also be supported in types. (Allowing unsaturated functions in types was a key difference between Adam Gundry's proposal for dependent types https://adam.gundry.co.uk/pub/thesis/, which requires a notion of a subset of the type and term languages shared in common, and mine, which makes no distinction between terms and types.) + There is a prototype implementation. + The ideas are backed up by peer-reviewed research. + Despite focusing on type families, this work applies equally to ordinary functions which might be used in types once we have stronger support for dependent types.
Cons: - This adds a new dimension of complexity to our kind system, by separating out matchable and unmatchable arrows. - The rules for defaulting appear convenient in practice, but are somewhat arbitrary. - The rules for defaulting care about context -- does an arrow appear in the type of a term or the type of a type? These rules thus go against the spirit of #378, which advocates for not accepting features that distinguish between types and terms.
Recommendation: With reservations, I recommend acceptance. I think that the power to use higher-order programming should not be restricted to terms, and allowing unsaturated functions at compile time is necessary in order to have convenient dependent types. However, I am concerned about the extra complexity of matchability. A key open question for me is how much matchability is apparent to users -- even ones using some higher-order type-level programming. If matchability is pervasive, then I would lean against. But my expectation is that matchability fades into the background -- much like levity polymorphism (unless you want it).
Open question: What to do about syntax? The proposed syntax is sensible. However, #370 suggests an alternative syntax that might be more forward-thinking.
Richard _______________________________________________ ghc-steering-committee mailing list ghc-steering-committee@haskell.org https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee

Hi everybody,
I really like this proposal. However:
- I think the defaulting rules should be revised. Not only because it may
conflict with #378 (if accepted), but because I think that the rules should
not differentiate between terms and types because getting different
outcomes from term functions and type function / families would be
surprising.
- I think we should wait until we decide about #370 for the syntax.
Regards,
Alejandro
On 20 Nov 2020 at 20:36:12, Richard Eisenberg
Hi committee,
Csongor Kiss has proposed -XUnsaturatedTypeFamilies.
Proposal: https://github.com/kcsongor/ghc-proposals/blob/unsaturated-type-families/pro... ICFP'19 paper: https://www.microsoft.com/en-us/research/uploads/prod/2019/03/unsaturated-ty... Discussion: https://github.com/ghc-proposals/ghc-proposals/pull/242
The central idea is to allow type functions (both type families and type synonyms) to appear unsaturated. (Currently, all type functions are required syntactically to be applied to all parameters they are declared with.) This poses a problem for type inference, as detailed in both the proposal and the paper. The key question: if we have (f a ~ g b), can we conclude (f ~ g) and (a ~ b)? Not if either of f or g is a type function. This proposal thus describes a mechanism to introduce a new flavor of arrow, such that we can identify type functions by their kind. Specifically, we have regular types like Maybe :: Type -> @M Type (where the M stands for "matchable"), but type functions like F :: Type -> @U Type (where the U stands for "unmatchable"). Unmatchable applications can not be decomposed during type inference.
Much of the proposal is concerned with backward-compatibility: most users will not want to write @M or @U after each of their arrows, so the proposal describes ways of defaulting this behavior to match (most) programmers' expectations.
The proposal also includes matchability polymorphism, the ability to abstract over a matchability parameter.
Pros: + This proposal greatly increases the expressiveness of Haskell's type system. + With this proposal, we can finally do proper functional programming in types, rather than just in terms. + This proposal is a key ingredient toward having dependent types, as unsaturated functions are commonplace in terms, and thus should also be supported in types. (Allowing unsaturated functions in types was a key difference between Adam Gundry's proposal for dependent types https://adam.gundry.co.uk/pub/thesis/, which requires a notion of a subset of the type and term languages shared in common, and mine, which makes no distinction between terms and types.) + There is a prototype implementation. + The ideas are backed up by peer-reviewed research. + Despite focusing on type families, this work applies equally to ordinary functions which might be used in types once we have stronger support for dependent types.
Cons: - This adds a new dimension of complexity to our kind system, by separating out matchable and unmatchable arrows. - The rules for defaulting appear convenient in practice, but are somewhat arbitrary. - The rules for defaulting care about context -- does an arrow appear in the type of a term or the type of a type? These rules thus go against the spirit of #378, which advocates for not accepting features that distinguish between types and terms.
Recommendation: With reservations, I recommend acceptance. I think that the power to use higher-order programming should not be restricted to terms, and allowing unsaturated functions at compile time is necessary in order to have convenient dependent types. However, I am concerned about the extra complexity of matchability. A key open question for me is how much matchability is apparent to users -- even ones using some higher-order type-level programming. If matchability is pervasive, then I would lean against. But my expectation is that matchability fades into the background -- much like levity polymorphism (unless you want it).
Open question: What to do about syntax? The proposed syntax is sensible. However, #370 suggests an alternative syntax that might be more forward-thinking.
Richard _______________________________________________ ghc-steering-committee mailing list ghc-steering-committee@haskell.org https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee

I'm on board with unsaturated type families.
Like Linear Haskell, it's quite a "big" proposal, but accepting it is compatible with idea of Haskell as a laboratory for exploration. I think we should flag it as experimental, with the implication that details are liable to change as we gain experience.
Like others, I'd like us to converge on #370 before fixing syntax.
I don’t have a strong opinion about the defaulting stuff.
Declaration of interest: I'm a co-author on the paper.
Simon
| -----Original Message-----
| From: ghc-steering-committee

This thread has seen only positive responses, and with no responses for the past 6 days. I'm thus inclined to accept the proposal. However, there are open questions around the following points: * the concrete syntax (pending discussion on #370) * defaulting rules (as raised by Alejandro in this thread) Conveniently, these are both listed as Unresolved Questions in the proposal itself. We need a way of resolving these questions. The syntax question may become clearer once we know what to do about #370. The defaulting question is harder. I vote to return to this question once #378 has settled somewhat -- but even then, it will be hard. Still, I think we should move forward with accepting the main proposal, and we can continue to debate the defaulting strategy in a further thread, perhaps in parallel with reviewing the (already existing) implementation. I will accept this proposal as written at the end of the week, barring commentary here (or on GitHub) to stop me. Thanks! Richard
On Nov 25, 2020, at 10:28 AM, Simon Peyton Jones
wrote: I'm on board with unsaturated type families.
Like Linear Haskell, it's quite a "big" proposal, but accepting it is compatible with idea of Haskell as a laboratory for exploration. I think we should flag it as experimental, with the implication that details are liable to change as we gain experience.
Like others, I'd like us to converge on #370 before fixing syntax.
I don’t have a strong opinion about the defaulting stuff.
Declaration of interest: I'm a co-author on the paper.
Simon
| -----Original Message----- | From: ghc-steering-committee
On Behalf Of Richard Eisenberg | Sent: 20 November 2020 19:36 | To: Simon Peyton Jones via ghc-steering-committee | Subject: [ghc-steering-committee] Unsaturated type families (#242) | | Hi committee, | | Csongor Kiss has proposed -XUnsaturatedTypeFamilies. | | Proposal: | https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgith | ub.com%2Fkcsongor%2Fghc-proposals%2Fblob%2Funsaturated-type- | families%2Fproposals%2F0000-unsaturated-type- | families.rst&data=04%7C01%7Csimonpj%40microsoft.com%7Cbd9e62e3137e | 40385b5f08d88d8b91e0%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C1%7C6374 | 14978666235646%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2l | uMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C1000&sdata=WdLjCp2ReG9ZXOjmE | Ow6VCJlAO7Yf1aWkVAXHxrsmMM%3D&reserved=0 | ICFP'19 paper: | https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fwww. | microsoft.com%2Fen- | us%2Fresearch%2Fuploads%2Fprod%2F2019%2F03%2Funsaturated-type- | families-icfp- | 2019.pdf&data=04%7C01%7Csimonpj%40microsoft.com%7Cbd9e62e3137e4038 | 5b5f08d88d8b91e0%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C1%7C63741497 | 8666235646%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzI | iLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C1000&sdata=dgowMlsNpH0X9fPAr498F | Y9u8xML9n0G1nwvPN4R9HA%3D&reserved=0 | Discussion: | https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgith | ub.com%2Fghc-proposals%2Fghc- | proposals%2Fpull%2F242&data=04%7C01%7Csimonpj%40microsoft.com%7Cbd | 9e62e3137e40385b5f08d88d8b91e0%7C72f988bf86f141af91ab2d7cd011db47%7C1% | 7C1%7C637414978666235646%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiL | CJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C1000&sdata=C9N0y7l | KhZsepv0mkXbJOMDVLFi4bN5kaVW7DbXW1ro%3D&reserved=0 | | The central idea is to allow type functions (both type families and | type synonyms) to appear unsaturated. (Currently, all type functions | are required syntactically to be applied to all parameters they are | declared with.) This poses a problem for type inference, as detailed | in both the proposal and the paper. The key question: if we have (f a | ~ g b), can we conclude (f ~ g) and (a ~ b)? Not if either of f or g | is a type function. This proposal thus describes a mechanism to | introduce a new flavor of arrow, such that we can identify type | functions by their kind. Specifically, we have regular types like | Maybe :: Type -> @M Type (where the M stands for "matchable"), but | type functions like F :: Type -> @U Type (where the U stands for | "unmatchable"). Unmatchable applications can not be decomposed during | type inference. | | Much of the proposal is concerned with backward-compatibility: most | users will not want to write @M or @U after each of their arrows, so | the proposal describes ways of defaulting this behavior to match | (most) programmers' expectations. | | The proposal also includes matchability polymorphism, the ability to | abstract over a matchability parameter. | | Pros: | + This proposal greatly increases the expressiveness of Haskell's type | system. | + With this proposal, we can finally do proper functional programming | in types, rather than just in terms. | + This proposal is a key ingredient toward having dependent types, as | + unsaturated functions are commonplace in terms, and thus should also | be supported in types. (Allowing unsaturated functions in types was a | key difference between Adam Gundry's proposal for dependent types | https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fadam | .gundry.co.uk%2Fpub%2Fthesis%2F&data=04%7C01%7Csimonpj%40microsoft | .com%7Cbd9e62e3137e40385b5f08d88d8b91e0%7C72f988bf86f141af91ab2d7cd011 | db47%7C1%7C1%7C637414978666235646%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4w | LjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C1000&sdat | a=wk7Xc%2Bb5FLSrndKYZ2ytJh6gO2oYiCXLDhQhdEOfSOg%3D&reserved=0, | which requires a notion of a subset of the type and term languages | shared in common, and mine, which makes no distinction between terms | and types.) There is a prototype implementation. | + The ideas are backed up by peer-reviewed research. | + Despite focusing on type families, this work applies equally to | ordinary functions which might be used in types once we have stronger | support for dependent types. | | Cons: | - This adds a new dimension of complexity to our kind system, by | separating out matchable and unmatchable arrows. | - The rules for defaulting appear convenient in practice, but are | somewhat arbitrary. | - The rules for defaulting care about context -- does an arrow appear | in the type of a term or the type of a type? These rules thus go | against the spirit of #378, which advocates for not accepting features | that distinguish between types and terms. | | Recommendation: With reservations, I recommend acceptance. I think | that the power to use higher-order programming should not be | restricted to terms, and allowing unsaturated functions at compile | time is necessary in order to have convenient dependent types. | However, I am concerned about the extra complexity of matchability. A | key open question for me is how much matchability is apparent to users | -- even ones using some higher-order type-level programming. If | matchability is pervasive, then I would lean against. But my | expectation is that matchability fades into the background -- much | like levity polymorphism (unless you want it). | | Open question: What to do about syntax? The proposed syntax is | sensible. However, #370 suggests an alternative syntax that might be | more forward-thinking. | | Richard | _______________________________________________ | ghc-steering-committee mailing list | ghc-steering-committee@haskell.org | https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fmail | .haskell.org%2Fcgi-bin%2Fmailman%2Flistinfo%2Fghc-steering- | committee&data=04%7C01%7Csimonpj%40microsoft.com%7Cbd9e62e3137e403 | 85b5f08d88d8b91e0%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C1%7C6374149 | 78666235646%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMz | IiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C1000&sdata=cIlDCT4r8C8Yc0%2BOib | Q%2F6Dv1qzBiB1PpavCdAJI3ruw%3D&reserved=0

Dear all,
I'm a bit worried by the limited response from the committee on this
proposal. It is a non-trivial proposal, and I think it deserves more eyes.
So please have a look at them so that we can commit to this with confidence.
/Arnaud
On Tue, Dec 1, 2020 at 7:28 PM Richard Eisenberg
This thread has seen only positive responses, and with no responses for the past 6 days. I'm thus inclined to accept the proposal.
However, there are open questions around the following points: * the concrete syntax (pending discussion on #370) * defaulting rules (as raised by Alejandro in this thread)
Conveniently, these are both listed as Unresolved Questions in the proposal itself. We need a way of resolving these questions. The syntax question may become clearer once we know what to do about #370. The defaulting question is harder. I vote to return to this question once #378 has settled somewhat -- but even then, it will be hard. Still, I think we should move forward with accepting the main proposal, and we can continue to debate the defaulting strategy in a further thread, perhaps in parallel with reviewing the (already existing) implementation.
I will accept this proposal as written at the end of the week, barring commentary here (or on GitHub) to stop me.
Thanks! Richard
On Nov 25, 2020, at 10:28 AM, Simon Peyton Jones
wrote: I'm on board with unsaturated type families.
Like Linear Haskell, it's quite a "big" proposal, but accepting it is compatible with idea of Haskell as a laboratory for exploration. I think we should flag it as experimental, with the implication that details are liable to change as we gain experience.
Like others, I'd like us to converge on #370 before fixing syntax.
I don’t have a strong opinion about the defaulting stuff.
Declaration of interest: I'm a co-author on the paper.
Simon
| -----Original Message----- | From: ghc-steering-committee
On Behalf Of Richard Eisenberg | Sent: 20 November 2020 19:36 | To: Simon Peyton Jones via ghc-steering-committee | Subject: [ghc-steering-committee] Unsaturated type families (#242) | | Hi committee, | | Csongor Kiss has proposed -XUnsaturatedTypeFamilies. | | Proposal: | https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgith | ub.com%2Fkcsongor%2Fghc-proposals%2Fblob%2Funsaturated-type- | families%2Fproposals%2F0000-unsaturated-type- | families.rst&data=04%7C01%7Csimonpj%40microsoft.com %7Cbd9e62e3137e | 40385b5f08d88d8b91e0%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C1%7C6374 | 14978666235646%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2l | uMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C1000&sdata=WdLjCp2ReG9ZXOjmE | Ow6VCJlAO7Yf1aWkVAXHxrsmMM%3D&reserved=0 | ICFP'19 paper: | https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fwww . | microsoft.com%2Fen- | us%2Fresearch%2Fuploads%2Fprod%2F2019%2F03%2Funsaturated-type- | families-icfp- | 2019.pdf&data=04%7C01%7Csimonpj%40microsoft.com %7Cbd9e62e3137e4038 | 5b5f08d88d8b91e0%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C1%7C63741497 | 8666235646%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzI | iLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C1000&sdata=dgowMlsNpH0X9fPAr498F | Y9u8xML9n0G1nwvPN4R9HA%3D&reserved=0 | Discussion: | https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgith | ub.com%2Fghc-proposals%2Fghc- | proposals%2Fpull%2F242&data=04%7C01%7Csimonpj%40microsoft.com %7Cbd | 9e62e3137e40385b5f08d88d8b91e0%7C72f988bf86f141af91ab2d7cd011db47%7C1% | 7C1%7C637414978666235646%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiL | CJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C1000&sdata=C9N0y7l | KhZsepv0mkXbJOMDVLFi4bN5kaVW7DbXW1ro%3D&reserved=0 | | The central idea is to allow type functions (both type families and | type synonyms) to appear unsaturated. (Currently, all type functions | are required syntactically to be applied to all parameters they are | declared with.) This poses a problem for type inference, as detailed | in both the proposal and the paper. The key question: if we have (f a | ~ g b), can we conclude (f ~ g) and (a ~ b)? Not if either of f or g | is a type function. This proposal thus describes a mechanism to | introduce a new flavor of arrow, such that we can identify type | functions by their kind. Specifically, we have regular types like | Maybe :: Type -> @M Type (where the M stands for "matchable"), but | type functions like F :: Type -> @U Type (where the U stands for | "unmatchable"). Unmatchable applications can not be decomposed during | type inference. | | Much of the proposal is concerned with backward-compatibility: most | users will not want to write @M or @U after each of their arrows, so | the proposal describes ways of defaulting this behavior to match | (most) programmers' expectations. | | The proposal also includes matchability polymorphism, the ability to | abstract over a matchability parameter. | | Pros: | + This proposal greatly increases the expressiveness of Haskell's type | system. | + With this proposal, we can finally do proper functional programming | in types, rather than just in terms. | + This proposal is a key ingredient toward having dependent types, as | + unsaturated functions are commonplace in terms, and thus should also | be supported in types. (Allowing unsaturated functions in types was a | key difference between Adam Gundry's proposal for dependent types | https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fadam | .gundry.co.uk %2Fpub%2Fthesis%2F&data=04%7C01%7Csimonpj%40microsoft | .com%7Cbd9e62e3137e40385b5f08d88d8b91e0%7C72f988bf86f141af91ab2d7cd011 | db47%7C1%7C1%7C637414978666235646%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4w | LjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C1000&sdat | a=wk7Xc%2Bb5FLSrndKYZ2ytJh6gO2oYiCXLDhQhdEOfSOg%3D&reserved=0, | which requires a notion of a subset of the type and term languages | shared in common, and mine, which makes no distinction between terms | and types.) There is a prototype implementation. | + The ideas are backed up by peer-reviewed research. | + Despite focusing on type families, this work applies equally to | ordinary functions which might be used in types once we have stronger | support for dependent types. | | Cons: | - This adds a new dimension of complexity to our kind system, by | separating out matchable and unmatchable arrows. | - The rules for defaulting appear convenient in practice, but are | somewhat arbitrary. | - The rules for defaulting care about context -- does an arrow appear | in the type of a term or the type of a type? These rules thus go | against the spirit of #378, which advocates for not accepting features | that distinguish between types and terms. | | Recommendation: With reservations, I recommend acceptance. I think | that the power to use higher-order programming should not be | restricted to terms, and allowing unsaturated functions at compile | time is necessary in order to have convenient dependent types. | However, I am concerned about the extra complexity of matchability. A | key open question for me is how much matchability is apparent to users | -- even ones using some higher-order type-level programming. If | matchability is pervasive, then I would lean against. But my | expectation is that matchability fades into the background -- much | like levity polymorphism (unless you want it). | | Open question: What to do about syntax? The proposed syntax is | sensible. However, #370 suggests an alternative syntax that might be | more forward-thinking. | | Richard | _______________________________________________ | ghc-steering-committee mailing list | ghc-steering-committee@haskell.org | https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fmail | .haskell.org%2Fcgi-bin%2Fmailman%2Flistinfo%2Fghc-steering- | committee&data=04%7C01%7Csimonpj%40microsoft.com %7Cbd9e62e3137e403 | 85b5f08d88d8b91e0%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C1%7C6374149 | 78666235646%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMz | IiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C1000&sdata=cIlDCT4r8C8Yc0%2BOib | Q%2F6Dv1qzBiB1PpavCdAJI3ruw%3D&reserved=0 _______________________________________________ ghc-steering-committee mailing list ghc-steering-committee@haskell.org https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee

I felt rather too biased to comment on this proposal, as I have been very publicly vocal about how excited I am to see it in GHC. However, it occurs to me that my thoughts on the proposal are rather too scattered across the Internet, so I’ll try to collate the main points that I have. I will caveat these by saying that they have mostly been addressed in the thread and/or the proposal, and they certainly don’t change my opinion that the proposal be accepted.
* A pretty significant consequence of this proposal is partial application of type synonyms. I think the inability to partially apply these is a rather counter-intuitive restriction to beginners (particularly when they’ve just started to get familiar with partial application at the value level). Certainly, when introducing colleagues to Haskell, it is a question that comes up reasonably often: “why must I write type T = Maybe and never type T x = Maybe x?” Of course, once one considers the importance of `f a ~ g b <=> (f ~ g, a ~ b)` for inference, and an example like type T x = Either x Int, this starts to make more sense, but we’ve had to reach a surprisingly deep level of understanding to figure this out.
Naturally, lifting that restriction is going to mean one less thing to explain ("type-level works like term-level!”) but I worry about the potential error messages here. If a user is at a point where they feel comfortable playing with type families, I think they’re perhaps more primed for strange error messages, but can I ever run into a matchability mismatch error as an absolute beginner? The classic example (that Joachim already raised) is trying to write a functor instance for type Id x = x. If I’m new to the language, it’s potentially not clear to me why I can’t do this (at least until the rest of Csongor’s research finds its way into the compiler). In which case, I’d like to see a more specialised error such as, “You can’t write a class instance for a partially-applied type synonym”, rather than exposing someone to 'M and 'U in their first week of Haskell.
* Now we have unmatchable (not generative, not injective) and matchable (generative, injective), it feels incomplete not to have annotations for generative-but-not-injective and injective-but-not-generative arrows. While generativity annotation (and checking!) is effectively an entirely new chunk of work, it’s a shame that we have the syntax to specify the injectivity of a type family when we create it, but not when we consume it. I have some concrete examples of where having to declare injective type families as fully unmatchable leads to ambiguity that I can share if anyone is interested, but my understanding from Csongor is that this is a deceptively large amount of work, and definitely out of scope for this particular proposal.
Looking down my list, these are the two thoughts I have that haven’t been explicitly covered in full somewhere in the GitHub thread, and I feel they could be summarised as an implementation suggestion and a feature request. All of which is to say, I’m still very much in support of the proposal, and extremely excited to start using it.
Thanks,
Tom
On 2 Dec 2020, at 15:30, Spiwack, Arnaud
On Nov 25, 2020, at 10:28 AM, Simon Peyton Jones
mailto:simonpj@microsoft.com> wrote: I'm on board with unsaturated type families.
Like Linear Haskell, it's quite a "big" proposal, but accepting it is compatible with idea of Haskell as a laboratory for exploration. I think we should flag it as experimental, with the implication that details are liable to change as we gain experience.
Like others, I'd like us to converge on #370 before fixing syntax.
I don’t have a strong opinion about the defaulting stuff.
Declaration of interest: I'm a co-author on the paper.
Simon
| -----Original Message----- | From: ghc-steering-committee
mailto:bounces@haskell.org> On Behalf Of Richard Eisenberg | Sent: 20 November 2020 19:36 | To: Simon Peyton Jones via ghc-steering-committee mailto:committee@haskell.org> | Subject: [ghc-steering-committee] Unsaturated type families (#242) | | Hi committee, | | Csongor Kiss has proposed -XUnsaturatedTypeFamilies. | | Proposal: | https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgith | ub.comhttp://ub.com/%2Fkcsongor%2Fghc-proposals%2Fblob%2Funsaturated-type- | families%2Fproposals%2F0000-unsaturated-type- | families.rst&data=04%7C01%7Csimonpj%40microsoft.comhttp://40microsoft.com/%7Cbd9e62e3137e | 40385b5f08d88d8b91e0%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C1%7C6374 | 14978666235646%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2l | uMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C1000&sdata=WdLjCp2ReG9ZXOjmE | Ow6VCJlAO7Yf1aWkVAXHxrsmMM%3D&reserved=0 | ICFP'19 paper: | https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fwww. | microsoft.comhttp://microsoft.com/%2Fen- | us%2Fresearch%2Fuploads%2Fprod%2F2019%2F03%2Funsaturated-type- | families-icfp- | 2019.pdf&data=04%7C01%7Csimonpj%40microsoft.comhttp://40microsoft.com/%7Cbd9e62e3137e4038 | 5b5f08d88d8b91e0%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C1%7C63741497 | 8666235646%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzI | iLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C1000&sdata=dgowMlsNpH0X9fPAr498F | Y9u8xML9n0G1nwvPN4R9HA%3D&reserved=0 | Discussion: | https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgith | ub.comhttp://ub.com/%2Fghc-proposals%2Fghc- | proposals%2Fpull%2F242&data=04%7C01%7Csimonpj%40microsoft.comhttp://40microsoft.com/%7Cbd | 9e62e3137e40385b5f08d88d8b91e0%7C72f988bf86f141af91ab2d7cd011db47%7C1% | 7C1%7C637414978666235646%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiL | CJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C1000&sdata=C9N0y7l | KhZsepv0mkXbJOMDVLFi4bN5kaVW7DbXW1ro%3D&reserved=0 | | The central idea is to allow type functions (both type families and | type synonyms) to appear unsaturated. (Currently, all type functions | are required syntactically to be applied to all parameters they are | declared with.) This poses a problem for type inference, as detailed | in both the proposal and the paper. The key question: if we have (f a | ~ g b), can we conclude (f ~ g) and (a ~ b)? Not if either of f or g | is a type function. This proposal thus describes a mechanism to | introduce a new flavor of arrow, such that we can identify type | functions by their kind. Specifically, we have regular types like | Maybe :: Type -> @M Type (where the M stands for "matchable"), but | type functions like F :: Type -> @U Type (where the U stands for | "unmatchable"). Unmatchable applications can not be decomposed during | type inference. | | Much of the proposal is concerned with backward-compatibility: most | users will not want to write @M or @U after each of their arrows, so | the proposal describes ways of defaulting this behavior to match | (most) programmers' expectations. | | The proposal also includes matchability polymorphism, the ability to | abstract over a matchability parameter. | | Pros: | + This proposal greatly increases the expressiveness of Haskell's type | system. | + With this proposal, we can finally do proper functional programming | in types, rather than just in terms. | + This proposal is a key ingredient toward having dependent types, as | + unsaturated functions are commonplace in terms, and thus should also | be supported in types. (Allowing unsaturated functions in types was a | key difference between Adam Gundry's proposal for dependent types | https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fadam | .gundry.co.ukhttp://gundry.co.uk/%2Fpub%2Fthesis%2F&data=04%7C01%7Csimonpj%40microsoft | .com%7Cbd9e62e3137e40385b5f08d88d8b91e0%7C72f988bf86f141af91ab2d7cd011 | db47%7C1%7C1%7C637414978666235646%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4w | LjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C1000&sdat | a=wk7Xc%2Bb5FLSrndKYZ2ytJh6gO2oYiCXLDhQhdEOfSOg%3D&reserved=0, | which requires a notion of a subset of the type and term languages | shared in common, and mine, which makes no distinction between terms | and types.) There is a prototype implementation. | + The ideas are backed up by peer-reviewed research. | + Despite focusing on type families, this work applies equally to | ordinary functions which might be used in types once we have stronger | support for dependent types. | | Cons: | - This adds a new dimension of complexity to our kind system, by | separating out matchable and unmatchable arrows. | - The rules for defaulting appear convenient in practice, but are | somewhat arbitrary. | - The rules for defaulting care about context -- does an arrow appear | in the type of a term or the type of a type? These rules thus go | against the spirit of #378, which advocates for not accepting features | that distinguish between types and terms. | | Recommendation: With reservations, I recommend acceptance. I think | that the power to use higher-order programming should not be | restricted to terms, and allowing unsaturated functions at compile | time is necessary in order to have convenient dependent types. | However, I am concerned about the extra complexity of matchability. A | key open question for me is how much matchability is apparent to users | -- even ones using some higher-order type-level programming. If | matchability is pervasive, then I would lean against. But my | expectation is that matchability fades into the background -- much | like levity polymorphism (unless you want it). | | Open question: What to do about syntax? The proposed syntax is | sensible. However, #370 suggests an alternative syntax that might be | more forward-thinking. | | Richard | _______________________________________________ | ghc-steering-committee mailing list | ghc-steering-committee@haskell.orgmailto:ghc-steering-committee@haskell.org | https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fmail | .haskell.orghttp://haskell.org/%2Fcgi-bin%2Fmailman%2Flistinfo%2Fghc-steering- | committee&data=04%7C01%7Csimonpj%40microsoft.comhttp://40microsoft.com/%7Cbd9e62e3137e403 | 85b5f08d88d8b91e0%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C1%7C6374149 | 78666235646%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMz | IiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C1000&sdata=cIlDCT4r8C8Yc0%2BOib | Q%2F6Dv1qzBiB1PpavCdAJI3ruw%3D&reserved=0
_______________________________________________ ghc-steering-committee mailing list ghc-steering-committee@haskell.orgmailto:ghc-steering-committee@haskell.org https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee _______________________________________________ ghc-steering-committee mailing list ghc-steering-committee@haskell.orgmailto:ghc-steering-committee@haskell.org https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee

Hi, Am Mittwoch, den 02.12.2020, 16:30 +0100 schrieb Spiwack, Arnaud:
I'm a bit worried by the limited response from the committee on this proposal. It is a non-trivial proposal, and I think it deserves more eyes. So please have a look at them so that we can commit to this with confidence.
it is above my head to commit with confidence. Yes, I want them! Do I want the matchability kind (and not subtyping)? Do I want matchability-polymorphism? Are these the right defaults? I don't know! So if the expects say “that's the best we can do”, then all for it. If the experts say “this there are other corner in the design space”, and maybe some are simpler/more elegant/what not? Then I can comment. BTW, https://github.com/ghc-proposals/ghc-proposals/pull/242#issuecomment-7367388... is unanswerd yet. Cheers, Joachim -- Joachim Breitner mail@joachim-breitner.de http://www.joachim-breitner.de/

Apologies for being slow, I've left a number of questions on GitHub, mostly asking for clarification on various points. I'm also generally in favor of this proposal, though like others I have concerns around the defaulting strategies. Mine are mostly around the large number of rules that I'll have to keep in my head if I need to start caring about matchabilites. But I'd be happy with some sort of provisional acceptance, subject to resolving the syntax and defaulting rules later. On Wed, Dec 2, 2020, at 10:30, Spiwack, Arnaud wrote:
Dear all,
I'm a bit worried by the limited response from the committee on this proposal. It is a non-trivial proposal, and I think it deserves more eyes. So please have a look at them so that we can commit to this with confidence.
/Arnaud
On Tue, Dec 1, 2020 at 7:28 PM Richard Eisenberg
wrote: This thread has seen only positive responses, and with no responses for the past 6 days. I'm thus inclined to accept the proposal.
However, there are open questions around the following points: * the concrete syntax (pending discussion on #370) * defaulting rules (as raised by Alejandro in this thread)
Conveniently, these are both listed as Unresolved Questions in the proposal itself. We need a way of resolving these questions. The syntax question may become clearer once we know what to do about #370. The defaulting question is harder. I vote to return to this question once #378 has settled somewhat -- but even then, it will be hard. Still, I think we should move forward with accepting the main proposal, and we can continue to debate the defaulting strategy in a further thread, perhaps in parallel with reviewing the (already existing) implementation.
I will accept this proposal as written at the end of the week, barring commentary here (or on GitHub) to stop me.
Thanks! Richard
On Nov 25, 2020, at 10:28 AM, Simon Peyton Jones
wrote: I'm on board with unsaturated type families.
Like Linear Haskell, it's quite a "big" proposal, but accepting it is compatible with idea of Haskell as a laboratory for exploration. I think we should flag it as experimental, with the implication that details are liable to change as we gain experience.
Like others, I'd like us to converge on #370 before fixing syntax.
I don’t have a strong opinion about the defaulting stuff.
Declaration of interest: I'm a co-author on the paper.
Simon
| -----Original Message----- | From: ghc-steering-committee
On Behalf Of Richard Eisenberg | Sent: 20 November 2020 19:36 | To: Simon Peyton Jones via ghc-steering-committee | Subject: [ghc-steering-committee] Unsaturated type families (#242) | | Hi committee, | | Csongor Kiss has proposed -XUnsaturatedTypeFamilies. | | Proposal: | https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgith | ub.com%2Fkcsongor%2Fghc-proposals%2Fblob%2Funsaturated-type- | families%2Fproposals%2F0000-unsaturated-type- | families.rst&data=04%7C01%7Csimonpj%40microsoft.com%7Cbd9e62e3137e | 40385b5f08d88d8b91e0%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C1%7C6374 | 14978666235646%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2l | uMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C1000&sdata=WdLjCp2ReG9ZXOjmE | Ow6VCJlAO7Yf1aWkVAXHxrsmMM%3D&reserved=0 | ICFP'19 paper: | https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fwww. | microsoft.com%2Fen- | us%2Fresearch%2Fuploads%2Fprod%2F2019%2F03%2Funsaturated-type- | families-icfp- | 2019.pdf&data=04%7C01%7Csimonpj%40microsoft.com%7Cbd9e62e3137e4038 | 5b5f08d88d8b91e0%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C1%7C63741497 | 8666235646%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzI | iLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C1000&sdata=dgowMlsNpH0X9fPAr498F | Y9u8xML9n0G1nwvPN4R9HA%3D&reserved=0 | Discussion: | https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgith | ub.com%2Fghc-proposals%2Fghc- | proposals%2Fpull%2F242&data=04%7C01%7Csimonpj%40microsoft.com%7Cbd | 9e62e3137e40385b5f08d88d8b91e0%7C72f988bf86f141af91ab2d7cd011db47%7C1% | 7C1%7C637414978666235646%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiL | CJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C1000&sdata=C9N0y7l | KhZsepv0mkXbJOMDVLFi4bN5kaVW7DbXW1ro%3D&reserved=0 | | The central idea is to allow type functions (both type families and | type synonyms) to appear unsaturated. (Currently, all type functions | are required syntactically to be applied to all parameters they are | declared with.) This poses a problem for type inference, as detailed | in both the proposal and the paper. The key question: if we have (f a | ~ g b), can we conclude (f ~ g) and (a ~ b)? Not if either of f or g | is a type function. This proposal thus describes a mechanism to | introduce a new flavor of arrow, such that we can identify type | functions by their kind. Specifically, we have regular types like | Maybe :: Type -> @M Type (where the M stands for "matchable"), but | type functions like F :: Type -> @U Type (where the U stands for | "unmatchable"). Unmatchable applications can not be decomposed during | type inference. | | Much of the proposal is concerned with backward-compatibility: most | users will not want to write @M or @U after each of their arrows, so | the proposal describes ways of defaulting this behavior to match | (most) programmers' expectations. | | The proposal also includes matchability polymorphism, the ability to | abstract over a matchability parameter. | | Pros: | + This proposal greatly increases the expressiveness of Haskell's type | system. | + With this proposal, we can finally do proper functional programming | in types, rather than just in terms. | + This proposal is a key ingredient toward having dependent types, as | + unsaturated functions are commonplace in terms, and thus should also | be supported in types. (Allowing unsaturated functions in types was a | key difference between Adam Gundry's proposal for dependent types | https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fadam | .gundry.co.uk%2Fpub%2Fthesis%2F&data=04%7C01%7Csimonpj%40microsoft | .com%7Cbd9e62e3137e40385b5f08d88d8b91e0%7C72f988bf86f141af91ab2d7cd011 | db47%7C1%7C1%7C637414978666235646%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4w | LjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C1000&sdat | a=wk7Xc%2Bb5FLSrndKYZ2ytJh6gO2oYiCXLDhQhdEOfSOg%3D&reserved=0, | which requires a notion of a subset of the type and term languages | shared in common, and mine, which makes no distinction between terms | and types.) There is a prototype implementation. | + The ideas are backed up by peer-reviewed research. | + Despite focusing on type families, this work applies equally to | ordinary functions which might be used in types once we have stronger | support for dependent types. | | Cons: | - This adds a new dimension of complexity to our kind system, by | separating out matchable and unmatchable arrows. | - The rules for defaulting appear convenient in practice, but are | somewhat arbitrary. | - The rules for defaulting care about context -- does an arrow appear | in the type of a term or the type of a type? These rules thus go | against the spirit of #378, which advocates for not accepting features | that distinguish between types and terms. | | Recommendation: With reservations, I recommend acceptance. I think | that the power to use higher-order programming should not be | restricted to terms, and allowing unsaturated functions at compile | time is necessary in order to have convenient dependent types. | However, I am concerned about the extra complexity of matchability. A | key open question for me is how much matchability is apparent to users | -- even ones using some higher-order type-level programming. If | matchability is pervasive, then I would lean against. But my | expectation is that matchability fades into the background -- much | like levity polymorphism (unless you want it). | | Open question: What to do about syntax? The proposed syntax is | sensible. However, #370 suggests an alternative syntax that might be | more forward-thinking. | | Richard | _______________________________________________ | ghc-steering-committee mailing list | ghc-steering-committee@haskell.org | https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fmail | .haskell.org%2Fcgi-bin%2Fmailman%2Flistinfo%2Fghc-steering- | committee&data=04%7C01%7Csimonpj%40microsoft.com%7Cbd9e62e3137e403 | 85b5f08d88d8b91e0%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C1%7C6374149 | 78666235646%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMz | IiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C1000&sdata=cIlDCT4r8C8Yc0%2BOib | Q%2F6Dv1qzBiB1PpavCdAJI3ruw%3D&reserved=0 _______________________________________________ ghc-steering-committee mailing list ghc-steering-committee@haskell.org https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee
ghc-steering-committee mailing list ghc-steering-committee@haskell.org https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee

I have written a comment on the GitHub thread
https://github.com/ghc-proposals/ghc-proposals/pull/242#issuecomment-7375519...
I argue for acceptance, but I suggest that we might want to start distinguishing "experimental proposals" from normal proposals.
Simon
| -----Original Message-----
| From: ghc-steering-committee

The proposal has been accepted on an experimental basis. I added the following text to the proposal itself during acceptance: Committee Decision ------------------ The committee has accepted this proposal on an *experimental* basis. This feature is wholly new to Haskell (and to programming, more generally), and we will learn more from experience. But we cannot gain the experience without incorporating and releasing the feature. We thus label it as subject to change. Changes will be incorporated into this document before they are released. In particular, the following aspects are subject to change: * Syntax (especially in light of `Proposal #370 https://github.com/ghc-proposals/ghc-proposals/pull/370`_). * The defaulting rules. These changes might continue (without prior debate here) even after a release, but all changes will be made in consultation with the GHC developer team, via debate at `GitLab https://gitlab.haskell.org/ghc/ghc/`_. Thanks, all! Richard
On Dec 3, 2020, at 3:27 AM, Simon Peyton Jones via ghc-steering-committee
wrote: I have written a comment on the GitHub thread https://github.com/ghc-proposals/ghc-proposals/pull/242#issuecomment-7375519...
I argue for acceptance, but I suggest that we might want to start distinguishing "experimental proposals" from normal proposals.
Simon
| -----Original Message----- | From: ghc-steering-committee
On Behalf Of Eric Seidel | Sent: 03 December 2020 02:30 | To: ghc-steering-committee@haskell.org | Subject: Re: [ghc-steering-committee] Unsaturated type families (#242) | | Apologies for being slow, I've left a number of questions on GitHub, | mostly asking for clarification on various points. | | I'm also generally in favor of this proposal, though like others I | have concerns around the defaulting strategies. Mine are mostly around | the large number of rules that I'll have to keep in my head if I need | to start caring about matchabilites. But I'd be happy with some sort | of provisional acceptance, subject to resolving the syntax and | defaulting rules later. | | On Wed, Dec 2, 2020, at 10:30, Spiwack, Arnaud wrote: | > Dear all, | > | > I'm a bit worried by the limited response from the committee on this | > proposal. It is a non-trivial proposal, and I think it deserves more | > eyes. So please have a look at them so that we can commit to this | with | > confidence. | > | > /Arnaud | > | > On Tue, Dec 1, 2020 at 7:28 PM Richard Eisenberg | wrote: | > > This thread has seen only positive responses, and with no | responses for the past 6 days. I'm thus inclined to accept the | proposal. | > > | > > However, there are open questions around the following points: | > > * the concrete syntax (pending discussion on #370) | > > * defaulting rules (as raised by Alejandro in this thread) | > > | > > Conveniently, these are both listed as Unresolved Questions in the | proposal itself. We need a way of resolving these questions. The | syntax question may become clearer once we know what to do about #370. | The defaulting question is harder. I vote to return to this question | once #378 has settled somewhat -- but even then, it will be hard. | Still, I think we should move forward with accepting the main | proposal, and we can continue to debate the defaulting strategy in a | further thread, perhaps in parallel with reviewing the (already | existing) implementation. | > > | > > I will accept this proposal as written at the end of the week, | barring commentary here (or on GitHub) to stop me. | > > | > > Thanks! | > > Richard | > > | > > > On Nov 25, 2020, at 10:28 AM, Simon Peyton Jones | wrote: | > > > | > > > I'm on board with unsaturated type families. | > > > | > > > Like Linear Haskell, it's quite a "big" proposal, but accepting | it is compatible with idea of Haskell as a laboratory for exploration. | I think we should flag it as experimental, with the implication that | details are liable to change as we gain experience. | > > > | > > > Like others, I'd like us to converge on #370 before fixing | syntax. | > > > | > > > I don’t have a strong opinion about the defaulting stuff. | > > > | > > > Declaration of interest: I'm a co-author on the paper. | > > > | > > > Simon | > > > | > > > | -----Original Message----- | > > > | From: ghc-steering-committee > > | bounces@haskell.org> On Behalf Of Richard Eisenberg | > > > | Sent: 20 November 2020 19:36 | > > > | To: Simon Peyton Jones via ghc-steering-committee | > > > | | > > > | Subject: [ghc-steering-committee] Unsaturated type families | > > > | (#242) | > > > | | > > > | Hi committee, | > > > | | > > > | Csongor Kiss has proposed -XUnsaturatedTypeFamilies. | > > > | | > > > | Proposal: | > > > | | > > > | | https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F% | > > > | 2Fgith | > > > | ub.com%2Fkcsongor%2Fghc-proposals%2Fblob%2Funsaturated-type- | > > > | families%2Fproposals%2F0000-unsaturated-type- | > > > | | > > > | | families.rst&data=04%7C01%7Csimonpj%40microsoft.com%7Cbd9e62 | > > > | e3137e | > > > | | > > > | | 40385b5f08d88d8b91e0%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C1% | > > > | 7C6374 | > > > | | 14978666235646%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQI | > > > | joiV2l | > > > | | uMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C1000&sdata=WdLjCp2ReG9 | > > > | ZXOjmE | > > > | Ow6VCJlAO7Yf1aWkVAXHxrsmMM%3D&reserved=0 | > > > | ICFP'19 paper: | > > > | | https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fwww. | > > > | microsoft.com%2Fen- | > > > | us%2Fresearch%2Fuploads%2Fprod%2F2019%2F03%2Funsaturated- | type- | > > > | families-icfp- | > > > | | > > > | | 2019.pdf&data=04%7C01%7Csimonpj%40microsoft.com%7Cbd9e62e313 | > > > | 7e4038 | > > > | | > > > | | 5b5f08d88d8b91e0%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C1%7C63 | > > > | 741497 | > > > | | 8666235646%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV | > > > | 2luMzI | > > > | | iLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C1000&sdata=dgowMlsNpH0X9fP | > > > | Ar498F | > > > | Y9u8xML9n0G1nwvPN4R9HA%3D&reserved=0 | > > > | Discussion: | > > > | | > > > | | https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F% | > > > | 2Fgith | > > > | ub.com%2Fghc-proposals%2Fghc- | > > > | | > > > | | proposals%2Fpull%2F242&data=04%7C01%7Csimonpj%40microsoft.co | > > > | m%7Cbd | > > > | | 9e62e3137e40385b5f08d88d8b91e0%7C72f988bf86f141af91ab2d7cd011db4 | > > > | 7%7C1% | > > > | | 7C1%7C637414978666235646%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjA | > > > | wMDAiL | > > > | | CJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C1000&sdata=C | > > > | 9N0y7l | > > > | KhZsepv0mkXbJOMDVLFi4bN5kaVW7DbXW1ro%3D&reserved=0 | > > > | | > > > | The central idea is to allow type functions (both type | families | > > > | and type synonyms) to appear unsaturated. (Currently, all | type | > > > | functions are required syntactically to be applied to all | > > > | parameters they are declared with.) This poses a problem for | > > > | type inference, as detailed in both the proposal and the | paper. | > > > | The key question: if we have (f a ~ g b), can we conclude (f | ~ | > > > | g) and (a ~ b)? Not if either of f or g is a type function. | > > > | This proposal thus describes a mechanism to introduce a new | > > > | flavor of arrow, such that we can identify type functions by | > > > | their kind. Specifically, we have regular types like Maybe :: | > > > | Type -> @M Type (where the M stands for "matchable"), but | type | > > > | functions like F :: Type -> @U Type (where the U stands for | > > > | "unmatchable"). Unmatchable applications can not be decomposed | during type inference. | > > > | | > > > | Much of the proposal is concerned with backward- | compatibility: | > > > | most users will not want to write @M or @U after each of | their | > > > | arrows, so the proposal describes ways of defaulting this | > > > | behavior to match | > > > | (most) programmers' expectations. | > > > | | > > > | The proposal also includes matchability polymorphism, the | > > > | ability to abstract over a matchability parameter. | > > > | | > > > | Pros: | > > > | + This proposal greatly increases the expressiveness of | > > > | Haskell's type system. | > > > | + With this proposal, we can finally do proper functional | > > > | programming in types, rather than just in terms. | > > > | + This proposal is a key ingredient toward having dependent | > > > | types, as + unsaturated functions are commonplace in terms, | and | > > > | thus should also be supported in types. (Allowing unsaturated | > > > | functions in types was a key difference between Adam Gundry's | > > > | proposal for dependent types | > > > | | https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F% | > > > | 2Fadam | > > > | | .gundry.co.uk%2Fpub%2Fthesis%2F&data=04%7C01%7Csimonpj%40mic | > > > | rosoft | > > > | | > > > | | .com%7Cbd9e62e3137e40385b5f08d88d8b91e0%7C72f988bf86f141af91ab2d | > > > | 7cd011 | > > > | | db47%7C1%7C1%7C637414978666235646%7CUnknown%7CTWFpbGZsb3d8eyJWIj | > > > | oiMC4w | > > > | | LjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C1000&am | > > > | p;sdat | > > > | | a=wk7Xc%2Bb5FLSrndKYZ2ytJh6gO2oYiCXLDhQhdEOfSOg%3D&reserved= | > > > | 0, which requires a notion of a subset of the type and term | > > > | languages shared in common, and mine, which makes no | > > > | distinction between terms and types.) There is a prototype | > > > | implementation. | > > > | + The ideas are backed up by peer-reviewed research. | > > > | + Despite focusing on type families, this work applies | equally | > > > | to ordinary functions which might be used in types once we | have | > > > | stronger support for dependent types. | > > > | | > > > | Cons: | > > > | - This adds a new dimension of complexity to our kind system, | > > > | by separating out matchable and unmatchable arrows. | > > > | - The rules for defaulting appear convenient in practice, but | > > > | are somewhat arbitrary. | > > > | - The rules for defaulting care about context -- does an | arrow | > > > | appear in the type of a term or the type of a type? These | rules | > > > | thus go against the spirit of #378, which advocates for not | > > > | accepting features that distinguish between types and terms. | > > > | | > > > | Recommendation: With reservations, I recommend acceptance. I | > > > | think that the power to use higher-order programming should | not | > > > | be restricted to terms, and allowing unsaturated functions at | > > > | compile time is necessary in order to have convenient | dependent types. | > > > | However, I am concerned about the extra complexity of | > > > | matchability. A key open question for me is how much | > > > | matchability is apparent to users | > > > | -- even ones using some higher-order type-level programming. | If | > > > | matchability is pervasive, then I would lean against. But my | > > > | expectation is that matchability fades into the background -- | > > > | much like levity polymorphism (unless you want it). | > > > | | > > > | Open question: What to do about syntax? The proposed syntax | is | > > > | sensible. However, #370 suggests an alternative syntax that | > > > | might be more forward-thinking. | > > > | | > > > | Richard | > > > | _______________________________________________ | > > > | ghc-steering-committee mailing list | > > > | ghc-steering-committee@haskell.org | > > > | | > > > | | https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F% | > > > | 2Fmail | > > > | .haskell.org%2Fcgi-bin%2Fmailman%2Flistinfo%2Fghc-steering- | > > > | | > > > | | committee&data=04%7C01%7Csimonpj%40microsoft.com%7Cbd9e62e31 | > > > | 37e403 | > > > | | > > > | | 85b5f08d88d8b91e0%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C1%7C6 | > > > | 374149 | > > > | | 78666235646%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoi | > > > | V2luMz | > > > | | IiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C1000&sdata=cIlDCT4r8C8Yc0 | > > > | %2BOib | > > > | Q%2F6Dv1qzBiB1PpavCdAJI3ruw%3D&reserved=0 | > > | > > _______________________________________________ | > > ghc-steering-committee mailing list | > > ghc-steering-committee@haskell.org | > > | https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fma | > > il.haskell.org%2Fcgi-bin%2Fmailman%2Flistinfo%2Fghc-steering- | committ | > > | ee&data=04%7C01%7Csimonpj%40microsoft.com%7C692997bb67394e8cab4f | > > | 08d897335e15%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C1%7C6374255946 | > > | 59710772%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzI | > > | iLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C3000&sdata=IBnpaWeHnKRh6p0Sv6s | > > imMc%2Ffai00Qi9%2B8OIsmGPQp0%3D&reserved=0 | > _______________________________________________ | > ghc-steering-committee mailing list | > ghc-steering-committee@haskell.org | > | https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fmail | > .haskell.org%2Fcgi-bin%2Fmailman%2Flistinfo%2Fghc-steering- | committee&a | > | mp;data=04%7C01%7Csimonpj%40microsoft.com%7C692997bb67394e8cab4f08d897 | > | 335e15%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C1%7C637425594659710772 | > | %7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6I | > | k1haWwiLCJXVCI6Mn0%3D%7C3000&sdata=IBnpaWeHnKRh6p0Sv6simMc%2Ffai00 | > Qi9%2B8OIsmGPQp0%3D&reserved=0 | > | _______________________________________________ | ghc-steering-committee mailing list | ghc-steering-committee@haskell.org | https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fmail | .haskell.org%2Fcgi-bin%2Fmailman%2Flistinfo%2Fghc-steering- | committee&data=04%7C01%7Csimonpj%40microsoft.com%7C692997bb67394e8 | cab4f08d897335e15%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C1%7C6374255 | 94659710772%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMz | IiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C3000&sdata=IBnpaWeHnKRh6p0Sv6si | mMc%2Ffai00Qi9%2B8OIsmGPQp0%3D&reserved=0 _______________________________________________ ghc-steering-committee mailing list ghc-steering-committee@haskell.org https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee
participants (7)
-
Alejandro Serrano Mena
-
Eric Seidel
-
Joachim Breitner
-
Richard Eisenberg
-
Simon Peyton Jones
-
Spiwack, Arnaud
-
Tom Harding