[ghc-steering-committee] Quick look impredicativity (#274) — recommendation: accept

[Spiwack, Arnaud]

Dear all,

As the title implies: I'm hereby recommending accepting the Quick look
impredicativity proposal.

Summary:

The proposal modifies the `-XImpredicativeTypes` extension with a well
defined semantics which consists in considering n-ary applications, rather
than binary. And look, in such an application, for arguments which
absolutely require impredicative instantiation (either universally
quantified type applications, or arguments where a universal type is
guarded by an invariant type constructor).

In order to have the expected behaviour for `($)` and `(.)`, the proposal
also makes the left-hand argument of the arrow invariant with respect to
instantiation (currently: contravariant). The proposal is to make this
change effective, even if `-XRankNTypes` is turned on, but not
`-XImpredicativeTypes`. The proposal also introduces an extension
`-XContravariantFunctions` to restore the old behaviour, for compatibility.

Rational:

`-XImpredicativeTypes` is a useful extension which is currently in a rather
sad state. I'm happy to see it stabilise to a clear semantics. The
semantics in the proposal covers a ton of use cases. It strikes a very good
balance between usefulness and predictability.

The use of n-ary application in the type system also has good theoretical
roots: sequent calculi have n-ary applications. (in manyrespects,
bidirectional type systems are also about n-ary application). So I don't
consider it a wart at all.

The propsal's semantics, including the absence of contravariant functions,
goes in the direction of _guessing less things_. This is a direction that
many GHC features have taken lately. I think it's a very very good
direction! Guessing can be damaging for predictability, but. more
importantly, guessing has a tendency to compose badly with other typing
features. (it is to be noted, too, that the implementation of contravariant
functions. in GHC, eta-expands the function, which can casually change its
semantics, if the function was bottom).

So, everything in this proposal does look good to me, except that, I think,
I would like a deprecation route for the `-XContravariantFunctions`
extension. Otherwise, we will be stuck with legacy code forever.

Best,
Arnaud
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-steering-committee/attachments/20191014/7ca62e31/attachment.html>