In Purescript, IO an other effects are managed with the Eff monad, and extensible effects, which are declared like this: main :: Eff (trace :: Trace, random :: Random) {}So if I understand well, this main declaration only allows to log to console, and generate random numbers. The trace :: Trace, random :: Random is a row of effect, ie an unordered labeled collection of effects.Now I get that Trace is an effect, and trace is its label. But why do we need both? It makes sense for records such as { foo::String, bar::String } but I cannot understand why I would need to manage two Random effect with different labels. ie I would write the following:main :: Eff (Trace, Random) {} -- no redundant labelsAre effect labels useful in purescript? If yes what for?
extensible effects in purescript
functional programming;purescript
The simple answer is that the machinery for rows already existed in the typechecker, from the very first release of the PureScript compiler, so it made sense to reuse it to define the Eff monad. The only change was to allow rows to be parameterized by the kind of the types indexed by their labels.It certainly seems like labels are unnecessary, and they would be if effects were merely symbols. Another answer, however, is that labels allow us to keep the desirable property of having most general unifiers in the type system.Contrived ExampleSuppose you defined a handler whose type contained a row of effects with two or more unknown type variables:runFooBarEffects :: forall eff foo bar. Eff (foo :: foo, bar :: bar | eff) a -> Eff (combined :: Baz foo bar | eff) aAnd a corresponding action with concrete effect types:myAction :: Eff (foo :: Foo, bar :: Bar, trace :: Trace) StringWhen we try to run this action with runFooBarEffects myAction, the typechecker correctly infers the result type Eff (combined :: Baz Foo Bar, trace :: Trace) String by unification.However, imagine if there were no labels present. The unification algorithm would not be able to proceed, because foo could be unified with either Foo or Bar, since rows are unordered. There is no longer a most general unifier for the two rows.This example is indeed contrived, but illustrates the point that since we are not restricted to simple atomic types (symbols) appearing in rows, but instead have a whole lattice of types, we need labels to keep the type system sane.