[ghc-steering-committee] Unsaturated type families (#242)
Eric Seidel
eric at seidel.io
Thu Dec 3 02:29:41 UTC 2020
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 <rae at richarde.dev> 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 <simonpj at 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 <ghc-steering-committee-
> > > | bounces at haskell.org> On Behalf Of Richard Eisenberg
> > > | Sent: 20 November 2020 19:36
> > > | To: Simon Peyton Jones via ghc-steering-committee <ghc-steering-
> > > | committee at 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.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 at 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 at haskell.org
> > https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee
> _______________________________________________
> ghc-steering-committee mailing list
> ghc-steering-committee at haskell.org
> https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee
>
More information about the ghc-steering-committee
mailing list