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

[Alejandro Serrano Mena]

 Hi everybody,
I really like this proposal. However:
- I think the defaulting rules should be revised. Not only because it may
conflict with #378 (if accepted), but because I think that the rules should
not differentiate between terms and types because getting different
outcomes from term functions and type function / families would be
surprising.
- I think we should wait until we decide about #370 for the syntax.

Regards,
Alejandro

On 20 Nov 2020 at 20:36:12, Richard Eisenberg <rae at richarde.dev> wrote:

> Hi committee,
>
> Csongor Kiss has proposed -XUnsaturatedTypeFamilies.
>
> Proposal:
> https://github.com/kcsongor/ghc-proposals/blob/unsaturated-type-families/proposals/0000-unsaturated-type-families.rst
> ICFP'19 paper:
> https://www.microsoft.com/en-us/research/uploads/prod/2019/03/unsaturated-type-families-icfp-2019.pdf
> Discussion: https://github.com/ghc-proposals/ghc-proposals/pull/242
>
> 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://adam.gundry.co.uk/pub/thesis/, 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://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/20201125/98ab4243/attachment.html>