[ghc-steering-committee] Unsaturated type families (#242)
Simon Peyton Jones
simonpj at microsoft.com
Thu Dec 3 08:27:56 UTC 2020
I have written a comment on the GitHub thread
https://github.com/ghc-proposals/ghc-proposals/pull/242#issuecomment-737551909
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 <ghc-steering-committee-
| bounces at haskell.org> On Behalf Of Eric Seidel
| Sent: 03 December 2020 02:30
| To: ghc-steering-committee at 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 <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%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 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%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 at 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 at 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 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%7C692997bb67394e8
| cab4f08d897335e15%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C1%7C6374255
| 94659710772%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMz
| IiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C3000&sdata=IBnpaWeHnKRh6p0Sv6si
| mMc%2Ffai00Qi9%2B8OIsmGPQp0%3D&reserved=0
More information about the ghc-steering-committee
mailing list