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

Wed Dec 2 15:30:37 UTC 2020

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
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-steering-committee/attachments/20201202/2b2036ff/attachment.html>