Logo Questions Linux Laravel Mysql Ubuntu Git Menu
 

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

Tags:

haskell

monads

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)
like image 806
PDani Avatar asked Jun 10 '14 13:06

PDani


2 Answers

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"
like image 23
bheklilr Avatar answered Oct 19 '22 20:10

bheklilr


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.

like image 198
chi Avatar answered Oct 19 '22 22:10

chi