[Haskell-cafe] Re: a regressive view of support for imperative programming in Haskell
Stefan O'Rear wrote: apfelmus wrote: 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 I figured that wouldn't be a problem since our values don't escape, and the functions we define all respect the embedding... More formally: Projections and injections: proj :: Monad m = m (a - m b) - (a - m b) proj ma = \x - ma = \fn' - fn' x inj fn = return fn Define an equivalence relation: ma ≡ mb - proj ma = proj mb Projection respects equivalence: ma ≡ mb - proj ma = proj mb(intro -) ma ≡ mb = proj ma = proj mb(equiv def) proj ma = proj mb = proj ma = proj mb (assumption) Application respects equivalence: Yeah, that's the right approach, but it has a few typos. The correct version is (@) :: Monad m = m (a - m b) - m a - m b (@) ma = \x - x = proj ma Formulating (@) in terms of proj ma is a very clever idea since it follows immediately that ma @ x = ma' @ x iff proj ma = proj ma' iff ma ≡ ma' In other words, when viewed through @ and proj only, equivalent actions give equivalent results. The main point is that this does not hold for the other curry-friendly type m a - m b proj :: Monad m = (m a - m b) - (a - m b) proj f = f . return (@) :: Monad m = (m a - m b) - m a - m b (@) = id ma ≡ ma' iff proj ma = proj ma' since those functions may execute their argument multiple times. So, here's the counterexample once :: Monad m = m A - m A once = id twice :: Monad m = m A - m A twice x = x once x Now, we have proj once = return = proj twice but effect :: IO () -- a given effect effect = putStrLn Kilroy was here! once @ effect = effect ≠ twice @ effect = effect effect The same can be done for several arguments, along the lines of proj2 :: m (a - m (b - m c)) - (a - b - m c) proj2 f = proj . (proj f) app2 :: m (a - m (b - m c)) - (m a - m b - m c) app2 f mx my = (f @ mx) @ my = my = proj (mx = proj f) = my = \y - mx = \x - proj2 f x y and similar results. Regards, apfelmus ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Re: a regressive view of support for imperative programming in Haskell
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
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: a regressive view of support for imperative programming in Haskell
On Mon, Aug 13, 2007 at 04:35:12PM +0200, apfelmus wrote: 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 (\a x - a = ($ x)) ((\f - return f) X) == (β) (\a x - a = ($ x)) (return X) == (β) (\x - (return X) = ($ x)) == (monad law) (\x - ($ x) X)== (β on the sugar-hidden 'flip') (\x - X x)== (η) X Up to subtle strictness bugs arising from my use of η :), you're safe. Stefan signature.asc Description: Digital signature ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Re: a regressive view of support for imperative programming in Haskell
Stefan O'Rear schrieb: On Mon, Aug 13, 2007 at 04:35:12PM +0200, apfelmus wrote: 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 (\a x - a = ($ x)) ((\f - return f) X) == (β) (\a x - a = ($ x)) (return X) == (β) (\x - (return X) = ($ x)) == (monad law) (\x - ($ x) X)== (β on the sugar-hidden 'flip') (\x - X x)== (η) X Up to subtle strictness bugs arising from my use of η :), you're safe. Yes, but that's only one direction :) The other one is the problem: return . (\f x - f = ($ x)) =?= id Here's a counterexample f :: IO (a - IO a) f = writeAHaskellProgram return return f' :: IO (a - IO a) f' = return $ (\f x - f = ($ x)) $ f == (β) return $ \x - (writeAHaskellProgram return return) = ($ x) == (BIND) return $ \x - writeAHaskellProgram (return return = ($ x)) == (LUNIT) return $ \x - writeAHaskellProgram (($ x) return) == (β) return $ \x - writeAHaskellProgram return x Those two are different, because clever = f return () = writeAHaskellProgram clever' = f' return () = return () are clearly different ;) Regards, apfelmus ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: a regressive view of support for imperative programming in Haskell
On Mon, Aug 13, 2007 at 05:39:34PM +0200, apfelmus wrote: Stefan O'Rear schrieb: On Mon, Aug 13, 2007 at 04:35:12PM +0200, apfelmus wrote: 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 (\a x - a = ($ x)) ((\f - return f) X) == (β) (\a x - a = ($ x)) (return X) == (β) (\x - (return X) = ($ x)) == (monad law) (\x - ($ x) X)== (β on the sugar-hidden 'flip') (\x - X x)== (η) X Up to subtle strictness bugs arising from my use of η :), you're safe. Yes, but that's only one direction :) The other one is the problem: return . (\f x - f = ($ x)) =?= id Here's a counterexample f :: IO (a - IO a) f = writeAHaskellProgram return return f' :: IO (a - IO a) f' = return $ (\f x - f = ($ x)) $ f == (β) return $ \x - (writeAHaskellProgram return return) = ($ x) == (BIND) return $ \x - writeAHaskellProgram (return return = ($ x)) == (LUNIT) return $ \x - writeAHaskellProgram (($ x) return) == (β) return $ \x - writeAHaskellProgram return x Those two are different, because clever = f return () = writeAHaskellProgram clever' = f' return () = return () are clearly different ;) I figured that wouldn't be a problem since our values don't escape, and the functions we define all respect the embedding... More formally: Projections and injections: proj ma = \x - ma = \ fn' - fn' x inj fn = return fn Define an equivalence relation: ma ≡ mb - proj ma = proj mb Projection respects equivalence: ma ≡ mb - proj ma = proj mb(intro -) ma ≡ mb = proj ma = proj mb(equiv def) proj ma = proj mb = proj ma = proj mb (assumption) Application: (@) ma1 = \x - join (proj ma1 x) Application respects equivalence: ma1 ≡ ma2 - (@) ma1 = (@) ma2 (intro -) ma1 ≡ ma2 = (@) ma1 = (@) ma2 (β) ma1 ≡ ma2 = (\x - join (proj ma1 x)) = (\x - join (proj ma2 x)) (extensionality) ma1 ≡ ma2 = join (proj ma1 x) = join (proj ma2 x)(application respects = left) ma1 ≡ ma2 = proj ma1 x = proj ma2 x(application respects = right) ma1 = ma2 = proj ma1 = proj ma2(lemma) Stefan signature.asc Description: Digital signature ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: a regressive view of support for imperative programming in Haskell
David Roundy wrote: The only cost is that this syntax relies on the do notation, and thus makes the desugaring of that do notation slightly more complicated when used. If I understand correctly, do blah f (do foo bar (- action) ) blah has an ambiguity: which do-block is the action bound in? I can easily imagine myself being frustrated at having to refactor my code if the defined answer is not the one I want at the moment. Isaac ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: a regressive view of support for imperative programming in Haskell
On Mon, Aug 13, 2007 at 01:27:45PM -0300, Isaac Dupree wrote: David Roundy wrote: The only cost is that this syntax relies on the do notation, and thus makes the desugaring of that do notation slightly more complicated when used. If I understand correctly, do blah f (do foo bar (- action) ) blah has an ambiguity: which do-block is the action bound in? I can easily imagine myself being frustrated at having to refactor my code if the defined answer is not the one I want at the moment. It doesn't have an ambiguity, because it's defined to be bound in the innermost do loop. This isn't a new concept, the - syntax in the existing do notation has the same behavior. -- David Roundy Department of Physics Oregon State University ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Re: a regressive view of support for imperative programming in Haskell
Donn Cave wrote: (I have a soft spot for O'Haskell, but alas I must be nearly alone on that.) You are /not/ alone :-) I always found it very sad that O'Haskell and also its sucessor Timber (with all the good real-time stuff added) died the 'quick death' of most research languages. Cheers Ben ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Re: a regressive view of support for imperative programming in Haskell
David Roundy wrote: Several times since reading the beginning of this discussion I've wished I had the new syntax so I could write something like: do if predicateOnFileContents (- readFile foo) then ... instead of either do contents - readFile foo if predicateOnFileContents contents then ... or (as you'd prefer) readFile foo = \contents - if predicateOnFileContents contents then ... Isn't this problem, namely being forced to name intermediate results, also solved by some sort of idiom bracket sugar, maybe together with the lambda case proposal? I would prefer both very much to the proposed (- action) syntax for the same reasons that e.g. Jules Bean nicely summarized. Cheers Ben ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: a regressive view of support for imperative programming in Haskell
On 8/9/07, Benjamin Franksen [EMAIL PROTECTED] wrote: Donn Cave wrote: (I have a soft spot for O'Haskell, but alas I must be nearly alone on that.) You are /not/ alone :-) I always found it very sad that O'Haskell and also its sucessor Timber (with all the good real-time stuff added) died the 'quick death' of most research languages. There is also RHaskell, which implements an O'Haskell-like system as a Haskell library. http://www.informatik.uni-freiburg.de/~wehr/haskell/ ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: a regressive view of support for imperative programming in Haskell
On Thu, Aug 09, 2007 at 08:45:14PM +0200, Benjamin Franksen wrote: David Roundy wrote: Several times since reading the beginning of this discussion I've wished I had the new syntax so I could write something like: do if predicateOnFileContents (- readFile foo) then ... instead of either do contents - readFile foo if predicateOnFileContents contents then ... or (as you'd prefer) readFile foo = \contents - if predicateOnFileContents contents then ... Isn't this problem, namely being forced to name intermediate results, also solved by some sort of idiom bracket sugar, maybe together with the lambda case proposal? I would prefer both very much to the proposed (- action) syntax for the same reasons that e.g. Jules Bean nicely summarized. I'm not familiar with the lambda case proposal, and don't know what you mean by idiom bracket sugar, but I haven't had an idea (or heard of one) that was nearly so elegant as the (- action) proposal, which neatly allows one to lift any existing pure function or syntactic construct (except lambda expressions?) into a monad. i.e. we don't need to define a separate 'if', 'case', etc, and we don't need liftM, liftM2, liftM3, liftM4andahalf, all of which are subsumed by a single pretty syntax. The only cost is that this syntax relies on the do notation, and thus makes the desugaring of that do notation slightly more complicated when used. -- David Roundy Department of Physics Oregon State University ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
