Deep Subsumption Proposal

We invite comment about the Deep Subsumption proposal. The proposal invites the community to comment on a technical solution to the issues introduced by the simplified subsumption proposal.

The simplified subsumption proposal argued in favour of simplifying the subsumption judgement in GHC’s type system, by removing:

  • Covariance and contravariance of function types
  • Deep skolemisation
  • Deep instantiation.

The change was motivated by wanting to simplify both the implementation and language semantics, as well as being a stepping-stone to the implementation of Quick-look impredicativity.

Unfortunately, the breakage study failed to accurately predict how annoying this change would be to users. Some common patterns found in libraries now require eta-expansion, when the compiler used to automatically insert the appropriate lambdas.

This proposal suggests adding a new language extension, DeepSubsumption, enabled by default in the common case when the language is set to -XHaskell2010, which recovers the previous subsumption rules. This would allow users to opt-in to deep subsumption as it was before GHC-9.0.

12 Likes

Has there been any interest in implementing the technique described by Philip Johnson-Freyd, Paul Downen and Zena Ariola in their paper First Class Call Stacks: Exploring Head Reduction? From page 16 of 18:

From a cursory glance, the most prominent question (for Haskell anyway) is whether the technique can be adapted for use with call-by-need languages without excessive complexity: more information needed.

1 Like