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

[Simon Peyton Jones]

I strongly support acceptance.   I think is a genuine step forward, specifically because it has such a nice, small, modular, and (critically) non-invasive implementation.  And we already have that implementation, so it’s not just an aspirational claim.

Moreover, precisely because the implementation is so simple, the explanation to the user can be correspondingly simple.

I’ve been trying to get here for well over a decade, and now I feel that we have finally landed.   Hooray.

Declaration of interest: I’m part of the team that developed the idea.

Simon

From: ghc-steering-committee <ghc-steering-committee-bounces at haskell.org> On Behalf Of Spiwack, Arnaud
Sent: 14 October 2019 07:54
To: ghc-steering-committee <ghc-steering-committee at haskell.org>
Subject: [ghc-steering-committee] Quick look impredicativity (#274) — recommendation: accept

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/fc2aeabd/attachment-0001.html>