I am reading the paper Build systems à la carte by A. Mokhov, N. Mitchell and S. Peyton Jones.
One of the first concepts they define is that of a Task
. It has type
newtype Task c k v = Task ( forall f. c f => (k -> f v) -> f v )
where c
is a constraint (e.g. Applicative
or Monad
), k
is the type of keys, and v
of values.
I need some help parsing the meaning forall f
in the above definition. If the definition of Task
had been
newtype Task k v = Task ( (k -> v) -> v )
then it would be clear: a Task is a way to build a value in v
, given a way (k -> v)
to retrieve its inputs from the corresponding keys.
If we add f
to the mix, what changes? How can one even define a task, if it must accept inputs of type (k -> f v)
for any possible f
satisfying c
?
CodePudding user response:
You have correctly understood the forall - the function must work for any possible f.
To define a task remember we will know what c is, so we can use the facilities of Applicative or Monad.
Let's say we want a Task Monad Int String
t :: Task Monad Int String
t = Task taskFunction
So we need a function that will work for any monad.
taskFunction :: forall f . Monad f => (Int -> f String) -> f String
(The forall could be left out in this signature, it would be implied anyway.)
And we write it using bind, return, do notation, etc.
taskFunction getter = do x <- getter 37
y <- getter 42
return (x y)