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