haskellforall

What does `forall` mean in this specific signature? (definition of Task in a build system in Haskell)


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 cis 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?


Solution

  • 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)