philosophy of Haskell

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
35 messages Options
12
Reply | Threaded
Open this post in threaded view
|

philosophy of Haskell

Michael Mossey
When I started to study Haskell, I was surprised that so much emphasis was
placed on simple things. Monads were introduced to me as basically a
wrapper, and a bind function that unwrapped something and wrapped something
else back up again. I didn't understand what the fuss was about. Later I
saw the amazing feats of expressiveness that were possible. I scratched my
head in confusion---"Wait, say that again?"

Here's a quote from Bertrand Russell about philosophy (read: Haskell). He's
actually being humorous, but it applies, in a way:

"The point of philosophy is to start with something so simple as not to
seem worth stating, and to end with something so paradoxical no one will
believe it."
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: philosophy of Haskell

Alberto G. Corona
I did`nt care about the underlying theory behind monads once I learn that the easy way to understand them is trough desugarization. Desugarize the "do" notation, after that, desugarize the >>= and >>  operators down to the function call notation and suddenly everithing lost its magic because it becomes clear that a haskell monad is a sugarization of plain  functional tricks.

But it seems that the trick is so productive because it comes from some fundamental properties of math, the reality, and maybe the human mind . Jost now I found this article: 


That definitively gives me the motivation to learn category theory seriously.

Alberto



2010/8/7 Michael Mossey <[hidden email]>
When I started to study Haskell, I was surprised that so much emphasis was placed on simple things. Monads were introduced to me as basically a wrapper, and a bind function that unwrapped something and wrapped something else back up again. I didn't understand what the fuss was about. Later I saw the amazing feats of expressiveness that were possible. I scratched my head in confusion---"Wait, say that again?"

Here's a quote from Bertrand Russell about philosophy (read: Haskell). He's actually being humorous, but it applies, in a way:

"The point of philosophy is to start with something so simple as not to seem worth stating, and to end with something so paradoxical no one will believe it."
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe


_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: philosophy of Haskell

jerzy.karczmarczuk
Alberto G. Corona  writes:

> (...) Desugarize the
> "do" notation, after that, desugarize the >>= and >>  operators down to the
> function call notation and suddenly everithing lost its magic because it
> becomes clear that a haskell monad is a sugarization of plain  functional
> tricks.

Yep.

But, BTW, could you tell me what was the result of the final desugarization
and the BASIC sense of the IO monad for you?

Jerzy Karczmarczuk
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: philosophy of Haskell

wren ng thornton
In reply to this post by Alberto G. Corona
Alberto G. Corona wrote:
> But it seems that the trick is so productive because it comes from some
> fundamental properties of math, the reality, and maybe the human mind . Jost
> now I found this article:
>
> Categorial Compositionality: A Category Theory Explanation for the
> Systematicity of Human
> Cognition<http://www.ploscompbiol.org/article/info:doi/10.1371/journal.pcbi.1000858?utm_source=feedburner&utm_medium=feed&utm_campaign=Feed:+ploscompbiol/NewArticles+(PLoS+Computational+Biology:+New+Articles)>

Ooh, that looks very shiny. Thanks for sharing :)

--
Live well,
~wren
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: philosophy of Haskell

Ertugrul Söylemez
In reply to this post by jerzy.karczmarczuk
[hidden email] wrote:

> Alberto G. Corona  writes:
>
> > (...) Desugarize the "do" notation, after that, desugarize the >>=
> > and >> operators down to the function call notation and suddenly
> > everithing lost its magic because it becomes clear that a haskell
> > monad is a sugarization of plain functional tricks.
>
> Yep.
>
> But, BTW, could you tell me what was the result of the final
> desugarization and the BASIC sense of the IO monad for you?

Example:

  do x <- getLine
     print (x+1)
     print (x+2)

There are various models.  One (the state monad model) of them would
desugar this to:

  \world0 ->
  let (x, world1) = getLine world0
      world2 = print (x+1) world1
      world3 = print (x+2) world2
  in world3

Another one (the EDSL model, which I personally prefer) would desugar it
to something as simple as this:

  GetLine `BindIO` \x ->
  Print (x+1) `BindIO`
  const (Print (x+2))

I wonder if there are more models for IO.


Greets,
Ertugrul


--
nightmare = unsafePerformIO (getWrongWife >>= sex)
http://ertes.de/


_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Re: philosophy of Haskell

Conal Elliott
There are various models.  One (the state monad model) of them would desugar this to:

 \world0 ->
 let (x, world1) = getLine world0
     world2 = print (x+1) world1
     world3 = print (x+2) world2
 in world3

Hi Ertugrul,

This state monad model does not really work for IO, since it fails to capture IO's concurrency (with non-deterministic interleaving).  I don't know whether/how the "EDSL model" you mention addresses concurrency or FFI.

So, maybe these models are models of something other (and much less expressive) than Haskell's IO.  Which re-raises Jerzy's question.

Regards,   - Conal

On Mon, Aug 9, 2010 at 10:38 PM, Ertugrul Soeylemez <[hidden email]> wrote:
[hidden email] wrote:

> Alberto G. Corona  writes:
>
> > (...) Desugarize the "do" notation, after that, desugarize the >>=
> > and >> operators down to the function call notation and suddenly
> > everithing lost its magic because it becomes clear that a haskell
> > monad is a sugarization of plain functional tricks.
>
> Yep.
>
> But, BTW, could you tell me what was the result of the final
> desugarization and the BASIC sense of the IO monad for you?

Example:

 do x <- getLine
    print (x+1)
    print (x+2)

There are various models.  One (the state monad model) of them would
desugar this to:

 \world0 ->
 let (x, world1) = getLine world0
     world2 = print (x+1) world1
     world3 = print (x+2) world2
 in world3

Another one (the EDSL model, which I personally prefer) would desugar it
to something as simple as this:

 GetLine `BindIO` \x ->
 Print (x+1) `BindIO`
 const (Print (x+2))

I wonder if there are more models for IO.


Greets,
Ertugrul


--
nightmare = unsafePerformIO (getWrongWife >>= sex)
http://ertes.de/


_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe


_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: philosophy of Haskell

Ertugrul Söylemez
Conal Elliott <[hidden email]> wrote:

> > There are various models.  One (the state monad model) of them would
> > desugar this to:
> >
> >  \world0 ->
> >  let (x, world1) = getLine world0
> >      world2 = print (x+1) world1
> >      world3 = print (x+2) world2
> >  in world3
>
> Hi Ertugrul,
>
> This state monad model does not really work for IO, since it fails to
> capture IO's concurrency (with non-deterministic interleaving).

Well, it does capture concurrency and FFI, but it has no explicit notion
for it.  In other words, concurrent threads and FFI calls are effects
like everything else, so the forkIO function just changes the world
state implicitly and that's it.


> I don't know whether/how the "EDSL model" you mention addresses
> concurrency or FFI.

Just like the state monad model.  This is not a weakness of the
interpretation, but of the IO monad itself, because it is quite a raw
and straightforward language for doing I/O.  Other approaches like
functional reactive programming may be better at capturing these things,
particularly the interactions between concurrent threads, at least for
specific applications.


> So, maybe these models are models of something other (and much less
> expressive) than Haskell's IO.  Which re-raises Jerzy's question.

Haskell's IO is flexible at the cost of being quite low level.  I think
to capture things like concurrency properly and explicitly you need a
richer sublanguage, maybe something based on the pi calculus.


Greets,
Ertugrul


--
nightmare = unsafePerformIO (getWrongWife >>= sex)
http://ertes.de/


_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Re: philosophy of Haskell

Conal Elliott


On Sat, Aug 14, 2010 at 9:27 AM, Ertugrul Soeylemez <[hidden email]> wrote:
Conal Elliott <[hidden email]> wrote:

> > There are various models.  One (the state monad model) of them would
> > desugar this to:
> >
> >  \world0 ->
> >  let (x, world1) = getLine world0
> >      world2 = print (x+1) world1
> >      world3 = print (x+2) world2
> >  in world3
>
> Hi Ertugrul,
>
> This state monad model does not really work for IO, since it fails to
> capture IO's concurrency (with non-deterministic interleaving).

Well, it does capture concurrency and FFI, but it has no explicit notion
for it.  In other words, concurrent threads and FFI calls are effects
like everything else, so the forkIO function just changes the world
state implicitly and that's it.

Consider that IO's concurrency means that something else can happen between printing x+1 and printing x+2, so that x+2 is *not* printed in world2, but rather in a world influenced outside of this thread.  Similarly, x+1 might not be printed in world1, and the getLine might not be executed in world0.  So World -> (a, World) is *not* expressive enough to explain Haskell-IO-style concurrency.

Do you see what I mean? 
 
> I don't know whether/how the "EDSL model" you mention addresses
> concurrency or FFI.

Just like the state monad model.  This is not a weakness of the
interpretation, but of the IO monad itself, because it is quite a raw
and straightforward language for doing I/O.

And the IO monad is what Jerzy asked about.  I'm pointing out that the state monad does not capture concurrency, and the "EDSL model" does not capture FFI.  (Really, it depends which "EDSL model".  I haven't seen one that can capture FFI.  And maybe not concurrency either.)
 Other approaches like
functional reactive programming may be better at capturing these things,
particularly the interactions between concurrent threads, at least for
specific applications.


> So, maybe these models are models of something other (and much less
> expressive) than Haskell's IO.  Which re-raises Jerzy's question.

Haskell's IO is flexible at the cost of being quite low level.  I think
to capture things like concurrency properly and explicitly you need a
richer sublanguage, maybe something based on the pi calculus.


Greets,
Ertugrul


--
nightmare = unsafePerformIO (getWrongWife >>= sex)
http://ertes.de/


_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe


_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Re: philosophy of Haskell

Bill Atkins-6
On Saturday Aug 14, 2010, at 12:50 AM, Conal Elliott wrote:

> And the IO monad is what Jerzy asked about.  I'm pointing out that the state monad does not capture concurrency, and the "EDSL model" does not capture FFI.  (Really, it depends which "EDSL model".  I haven't seen one that can capture FFI.  And maybe not concurrency either.)
>

So which model captures the way the IO monad works? _______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: philosophy of Haskell

Ertugrul Söylemez
In reply to this post by Conal Elliott
Conal Elliott <[hidden email]> wrote:

> On Sat, Aug 14, 2010 at 9:27 AM, Ertugrul Soeylemez <[hidden email]> wrote:
>
> > Conal Elliott <[hidden email]> wrote:
> >
> > > > There are various models.  One (the state monad model) of them
> > > > would desugar this to:
> > > >
> > > >  \world0 ->
> > > >  let (x, world1) = getLine world0
> > > >      world2 = print (x+1) world1
> > > >      world3 = print (x+2) world2
> > > >  in world3
> > >
> > > This state monad model does not really work for IO, since it fails
> > > to capture IO's concurrency (with non-deterministic interleaving).
> >
> > Well, it does capture concurrency and FFI, but it has no explicit
> > notion for it.  In other words, concurrent threads and FFI calls are
> > effects like everything else, so the forkIO function just changes
> > the world state implicitly and that's it.
>
> Consider that IO's concurrency means that something else can happen
> between printing x+1 and printing x+2, so that x+2 is *not* printed in
> world2, but rather in a world influenced outside of this thread.
> Similarly, x+1 might not be printed in world1, and the getLine might
> not be executed in world0.  So World -> (a, World) is *not* expressive
> enough to explain Haskell-IO-style concurrency.
>
> Do you see what I mean?

I don't agree.  A concurrent change is the effect of an IO action, not
of the thread.  For example if a concurrent thread writes to an MVar,
then that change becomes the effect of the next takeMVar, which gets
executed.  If a concurrent thread changes a file on disk, then that
changing becomes the effect of the next readFile, which reads the
changed file.

As said, the state monad model captures concurrency, but has no explicit
notion for it.  It captures it as an effect just like every other.


> > > I don't know whether/how the "EDSL model" you mention addresses
> > > concurrency or FFI.
> >
> > Just like the state monad model.  This is not a weakness of the
> > interpretation, but of the IO monad itself, because it is quite a
> > raw and straightforward language for doing I/O.
>
> And the IO monad is what Jerzy asked about.  I'm pointing out that the
> state monad does not capture concurrency, and the "EDSL model" does
> not capture FFI.  (Really, it depends which "EDSL model".  I haven't
> seen one that can capture FFI.  And maybe not concurrency either.)

The EDSL model is just an imperative language inside of Haskell.  It
captures thread launching as an action and concurrent changes as
actions.  Just as well it does capture FFI calls as actions, and so on.

Maybe you have some notion of "capturing" other than "being able to
express".  Maybe by "capturing" you mean being able to express the
particular concept/construct in the type system.  But then the IO monad
doesn't even capture writing to a file handle.  Or maybe you're talking
about elegance.  I don't really know.


Greets,
Ertugrul


--
nightmare = unsafePerformIO (getWrongWife >>= sex)
http://ertes.de/


_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Re: philosophy of Haskell

Conal Elliott
In reply to this post by Bill Atkins-6
On Sat, Aug 14, 2010 at 10:11 PM, Bill Atkins <[hidden email]> wrote:
On Saturday Aug 14, 2010, at 12:50 AM, Conal Elliott wrote:

> And the IO monad is what Jerzy asked about.  I'm pointing out that the state monad does not capture concurrency, and the "EDSL model" does not capture FFI.  (Really, it depends which "EDSL model".  I haven't seen one that can capture FFI.  And maybe not concurrency either.)
>

So which model captures the way the IO monad works?

I don't think anyone has given a denotational (functional-style) model for the meaning of IO.  As I wrote elsewhere:

IO carries the collective sins of our tribe, as the scapegoat did among the ancient Hebrews. Or, as Simon Peyton Jones expressed it, “The IO monad has become Haskell’s sin-bin. Whenever we don’t understand something, we toss it in the IO monad.” (From Wearing the hair shirt – A retrospective on Haskell.) Is it likely that we can then come along later and give a compelling and mathematically well-behaved notion of equality to our toxic waste pile? Or will it insist on behaving anti-sociably, as our own home-grown Toxic Avenger?


_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: philosophy of Haskell

Patai Gergely
In reply to this post by Michael Mossey
> I don't agree.  A concurrent change is the effect of an IO action, not
> of the thread.  For example if a concurrent thread writes to an MVar,
> then that change becomes the effect of the next takeMVar, which gets
> executed.  If a concurrent thread changes a file on disk, then that
> changing becomes the effect of the next readFile, which reads the
> changed file.
But that's exactly what the model cannot handle. Look at the following
snippet again:

>  let (x, world1) = getLine world0
>      world2 = print (x+1) world1

This clearly says that the world returned by getLine and the world
consumed by print is the same one, since the state monad model is pure,
therefore world1 is immutable. However, this is not true, since someone
else could have modified it in the meantime. The state monad can only
describe a single thread, but that's a non-existent situation in the
case of I/O, since the world keeps changing outside the program even if
the program itself is single-threaded.

Gergely

--
http://www.fastmail.fm - IMAP accessible web-mail

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: philosophy of Haskell

Ertugrul Söylemez
"Patai Gergely" <[hidden email]> wrote:

> > I don't agree.  A concurrent change is the effect of an IO action,
> > not of the thread.  For example if a concurrent thread writes to an
> > MVar, then that change becomes the effect of the next takeMVar,
> > which gets executed.  If a concurrent thread changes a file on disk,
> > then that changing becomes the effect of the next readFile, which
> > reads the changed file.
>
> But that's exactly what the model cannot handle. Look at the following
> snippet again:
>
> >  let (x, world1) = getLine world0
> >      world2 = print (x+1) world1
>
> This clearly says that the world returned by getLine and the world
> consumed by print is the same one, since the state monad model is
> pure, therefore world1 is immutable. However, this is not true, since
> someone else could have modified it in the meantime. The state monad
> can only describe a single thread, but that's a non-existent situation
> in the case of I/O, since the world keeps changing outside the program
> even if the program itself is single-threaded.

No.  As you say the world1 value is immutable, but that's not
contradictory.  If between 'getLine' and 'print' something was done by a
concurrent thread, then that change to the world is captured by 'print'.

See for example the following code:

  var <- newEmptyMVar
  forkIO $ threadDelay 1000000 >> putMVar var 15
  takeMVar var >>= print

Let's translate it:

  \world0 ->
  let (var, world1) = newEmptyMVar world0
      world2 = (forkIO $ threadDelay 1000000 >> putMVar var 15) world1
      (result, world3) = takeMVar var world2
  in print result world3

The subthread has the following code:

  \world0 ->
  let world1 = threadDelay 1000000 world0
  in putMVar var 15 world1

In the main thread the delay of one second and the change to the MVar is
/not/ an effect of another thread.  There is no notion of threads at
all.  It's a side effect of takeMVar.  The thread launched by forkIO
becomes part of the opaque world variable, which captures everything.
Otherwise we would have to say that the state monad model doesn't
capture user input either, because conceptually there is no difference
between a user typing something and a concurrent thread writing to
stdin.

IO has no specific notion for threads.  Threads are just side effects.
Things caused by threads is captured by normal IO actions like getLine
and takeMVar.  That's not a flaw of the interpretation as a state monad.
That's a flaw of the IO monad itself.


Greets,
Ertugrul


--
nightmare = unsafePerformIO (getWrongWife >>= sex)
http://ertes.de/


_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Re: philosophy of Haskell

Tillmann Rendel-4
Ertugrul Soeylemez wrote:
>>>  let (x, world1) = getLine world0
>>>      world2 = print (x+1) world1
>
> If between 'getLine' and 'print' something was done by a
> concurrent thread, then that change to the world is captured by 'print'.

But in a world passing interpretation of IO, print is supposed to be a
pure Haskell function. So the value world2 can only depend on the values
of print and world1, but not on the actions of some concurrent thread.

If print is not restricted to be a pure Haskell function, we don't need
the world passing in the first place.

   Tillmann
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re[2]: Re: philosophy of Haskell

Bulat Ziganshin-2
Hello Tillmann,

Sunday, August 15, 2010, 7:40:54 PM, you wrote:

> But in a world passing interpretation of IO, print is supposed to be a
> pure Haskell function. So the value world2 can only depend on the values
> of print and world1, but not on the actions of some concurrent thread.

the whole World includes any concurrent thread though ;)


--
Best regards,
 Bulat                            mailto:[hidden email]

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Re: philosophy of Haskell

Tillmann Rendel-4
Bulat Ziganshin wrote:
>> But in a world passing interpretation of IO, print is supposed to be a
>> pure Haskell function. So the value world2 can only depend on the values
>> of print and world1, but not on the actions of some concurrent thread.
>
> the whole World includes any concurrent thread though ;)

Oh I see. So given world1, print can simulate the behavior of the
concurrent thread to take it into account when constructing world2.
Since that simulation depends only on world1, print is still pure.

Does that mean that world passing *does* account for concurrency after all?

   Tillmann
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Re: philosophy of Haskell

Brandon S Allbery KF8NH
In reply to this post by Tillmann Rendel-4
-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1

On 8/15/10 11:40 , Tillmann Rendel wrote:
> But in a world passing interpretation of IO, print is supposed to be a pure
> Haskell function. So the value world2 can only depend on the values of print
> and world1, but not on the actions of some concurrent thread.
>
> If print is not restricted to be a pure Haskell function, we don't need the
> world passing in the first place.

I am confused by this discussion.  I originally thought some time back that
IO was about "world passing", but in fact it's just handing off a baton to
insure that a particular sequence of IO functions is executed in the
specified sequence and not reordered.  Nothing in the "baton" is intended to
represent the actual "state of the world", nor is anything said about
concurrent actions either in another thread of the current program or
elsewhere outside the program; only ordering of calls in the *current*
thread of execution.  (Which, hmm, implies that unsafePerformIO and
unsafeInterleaveIO are conceptually similar to forkIO.)

- --
brandon s. allbery     [linux,solaris,freebsd,perl]      [hidden email]
system administrator  [openafs,heimdal,too many hats]  [hidden email]
electrical and computer engineering, carnegie mellon university      KF8NH
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v2.0.10 (Darwin)
Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org/

iEYEARECAAYFAkxoGpUACgkQIn7hlCsL25U5SwCglJdUpOKbrFLmDO2X22nDq/no
UTIAoMllTt9LXOlblVaocbtVnRIx4dMY
=hCIW
-----END PGP SIGNATURE-----
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Re: philosophy of Haskell

Tillmann Rendel-4
Brandon S Allbery KF8NH wrote:
> I am confused by this discussion.  I originally thought some time back that
> IO was about "world passing", but in fact it's just handing off a baton to
> insure that a particular sequence of IO functions is executed in the
> specified sequence and not reordered.  Nothing in the "baton" is intended to
> represent the actual "state of the world", nor is anything said about
> concurrent actions either in another thread of the current program or
> elsewhere outside the program; only ordering of calls in the *current*
> thread of execution.

That explains how the IO monad forces side-effecting functions into a
specified sequence, but this discussion is about how to understand what
these side-effecting functions do in a *pure* framework. So the idea is
to regard, for example, putStr as a pure function from a world state to
a different world state, assuming that the world state contains a String
which represents the contents of the terminal. We could then implement
and understand putStr in pure Haskell:

   data World = World {
     terminal :: String
     ...
   }

   type IO a = World -> (World, a)

   putStr :: String -> World -> (World, ())
   putStr str world = (world {terminal = terminal world ++ str}, ())

The benefit of this point of view is that we can analyze the behavior of
putStr. For example, by equational reasoning, we could derive the
following equation:

   putStr s1 >> putStr s2   ==   putStr (s1 ++ s2)

It seems that we can account for more features of IO by adding more
fields to the World record. This discussion is about whether we can
account for *all* of IO this way.

   Tillmann
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Re: philosophy of Haskell

Brandon S Allbery KF8NH
-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1

On 8/15/10 13:27 , Tillmann Rendel wrote:

> Brandon S Allbery KF8NH wrote:
>> I am confused by this discussion.  I originally thought some time back that
>> IO was about "world passing", but in fact it's just handing off a baton to
>> insure that a particular sequence of IO functions is executed in the
>> specified sequence and not reordered.  Nothing in the "baton" is intended to
>> represent the actual "state of the world", nor is anything said about
>> concurrent actions either in another thread of the current program or
>> elsewhere outside the program; only ordering of calls in the *current*
>> thread of execution.
>
> That explains how the IO monad forces side-effecting functions into a
> specified sequence, but this discussion is about how to understand what
> these side-effecting functions do in a *pure* framework. So the idea is to

I think that *is* included in what I said, by negation:  it doesn't. Period.
 (As Conal observed.)  Trying to take the Haskell representation of IO as
the basis for a formal description of I/O actions is pretty much doomed from
the start; adding records or etc. will at best mask the symptoms.

- --
brandon s. allbery     [linux,solaris,freebsd,perl]      [hidden email]
system administrator  [openafs,heimdal,too many hats]  [hidden email]
electrical and computer engineering, carnegie mellon university      KF8NH
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v2.0.10 (Darwin)
Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org/

iEYEARECAAYFAkxoLP8ACgkQIn7hlCsL25W4QACgtJ4bz/W5fHVV/DxNgt8R39C8
ZkEAnj7rUnoUh4UQDFRdLeHKVmP8HLKS
=jnty
-----END PGP SIGNATURE-----
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: philosophy of Haskell

Patai Gergely
In reply to this post by Michael Mossey
> No.  As you say the world1 value is immutable, but that's not
> contradictory.  If between 'getLine' and 'print' something was done by a
> concurrent thread, then that change to the world is captured by 'print'.
Well, that's technically true, but it basically amounts to saying that
the 'model' of IO is itself. If I see 'print x', I don't really think of
an action that performs arbitrary side effects and prints x in the
process (unless some error prevents even that). Some notion of
compositionality is required, which would allow me to state how 'print
x' contributes to the changes of the world in a way that doesn't depend
on any context. Actions in the state monad are composable in that sense,
while the same doesn't apply to the IO monad when explained in terms of
state passing.

Gergely

--
http://www.fastmail.fm - The professional email service

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
12