Combining constraints in PureScript

Indeed I can!type App a b = a binfixr 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.

CompositionAdditionally, this trick allows combining multiple such “complex” constraints, also without using parentheses:type OneM m a = MonadFoo m => MonadBar m => atype TwoM m a = MonadBaz m => ag :: forall m.

OneM m :=> TwoM m :=> m QuxOr even declare a new “complex” constraint by combining several other “complex” constraints:type OnePlusTwoM m a = OneM m :=> TwoM m :=> aOr mix and match in various combinations:type OneM m a = MonadFoo m => MonadBar m => atype TwoM m a = MonadBaz m => atype ThreeM m a = OneM m :=> MonadWhat m => TwoM :=> ag :: forall m.

Functor m => ThreeM m :=> m QuxThe 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 usesOne 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 BargetBaz :: forall m.

MonadHttp m => m BazmkFoo :: Bar -> Baz -> FoofetchFoo :: forall m p.

MonadHttp m => Parallel p m => m FoofetchFoo = sequential $ mkFoo <$> parallel getBar <*> parallel getBazNow 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 Foog :: 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 Quxis equivalent to this:wtf :: forall m.

(MyM m :=> String) -> m Quxwhich is equivalent to this:wtf :: forall m.

MyM m String -> m Quxwhich 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 QuxThe 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.

.. More details

Leave a Reply