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

[Simon Peyton Jones]

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