<div dir="ltr"><div>I often wish I could use unsaturated type families. Where I can see that going fairly mainstream in the medium term is in the higher-kinded-data-type sort of idiom. Whereby one parameterises the type of a record (say) by a family `f :: * -> *` and vary the family to great effect.</div><div><br></div><div>For instance, it would make the types in the multiplate library [ <a href="https://hackage.haskell.org/package/multiplate">https://hackage.haskell.org/package/multiplate</a> ] quite a bit more palatable.</div><div><br></div><div>Like Richard, I want to advance a prudent: yes. As far as alternatives go, I'm in favour of never inferring matchability polymorphism [ alternative 6, currently ].<br></div><div><br></div><div>That being said this is a proposal which touches the arrow, which makes it a fairly large proposal. So it does need more careful eyes to anticipate issues. The proposal is, in particular, not fully backwards compatible (it involves promotion of data constructors which take functions as arguments, it's hard to avoid it). So please, give this one a good reading. Let's make sure we are happy with it.</div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Fri, Nov 20, 2020 at 8:36 PM Richard Eisenberg <<a href="mailto:rae@richarde.dev">rae@richarde.dev</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">Hi committee,<br>
<br>
Csongor Kiss has proposed -XUnsaturatedTypeFamilies.<br>
<br>
Proposal: <a href="https://github.com/kcsongor/ghc-proposals/blob/unsaturated-type-families/proposals/0000-unsaturated-type-families.rst" rel="noreferrer" target="_blank">https://github.com/kcsongor/ghc-proposals/blob/unsaturated-type-families/proposals/0000-unsaturated-type-families.rst</a><br>
ICFP'19 paper: <a href="https://www.microsoft.com/en-us/research/uploads/prod/2019/03/unsaturated-type-families-icfp-2019.pdf" rel="noreferrer" target="_blank">https://www.microsoft.com/en-us/research/uploads/prod/2019/03/unsaturated-type-families-icfp-2019.pdf</a><br>
Discussion: <a href="https://github.com/ghc-proposals/ghc-proposals/pull/242" rel="noreferrer" target="_blank">https://github.com/ghc-proposals/ghc-proposals/pull/242</a><br>
<br>
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.<br>
<br>
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.<br>
<br>
The proposal also includes matchability polymorphism, the ability to abstract over a matchability parameter.<br>
<br>
Pros:<br>
+ This proposal greatly increases the expressiveness of Haskell's type system.<br>
+ With this proposal, we can finally do proper functional programming in types, rather than just in terms.<br>
+ 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 <a href="https://adam.gundry.co.uk/pub/thesis/" rel="noreferrer" target="_blank">https://adam.gundry.co.uk/pub/thesis/</a>, 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.)<br>
+ There is a prototype implementation.<br>
+ The ideas are backed up by peer-reviewed research.<br>
+ 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.<br>
<br>
Cons:<br>
- This adds a new dimension of complexity to our kind system, by separating out matchable and unmatchable arrows.<br>
- The rules for defaulting appear convenient in practice, but are somewhat arbitrary.<br>
- 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.<br>
<br>
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).<br>
<br>
Open question: What to do about syntax? The proposed syntax is sensible. However, #370 suggests an alternative syntax that might be more forward-thinking.<br>
<br>
Richard<br>
_______________________________________________<br>
ghc-steering-committee mailing list<br>
<a href="mailto:ghc-steering-committee@haskell.org" target="_blank">ghc-steering-committee@haskell.org</a><br>
<a href="https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee" rel="noreferrer" target="_blank">https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee</a><br>
</blockquote></div>