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 => af :: forall m. MyM m (m Qux)
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 => ag :: 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 :=> ag :: 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 -> FoofetchFoo :: 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 => afetchFoo :: forall m. FetchFooM m :=> m FoofetchTen :: 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.