R/haskell - Was simplified subsumption worth it for industry Haskell

Here is a more detailed analysis and two potential solutions. Unfortunately both solutions have downsides of their own.

Take your first example:

readFreqSumFile file = readFreqSumProd $ withFile file ReadMode (\h -> PB.fromHandle h)

First of all, note the name of the commit: “Naively adapt to simplified subsumption”. That suggests that the authors still want to look for better solutions.

Digging a bit deeper, that fromHandle :: MonadIO m => Handle -> Producer' ByteString m () function depends critically on this definition:

type Producer' b m r = forall x' x. Proxy x' x () b m r 

Such type synonyms with forall quantifiers should be considered an anti-pattern now with simplified subsumption. There was a similar issue reported to the GHC issue tracker: Possible work-around for implicit params and simplified subsumption? (#21168) · Issues · Glasgow Haskell Compiler / GHC · GitLab

Solution 1. Use newtypes

@simonpj suggests making these type synonyms into newtypes:

newtype Producer' b m r = MkProducer' (forall x' x. Proxy x' x () b m r)

If you implement all the required constraints for this type then you can just write the original:

readFreqSumFile file = readFreqSumProd $ withFile file ReadMode PB.fromHandle

But this is not quite a good solution here, because I believe you can’t automatically derive all the instances and you cannot compose these producers with other pipes.

This interoperability could probably be restored by using the same tricks that the optics library uses to get their lenses to compose, but that seems like quite a big change here.

Solution 2. Rewrite type synonyms in place

Another simple change to resolve this is to just rewrite the type synonyms in-place:

fromHandle :: MonadIO m => Handle -> Proxy x' x () ByteString m ()

Then you can also just write the original non-eta-expanded version. But a problem is that it is harder understand that the Proxy in this case really must be a producer.

So what then?

Edit: Actually, what I propose here is rife with edge-cases, see this comment on the simplified subsumption pull request

One thing that comes to my mind with increasing frequency is a way to abstract over patterns like that Proxy x' x in a different way. Currently you can do two things: make these variables parameters of the type:

type Producer' x' x b m a = Proxy x' x b m a

or you can use a forall to bind the variables:

type Producer' b m a = forall x' x. Proxy x' x b m a

Sometimes neither is ideal.

What if we could have other abstraction mechanisms, such as a way to say that these variables should always be floated out to the binding the type belongs to. A question remains whether the variable should be shared across all occurrences of this type synonym or not. In this case we always want these variables to be as free as possible, so it should always rewrite multiple occurrences of the synonym like this:

x :: <...> Producer' b1 m1 a1 <...> Producer' b2 m2 a2 <...>

To:

x :: forall x1' x1 x2' x2. <...> Proxy x1' x1 b1 m1 a1 <...> Proxy x2' x2 b2 m2 a2 <...>

Another example of a use case where this would be useful, but with slightly different requirements is a type synonym for semigroups. In a function with signature like this:

append :: A -> A -> A

You might want to instantiate A to [a] to get:

append :: forall a. [a] -> [a] -> [a]

As you can see the type variables should be floated out, but this time they should be shared between each occurrence of the synonym A.

This is not something you see every day in Haskell code, but it comes up when writing backpack signatures. For a more complicated real world example where this came up for me, see: Add `primitive` as a boot dependency (#20299) · Issues · Glasgow Haskell Compiler / GHC · GitLab

4 Likes