Deep Subsumption Proposal

[mpickering]

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.

[atravers]

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:

In practice, the trilemma is usually avoided by giving up on call-by-name or extensionality rather than weak-head normal forms. However, it may be that effective approaches to head evaluation such as those in this paper are of interest even in call-by-value languages or in settings (such as Haskell with seq) that lack the η axiom. Exploring the practical utility of head reduction may be a profitable avenue for future work.

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.