How to apply higher order function to an effectful

问题:

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)

回答1:

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.

回答2:

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"