Combining constraints in PureScript

Combining and reusing constraints is directly supported in Haskell, but PureScript has to be tamed.

Motivation

Suppose I have a function like this:

f :: forall m. MonadFoo m => MonadBar m => MonadBaz m => m Qux

And suppose I have a whole bunch of such functions that are all related — i.e working on related data and calling each other, so that they all have the same three constraints. This leads to repetition: the three constraints need to be written out for every function.

Solution: first draft

In Haskell, I can combine them with a Constraint-kinded type:

type MyM m = (MonadFoo m, MonadBar m, MonadBaz m)
f :: forall m. MyM m => m Qux

But I can’t do this in PureScript, because it does not support constraint kinds. However, PureScript does support constrained types instead, so I could declare a type like this:

type MyM m a = MonadFoo m => MonadBar m => MonadBaz m => a
f :: forall m. MyM m (m Qux)

Photo by Joel Peel

Ergonomics

But this gives me two more problems:

• This doesn’t look like MyM is a constraint (which it is semantically), and
• I had to put parentheses around the return type.

When I meet an extra pair of parentheses in value expressions, I just set off my trusty operator $ onto them:

apply f x = f x
infixr 0 apply as $
a = f x $ g y    -- equivalent to "f x (g y)"

Can I do the same thing at type level? Indeed I can!

type App a b = a b
infixr 0 type App as :=>
f :: forall m. MyM m :=> m Qux    -- equivalent to "MyM m (m Qux)"

The specific choice of characters :=> is dictated by the desire for the final product to look “sort of” like a real constraint.

Composition

Additionally, this trick allows combining multiple such “complex” constraints, also without using parentheses:

type OneM m a = MonadFoo m => MonadBar m => a
type TwoM m a = MonadBaz m => a
g :: forall m. OneM m :=> TwoM m :=> m Qux

Or even declare a new “complex” constraint by combining several other “complex” constraints:

type OnePlusTwoM m a = OneM m :=> TwoM m :=> a

Or mix and match in various combinations:

type OneM m a = MonadFoo m => MonadBar m => a
type TwoM m a = MonadBaz m => a
type ThreeM m a = OneM m :=> MonadWhat m => TwoM :=> a
g :: forall m. Functor m => ThreeM m :=> m Qux

The rule of thumb is:

• “Normal” constraints (i.e. type classes) get a regular fat arrow to their right, e.g. Functor m =>
• “Complex” constraints (i.e. type FooM m a) get a colon-fat-arrow to their right, e.g. FooM m :=>

Advanced uses

One interesting possibility is “hiding” additional variables inside the constraint under certain circumstances. For example, suppose my function wants to have a network capability and wants to perform requests in parallel. We use the Parallel type class for that:

getBar :: forall m. MonadHttp m => m Bar
getBaz :: forall m. MonadHttp m => m Baz
mkFoo :: Bar -> Baz -> Foo
fetchFoo :: forall m p. MonadHttp m => Parallel p m => m Foo
fetchFoo = sequential $
    mkFoo <$> parallel getBar <*> parallel getBaz

Now whoever calls such function has to declare another seemingly extraneous parameter p, for example:

fetchTen :: forall m p. MonadHttp m => Parallel p m => m (Array Foo)
fetchTen = sequence $ fetchFoo <$> (0..10)

In this example, fetchTen itself doesn’t do anything parallel, so it’s unclear why the variable p is needed. The answer is, it’s needed in order to call fetchFoo, but this feels kind of redundant. Can’t fetchTen just say that it needs whatever fetchFoo needs and be done with it? Yes, it can!

type FetchFooM m a = forall p. MonadHttp m => Parallel p m => a
fetchFoo :: forall m. FetchFooM m :=> m Foo
fetchTen :: forall m. FetchFooM m :=> m (Array Foo)

This works, because there is a functional dependency on the Parallel class: m -> p. It means that p can be uniquely determined if you know what m is. Because of this, whoever calls fetchFoo needs only to choose m, and the choice of p then becomes fixed. And because nobody actually needs to choose it, it can remain hidden and out of sight inside FetchFooM.

A gotcha (because of course there is one)

For some reason, the type-level thin arrow -> has the lowest priority in PureScript, there is no way to declare a type-level operator that binds weaker. This means that the :=> operator binds stronger than the thin arrow, which means that this:

wtf :: forall m. MyM m :=> String -> m Qux

is equivalent to this:

wtf :: forall m. (MyM m :=> String) -> m Qux

which is equivalent to this:

wtf :: forall m. MyM m String -> m Qux

which is not at all what we meant.

There are two workarounds for this:

• Bring back the parentheses:
  wtf :: forall m. MyM m :=> (String -> m Qux)
• Add another “regular” constraint after the “complex” one:
  wtf :: forall m. MyM m :=> Monad m => String -> m Qux

The second workaround works, because, apparently, the fat arrow => has a priority higher than zero (which makes sense), so that it ends up binding
stronger than :=>, and everything works out.