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


i have functions:

higherorderpure :: (a -> b) -> c effectful :: monad m => (a -> m b) 

i'd apply first function 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  curve f = fromvertices $ map p2 [(x, f x) | x <- [1..100]]  func :: double -> either string double func _ = left "parse error" -- in other cases func can useful arithmetic computation right value  someop :: ((double -> double) -> dia any) -> (double -> either string double) -> either string (dia any) someop = ???  curve `someop` func :: either string (dia any) 

the type

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

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

this means, unfortunately, impossible implement operator someop.

proof

to prove impossible construct such t, proceed contradiction. assume t exists type

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

now, specialize c (a -> b). obtain

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

hence

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

then, specialize monad m continuation monad (* -> r) -> r

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

further specialize r a

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

so, obtain

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

finally, curry-howard isomorphism, deduce following intuitionistic tautology:

((a -> b) -> a) -> 

but above well-known peirce's law, not provable in intuitionistic logic. hence obtain contradiction.

conclusion

the above proves t can not implemented in general way, i.e., working in monad. in specific monad may still possible.


Comments

Popular posts from this blog

database - VFP Grid + SQL server 2008 - grid not showing correctly -

jquery - Set jPicker field to empty value -

.htaccess - htaccess convert request to clean url and add slash at the end of the url -