How to apply higher order function to an effectful function in Haskell?

Question

I have too functions:

higherOrderPure :: (a -> b) -> c
effectful :: Monad m => (a -> m b)

I'd like to apply the first function to the second:

higherOrderPure `someOp` effectful :: Monad m => m c

where

someOp :: Monad m => ((a -> b) -> c) -> (a -> m b) -> m c

Example:

curve :: (Double -> Double) -> Dia Any 
curve f = fromVertices $ map p2 [(x, f x) | x <- [1..100]]

func :: Double -> Either String Double
func _ = Left "Parse error" -- in other cases this func can be a useful arithmetic computation as a Right value

someOp :: ((Double -> Double) -> Dia Any) -> (Double -> Either String Double) -> Either String (Dia Any)
someOp = ???

curve `someOp` func :: Either String (Dia Any)

What is `map p2 (x, f x)` supposed to be doing? `map p2` implies that `p2` is a function, so `(x, f x)` _must_ be a list, but it is clearly a tuple. I also doubt that the `Dia` type is just an alias for lists, since `curve f = [...]`, meaning `curve` returns a list. Can you update your question with a working example? It also might help to include the type signatures of `p2` and `fromVertices`. — bheklilr, Jun 10 '14 at 13:20
That makes it much easier to understand what's going on, thanks! — bheklilr, Jun 10 '14 at 13:22
Which library are you using to do this? I'd like to browse its documentation to figure out if this problem is solvable in the way you want — bheklilr, Jun 10 '14 at 13:36
http://projects.haskell.org/diagrams/, but that's kind of irrelevant, the question is more like theoretical, the example is only for better understanding. — PDani, Jun 10 '14 at 13:47
I still can't find a way to unify a list type with the `Diagram` type (I'm assuming you're using `type Dia a = QDiagram B R2 a` with whichever backend you're using). Did you mean that extra layer of square brackets around `fromVerticies $ map p2 ...`? I think instead you meant `curve f = fromVertices $ map p2 [(x, f x) | x <- [1..100]]`, since that also balances your brackets. — bheklilr, Jun 10 '14 at 14:20

chi · Accepted Answer · 2014-06-10T14:24:33.750

23

The type

Monad m => ((a -> b) -> c) -> (a -> m b) -> m c

is not inhabited, i.e., there is no term t having that type (unless you exploit divergence, e.g. infinite recursion, error, undefined, etc.).

This means, unfortunately, that it is impossible to implement the operator someOp.

Proof

To prove that it is impossible to construct such a t, we proceed by contradiction. Assume t exists with type

t :: Monad m => ((a -> b) -> c) -> (a -> m b) -> m c

Now, specialize c to (a -> b). We obtain

t :: Monad m => ((a -> b) -> a -> b) -> (a -> m b) -> m (a -> b)

Hence

t id :: Monad m => (a -> m b) -> m (a -> b)

Then, specialize the monad m to the continuation monad (* -> r) -> r

t id :: (a -> (b -> r) -> r) -> ((a -> b) -> r) -> r

Further specialize r to a

t id :: (a -> (b -> a) -> a) -> ((a -> b) -> a) -> a

So, we obtain

t id const :: ((a -> b) -> a) -> a

Finally, by the Curry-Howard isomorphism, we deduce that the following is an intuitionistic tautology:

((A -> B) -> A) -> A

But the above is the well-known Peirce's law, which is not provable in intuitionistic logic. Hence we obtain a contradiction.

Conclusion

The above proves that t can not be implemented in a general way, i.e., working in any monad. In a specific monad this may still be possible.

edited Jun 10 '14 at 14:24

answered Jun 10 '14 at 13:55

chi

111,837
3
133
218

1

`peirce k = k unsafeCoerce` :) – András Kovács Jun 10 '14 at 16:45
1

peirce = undefined someOp = undefined FunctionToSolveWorldProblems = undefined – PyRulez Jun 10 '14 at 17:36
Is it even possible to have a function of type `(a -> b) -> c`? You can have specialized versions of this type, but never this type itself, I would think: how can I write a function which, given a function between any two types you like, returns a value of any other third type you like? – amalloy Jun 10 '14 at 19:19
@amalloy Indeed, but `Monad m => ((a -> b) -> c) -> (a -> m b) -> m c` allows for specialisation. For the argument to be uninhabited, we would have to prevent specialisation by using a higher-rank type, e.g. `(forall a. b. c. (a -> b) -> c) -> etc`. – duplode Jun 10 '14 at 19:36
1

@amalloy The polymorphic type `(a -> b) -> c` is not inhabited. If it were, the logical proposition `(A -> B) -> C` would be an intuitionistic tautology, but it is not even a classical tautology. That is, if `A=B=True` and `C=False` then `(A -> B) -> C` is false. This proves that it is not possible to construct a term of said polymorphic type. Specific instances (e.g. `a=b=c=Int`) are inhabited, though. – chi Jun 10 '14 at 19:48

score 5 · Answer 2 · answered Jun 10 '14 at 14:31

I think you can achieve what you want by writing a monadic version of curve:

curveM :: Monad m => (Double -> m Double) -> m (QDiagram B R2 Any)
curveM f = do
    let xs = [1..100]
    ys <- mapM f xs
    let pts = map p2 $ zip xs ys
    return $ fromVertices pts

This can easily be written shorter, but it has the type you want. This is analogous to map -> mapM and zipWith -> zipWithM. The monadic versions of the functions have to be separated out into different implementations.

To test:

func1, func2 :: Double -> Either String Double
func1 x = if x < 1000 then Right x else Left "Too large"
func2 x = if x < 10   then Right x else Left "Too large"

> curveM func1
Right (_ :: QDiagram B R2 Any)
> curveM func2
Left "Too large"

How to apply higher order function to an effectful function in Haskell?

2 Answers2

Proof

Conclusion

Linked