[Haskell-cafe] Re: a regressive view of support for imperative programming in Haskell

[apfelmus]

Benjamin Franksen wrote:
> As has been already mentioned in this thread, in
> http://www.soi.city.ac.uk/~ross/papers/Applicative.html Conor McBride and
> Ross Paterson invent/explain a new type class that is now part of the base
> package (Control.Applicative). They also use/propose syntactic sugar for
> it, i.e.
> 
> pure f <*> u1 <*> ... <*> un
> 
> ~~> (| f u1 ... un |)
> 
> (I just made up the symbols '(|' and '|)', the concrete syntax would have to
> be fixed by people more knowledgeable than me.)

The problem with [| and |] lifted to monads that this only works for
fully applied arguments, i.e. that

   handle :: IO Handle
   string :: IO String

   [| hPutStr handle string |] :: IO ()

works but

    [| hPutStr handle |]
   = join (return hPutStr `ap` handle)
  ^= join ((f :: m (a -> b -> m c)) `ap` (x :: m a))
   = join ( y :: m (b -> m c))

is a type error.

I think this is also what makes the (<- action) proposal so non-local
and what is the source of this whole discussion. The core problem is:

   Functions like  a -> b -> m c  can't be partially applied to
   monadic actions like  m a  without specifying the number of
   arguments in advance. In other words, such functions aren't
   curried correctly.

Clearly, LiftMn specifies the number of arguments. But _both_ the (<-) 
proposal and idiom brackets specify the number of arguments too! Namely 
by requiring that all arguments are fully applied. So, neither one is 
capable of partially applying the first argument without saturating the 
call, you can only write

   handle :: IO Handle

     -- define putStr in terms of the above hPutStr
   putStr :: String -> IO ()
   putStr = \x -> [| hPutStr handle (return x) |]
   putStr = \x -> do { hPutStr (<- handle) x }


One way to get currying for monads is to work with functions

   m a -> m b -> m c

However, this type is larger than  a -> b -> m c  , i.e. the function

   from :: Monad m => (a -> b -> m c) -> (m a -> m b -> m c)
   from f ma mb = ma >>= \a -> mb >>= \b -> f a b

is not surjective since we could perform the actions in a different order

   from2 f ma mb = mb >>= \b -> ma >>= \a -> f a b

In other words, if someone gives you a value of type  m a -> m b -> m c 
  , then you can't convert it to  a -> b -> m c  and back without 
risking that you end up with a different result.


But there is another type suitable for currying

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

which I believe is in some way equivalent to  a -> b -> m c

   from :: Monad m => (a -> b -> m c) -> m (a -> m (b -> m c))
   from f = return $ \a -> return $ \b -> f a b

   to   :: Monad m => m (a -> m (b -> m c)) -> (a -> b -> m c)
   to f a b = f >>= \g -> g a >>= \h -> h b

but I'm not sure. My assumption is that we have an equivalence

   forall a,b . m (a -> m b) ~ (a -> m b)

because any side effect executed by the extra m on the outside can well 
be delayed until we are supplied a value a. Well, at least when all 
arguments are fully applied, for some notion of "fully applied"

Anyway, here's how to curry with that type:

   (@) :: Monad m => m (a -> m b) -> (m a -> m b)
   (@) f x = join (f `ap` x)

   hPutStr :: IO (Handle -> IO (String -> IO ()))
   handle  :: IO Handle

   putStr :: IO (String -> IO ())
   putStr = hPutStr @ handle

With the infix type synonym

   type (~>) a b = a -> IO b

we can also write

   hPutStr :: IO (Handle ~> String ~> () )
   putStr  :: IO (String ~> () )

This is of course the Kleisli-Arrow which explains why currying works.


Regards,
apfelmus