Re: [ghc-steering-committee] Unsaturated type families (#242)

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