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

[Eric Seidel]

I support acceptance too, modulo a few small comments that I left on the GH discussion.

On Mon, Oct 14, 2019, at 02:53, Spiwack, Arnaud wrote:
> 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
> _______________________________________________
> ghc-steering-committee mailing list
> ghc-steering-committee at haskell.org
> https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee
>