Monad explanation

Tim Newsham

4 Feb 2009 4 Feb '09

12:41 p.m.

I put up a small Monad explanation (I wouldn't quite call it a tutorial): http://www.thenewsh.com/~newsham/haskell/monad.html The intent here is to is to have a short description of what a Monad is that is approachable by Haskell beginners or non- Haskell programmers who are looking for an intuitive definition but may not yet have the background or the inclination to jump into full tutorial to tackle the subject. Tim Newsham http://www.thenewsh.com/~newsham/

Show replies by date

Andrew Wagner

4 Feb 4 Feb

1:08 p.m.

This is nice and simple. My only concern is I'm not sure there's enough of a distinction between "Monad" and "State Monad". That is, I'm not sure it's clear enough that the way you're binding the small programs together in the initial example is only one way you could bind them together, and thus it's only one instance of Monad. On Wed, Feb 4, 2009 at 12:41 PM, Tim Newsham wrote:

...

I put up a small Monad explanation (I wouldn't quite call it a tutorial): http://www.thenewsh.com/~newsham/haskell/monad.html

The intent here is to is to have a short description of what a Monad is that is approachable by Haskell beginners or non- Haskell programmers who are looking for an intuitive definition but may not yet have the background or the inclination to jump into full tutorial to tackle the subject.

Tim Newsham http://www.thenewsh.com/~newsham/ _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

Tymur Porkuian

3:14 p.m.

For me, the key to understanding monads was that monad is "a value that know how to apply functions to itself". Or, more correctly, a container that knows how to apply functions to whatever is inside it. Before understanding this I read a lot of tutorials that presented monads as computations, IO sequencing structures, side effects encapsulation mechanisms, but it was a little bit too abstract, even though now

Tymur Porkuian

3:16 p.m.

Dan Piponi

3:20 p.m.

On Wed, Feb 4, 2009 at 12:16 PM, Tymur Porkuian wrote:

...

For me, the key to understanding monads was that monad is "a value that know how to apply functions to itself". Or, more correctly, a container that knows how to apply functions to whatever is inside it.

You've just described a Functor rather than a Monad. :-) -- Dan

Jonathan Cast

3:24 p.m.

On Wed, 2009-02-04 at 22:16 +0200, Tymur Porkuian wrote:

...

For me, the key to understanding monads was that monad is "a value that know how to apply functions to itself". Or, more correctly, a container that knows how to apply functions to whatever is inside it.

Close. (Monads are not `values' but types, but I'll let that slide). Remembering that all Haskell functions take a single argument, but we use currying to support an arbitrary number of arguments, we can arrange the Monad type class hierarchy like this: * Functor: A functor F allows a single function to be applied to a single F value. Multiple arguments (or none) are not supported; the definition of application does what you probably *don't* want if the function returns an F value itself. * Applicative: An applicative functor A allows a function of n arguments (for n >= 0) to be applied to n A values. However, the definition of application does what you probably *don't* want if the function returns an A value itself. * Monad: A monad M allows a function of n arguments (for n >= 0) to be applied to n M values; in addition, if the function returns an M value itself, you can combine that result with the arguments in a sensible way. jcc

Tymur Porkuian

4:13 p.m.

Actually, I understand these types in terms of containers that override standard method of function application for their contents. In fact, there may be no contents, or several items, or nothing at all, or something strange, but the container behaves like there is a value of some type inside it. In these terms: Maybe - container that may or may not contain something [a] - container that contains several values and applies function to all of them State - container that has some other "secondary" value in it. IO - container that remembers passed functions and later will ask user for value, then apply functions to it.

...

* Monad: A monad M allows a function of n arguments (for n >= 0) to be applied to n M values; in addition, if the function returns an M value itself, you can combine that result with the arguments in a sensible way.

Here, what does "sensible" mean? What do we override? Also, would it be right to say that Arrow is a container for functions that overrides function chaining?

Jonathan Cast

4:22 p.m.

On Wed, 2009-02-04 at 23:13 +0200, Tymur Porkuian wrote:

...

Actually, I understand these types in terms of containers that override standard method of function application for their contents.

Huh? You can't actually over-ride function application --- Haskell's built-in application always does exactly the same thing, at every type. You can, however, define new application-like operators that have other application-like behaviors. Haskell has a few of these: * return * (<$>) * (<*>) * (>>=)

...

In fact, there may be no contents, or several items, or nothing at all, or something strange, but the container behaves like there is a value of some type inside it.

In these terms: Maybe - container that may or may not contain something [a] - container that contains several values and applies function to all of them State - container that has some other "secondary" value in it. IO - container that remembers passed functions and later will ask user for value, then apply functions to it.

Nice but irrelevant. And I think your definition of IO is wrong.

...

...
* Monad: A monad M allows a function of n arguments (for n >= 0) to be applied to n M values; in addition, if the function returns an M value itself, you can combine that result with the arguments in a sensible way.

Here, what does "sensible" mean?

Sensible. As in, the definition of `join' in your monad can't be senseless, or irrelevant to the monad's intended use.

...

What do we override?

join

...

Also, would it be right to say that Arrow is a container for functions that overrides function chaining?

No. jcc

Tymur Porkuian

4:55 p.m.

...

Huh? You can't actually over-ride function application --- Haskell's built-in application always does exactly the same thing, at every type.

It's a metaphor. In every case container has its own method of applying functions to its contents - e.g. instead of "f x" we write "x fmap f".

...

You can, however, define new application-like operators that have other application-like behaviors. Haskell has a few of these:

* return * (<$>) * (<*>) * (>>=)

I know Haskell, that's not what I'm talking about. What I'm trying to do is to create a simple explanation for monads that doesn't involve neither mathematics nor "computation" metaphor.

Tymur Porkuian

4:56 p.m.

...

It's a metaphor. In every case container has its own method of applying functions to its contents - e.g. instead of "f x" we write "x fmap f".

x `fmap` f, of course

Tymur Porkuian

4:57 p.m.

...

x `fmap` f disregard that, f `fmap` x

Jonathan Cast

5:29 p.m.

On Wed, 2009-02-04 at 23:55 +0200, Tymur Porkuian wrote:

...

...
Huh? You can't actually over-ride function application --- Haskell's built-in application always does exactly the same thing, at every type.

...

It's a metaphor.

Oh, right. That one word that means `inaccurate way of putting things'! Invoking it solves everything! I maintain that my claims were entirely accurate. I maintain your claims are in-accurate and confusing.

...

In every case container has its own method of applying functions to its contents - e.g. instead of "f x" we write "x fmap f".

(NB. Typically only one of these will type-check; you know that, right?) jcc

Gregg Reynolds

4:20 p.m.

On Wed, Feb 4, 2009 at 11:41 AM, Tim Newsham wrote:

...

I put up a small Monad explanation (I wouldn't quite call it a tutorial): http://www.thenewsh.com/~newsham/haskell/monad.html http://www.thenewsh.com/%7Enewsham/haskell/monad.html

"The values of the IO monad are programs that do IO. " That's a fairly common representation, seems to work for lots of people, but it caused me no end of trouble. Values are mathematical objects; how, I asked myself, can they possibly /be/ programs that do IO (or actions, or computations, or <your metaphor here>)? It doesn't make sense, says I, so I must be misunderstanding something about "values"; better spend hours and hours researching and trying to figure this out. But it turns out the answer is simple: they can't. They're not actions, or IO procedures, or anything else other than plain old mathematical values, no different than '2' or Int -> Char. They happen to correspond in some way to the external physical behavior of the program, but that correspondence is an implementation detail beyond the scope of the formal (mathematical) semantics of the language. You don't even need monads for this part; they only enter the picture in order to provide ordered evaluation. In fact there really aren't any "monadic values", since a monad is pure morphism; the values at issue are "functoric values" if anything. It's (the implementation of) getChar the does the IO, not IO Char. So you could say that the monad itself is a purely mathematical structure that has the felicitous if accidental side effect of imposing temporal sequence on the physical interpretation (events) associated with the program. -g

Richard O'Keefe

9:18 p.m.

On 5 Feb 2009, at 10:20 am, Gregg Reynolds wrote:

...

That's a fairly common representation, seems to work for lots of people, but it caused me no end of trouble. Values are mathematical objects; how, I asked myself, can they possibly /be/ programs that do IO (or actions, or computations, or <your metaphor here>)? It doesn't make sense, says I,

without reference to the rest of your message, of course values can /be/ programs. One of the fundamental insights in programming is that (all) programs are values, which, in combination with the observation that some programs exist, means that some values are programs. Indeed, in the pure lambda calculus, _everything_ is a function (= program). If you don't like it put that way, say that values can be _names for_ programs, or that values can _be treated as_ programs by interpreters. I'd rather not get too far into White Knight territory, though.

Benjamin L.Russell

5 Feb 5 Feb

12:38 a.m.

On Thu, 5 Feb 2009 15:18:09 +1300, "Richard O'Keefe" wrote:

...

On 5 Feb 2009, at 10:20 am, Gregg Reynolds wrote:

...
That's a fairly common representation, seems to work for lots of people, but it caused me no end of trouble. Values are mathematical objects; how, I asked myself, can they possibly /be/ programs that do IO (or actions, or computations, or <your metaphor here>)? It doesn't make sense, says I,

without reference to the rest of your message, of course values can /be/ programs. One of the fundamental insights in programming is that (all) programs are values, which, in combination with the observation that some programs exist, means that some values are programs. Indeed, in the pure lambda calculus, _everything_ is a function (= program).

Indeed. Perhaps at least part of this confusion is caused by a difference in style of thinking between the functional and imperative programming paradigms; in functional programming, functions are first-class values, so they are treated just like any other values. Therefore, functional programs are values. This style of thinking contrasts with that of imperative programming, where programs are typically considered to be composed of statements which change global state when executed (see "Functional programming - HaskellWiki: 1 What is functional programming?" at http://www.haskell.org/haskellwiki/Functional_programming#What_is_functional... .

...

If you don't like it put that way, say that values can be _names for_ programs, or that values can _be treated as_ programs by interpreters. I'd rather not get too far into White Knight territory, though.

Actually, I have a question myself on this issue. I had intended to give an example of a self-referential program that modifies itself to illustrate programs as first-class values, but then I just discovered that it seems that Haskell doesn't support reflection (see http://en.wikipedia.org/wiki/Reflection_(computer_science)). In particular, I just came across the following archived post in Haskell-Cafe, "Re: [Haskell-cafe] To yi or not to yi, is this really the question? A plea for a cooperative, ubiquitous, distributed integrated development system.," dated "Mon, 18 Jun 2007 14:05:53 -0700" (see http://www.mail-archive.com/haskell-cafe@haskell.org/msg25257.html), in which Pasqualino 'Titto' Assini wrote as follows:

...

Most languages, even Java, have a reflection capability to dynamically inspect an object. It is surprising that Haskell doesn't offer it.

In the same thread, Claus Reinke, in his response, dated "Mon, 18 Jun 2007 15:45:50 -0700" (see http://www.mail-archive.com/haskell-cafe@haskell.org/msg25270.html), wrote as follows:

...

...
Most languages, even Java, have a reflection capability to dynamically inspect an object. It is surprising that Haskell doesn't offer it.

it has to be done with care, or it will invalidate *all* your nice reasoning about haskell programs. random example

reify (f . g) == [| f . g |] =/= [| \x-> f (g x) |] == reify (\x-> f (g x))

I tried looking up "self-reference" on HaskellWiki, but my search did not result in any hits. Is it possible to write a self-referential function in Haskell that modifies itself? My intuition is that this would violate referential transparency, so it is probably not possible, but as long as the program is only allowed to reference itself without actually modifying itself, then there should be a way. Alternatively, it should be possible for a Haskell program to create a copy of itself, and then to modify that copy, as long as referential transparency is not violated. To what extent are self-reference and reflection supported n Haskell? -- Benjamin L. Russell -- Benjamin L. Russell / DekuDekuplex at Yahoo dot com http://dekudekuplex.wordpress.com/ Translator/Interpreter / Mobile: +011 81 80-3603-6725 "Furuike ya, kawazu tobikomu mizu no oto." -- Matsuo Basho^

Max Rabkin

12:43 a.m.

On Wed, Feb 4, 2009 at 9:38 PM, Benjamin L. Russell wrote:

...

Is it possible to write a self-referential function in Haskell that modifies itself?

Is it possible to write *any* kind of function in Haskell that modifies *anything*? --Max

Benjamin L.Russell

4:38 a.m.

On Wed, 4 Feb 2009 21:43:04 -0800, Max Rabkin wrote:

...

On Wed, Feb 4, 2009 at 9:38 PM, Benjamin L. Russell wrote:

...
Is it possible to write a self-referential function in Haskell that modifies itself?

Is it possible to write *any* kind of function in Haskell that modifies *anything*?

While trying to research this issue, I came across a relevant archived thread in Haskell-Cafe, entitled "[Haskell-cafe] haskell and reflection," started by Greg Meredith, dated "Tue, 11 Sep 2007 07:09:22 -0700" (see http://www.mail-archive.com/haskell-cafe@haskell.org/msg29882.html), which at first had me worried. Specifically, Greg wrote as follows:

...

Am i wrong in my assessment that the vast majority of reflective machinery is missing from Haskell? Specifically,

- there is no runtime representation of type available for programmatic representation - there is no runtime representation of the type-inferencing or checking machinery - there is no runtime representation of the evaluation machinery - there is no runtime representation of the lexical or parsing machinery

However, I was somewhat relieved to find that Haskell apparently does support, in at least one GHC extension to Haskell, a limited form of reflection. In the same thread, Reinier Lamers, in his response, dated "Tue, 11 Sep 2007 13:08:38 -0700" (see http://www.mail-archive.com/haskell-cafe@haskell.org/msg29898.html), wrote as follows:

...

Op 11-sep-2007, om 18:43 heeft Greg Meredith het volgende geschreven:

[...]

Template Haskell [1] is a system that lets you write programs that get executed at *compile time*, and that produce parts of the Haskell program to be compiled by manipulating a representation of the program as structured data. It's a form of reflection restricted to compile time, if you'd ask me.

[...]

[1] http://www.haskell.org/haskellwiki/Template_Haskell

According to the site referenced by the above-mentioned link,

...

Template Haskell is an extension to Haskell 98 that allows you to do type-safe compile-time meta-programming, with Haskell both as the manipulating language and the language being manipulated.

This site is even referenced on the site for "The Meta-Programming Project" (see http://www.infosun.fim.uni-passau.de/cl/metaprog/index.php3), as follows:

...

Languages which we are using for meta-programming

* Template Haskell, permits analysis of object programs

Additionally, Don Stewart, in an earlier post in the same thread, dated "Thu, 13 Sep 2007 11:36:11 -0700" (see http://www.mail-archive.com/haskell-cafe@haskell.org/msg30009.html), wrote as follows:

...

lgreg.meredith:

...
Haskellians,

Am i wrong in my assessment that the vast majority of reflective machinery is missing from Haskell? Specifically,

* there is no runtime representation of type available for programmatic representation

...
* there is no runtime representation of the type-inferencing or checking machinery

...
* there is no runtime representation of the evaluation machinery

...
* there is no runtime representation of the lexical or parsing machinery

So there is library support for all of this, in various forms:

* lexer, parser, type checker, evaluator: ghc-api hs-plugins

* lexer, parser, pretty printer many parser libs (Language.Haskell, Template Haskell)

* runtime type representation Data.Typeable

* reflecting code to data: Data.Generics

As a sidenote, I discovered an interesting post and associated paper by Lauri Alanko, who in a post in the same thread, dated "Tue, 11 Sep 2007 10:12:09 -0700" (see http://www.mail-archive.com/haskell-cafe@haskell.org/msg29895.html), responded that while both structural and procedural reflection are possible in Haskell, because of static typing, type safety is nevertheless an issue:

...

On Tue, Sep 11, 2007 at 07:33:54AM -0700, Greg Meredith wrote:

...
Our analysis suggested the following breakdown

- Structural reflection -- all data used in the evaluation of programs has a programmatic representation - Procedural reflection -- all execution machinery used in the evaluation of programs has a programmatic representation

[...]

As for Haskell, there are various tools for both (at least Data.Typeable and hs-plugins), but neither are truly type-safe: it is possible to write code that uses these libraries and type-checks, yet crashes. Static typing makes reflection very difficult to support safely.

...

You might be interested in my MS thesis, where I explored these issues in some more length: http://www.cs.helsinki.fi/u/lealanko/alanko04types.pdf

This thesis is entitled "Types and Reflection" (see the above-mentioned URL), and summarizes the problem as follows (see p. 1):

...

This thesis is about reflection in typed programming languages. The central idea of this work, the thesis proper, can be summarized in three points: . Typed reflection is a good thing. . It has not yet been done properly. . It is nevertheless possible.

The basic problem with reflection in a statically typed language seems to be that "reflection wreaks havoc to the basic assumptions that type systems are based on" (see p. 11). Specifically, he explains as follows (see p. 38):

...

[A] type system verifies or infers universal properties about all possible executions of a program by making a context-sensitive syntactic analysis of the program’s structure. Usually this is possible because the computational rules for executing the program are simple, tractable and most importantly syntax-directed: the evaluation of each expression proceeds in a predictable fashion that is determined mostly by its syntactic form and only to a limited extent by run-time state. For each expression there are certain invariants that always hold for its evaluation, and these invariants can be expressed in the expression’s type.

In practice this means that we can prove the soundness of a type system with structural induction over the terms, using the dynamic semantics of the language to show that the evaluation of each expression will yield a well-typed result.

In the presence of reflective operations this mode of reasoning no longer works. The reason is that the effects of all primitive expressions on computational structures are no longer simple and tractable: an absorption operation turns an arbitrary run-time value into a computational structure, and there are therefore no simple invariants about the operation’s behavior.

This is of course an inherent property of reflection. Its idea, after all, is to allow the program more freedom at run-time instead of completely predefining its behavior when the program is written. Yet it is still a rarely used feature and it seems unreasonable that it should make static typing completely unattainable. Thankfully, this proves not to be the case.

In Greg Meredith's solution, he writes as follows (see p. 42):

...

[T]here is a tradeoff to be made between static safety and dynamic flexibility. It turns out that it is possible to do quite sophisticated run-time code manipulation while still retaining fully static safety guarantees both of the original code and the generated code.

In Section 8.3: "Dynamics in Haskell," Meredith elucidates as follows (see p. 62):

...

The language Haskell [H98] has a powerful type system, but the standard version of the language has no support for run-time type operations. However, there is a dynamics library that has for a long time been included in many implementations [LPJ03, Section 8]. The library provides a datatype Dynamic and some machinery for injecting values of different types into it and for extracting them out from it. Unfortunately, the user of the library is required to obey certain programming conventions, and if they are not followed, it is very easy to write code that breaks type safety. Moreover, the library provides only limited support for dynamics. For instance, it is not possible to inject polymorphic functions into a Dynamic.

More recently, Cheney and Hinze [CH02a] and Baars and Swierstra [BS02] have developed more flexible and type-safe frameworks for representing type information at runtime in Haskell. In fact, dynamic values are only one of the possible applications of the frameworks.

Cheney and Hinze's system is then described in more detail. Meredith then concludes as follows (see p. 63):

...

The above system is quite remarkable. The type Rep [tau] bridges the gap between static and dynamic type information while remaining completely type-safe even internally. Indeed, the type representations are very much like reified types. They can be synthesized and analyzed, and the isomorphisms allow a kind of absorption: conversion from run-time to compile-time type information.

Some problems relating to the need for programmer cooperation, the treatment of new named datatypes, and lack of full reflexivity are then described. Nevertheless, Meredith summarizes as follows (see p. 64):

...

Nevertheless, these "lightweight dynamics" are surprisingly powerful, considering that they can be implemented in a statically typed language without extending the type system. For example, Baars and Swierstra demonstrate how to write a type-safe eval function for a simple language so that all type checking is done before the code is evaluated. Although this is not full reflection due to the simplicity of the object language, the result is still encouraging. For one thing, at least now a type can be pretty-printed even without the presence of a value of that type.

Apparently, there is hope for reflection in Haskell with such libraries. What would be especially interesting would be a specific example of a type-safe Haskell program that could modify itself at runtime. If anyone has any examples to cite, I would be very interested in reading about them in this thread. -- Benjamin L. Russell -- Benjamin L. Russell / DekuDekuplex at Yahoo dot com http://dekudekuplex.wordpress.com/ Translator/Interpreter / Mobile: +011 81 80-3603-6725 "Furuike ya, kawazu tobikomu mizu no oto." -- Matsuo Basho^

Daryoush Mehrtash

5:23 a.m.

Can someone compare/contrast functions and computation? thanks daryoush On Thu, Feb 5, 2009 at 1:38 AM, Benjamin L. Russell wrote:

...

On Wed, 4 Feb 2009 21:43:04 -0800, Max Rabkin wrote:

...
On Wed, Feb 4, 2009 at 9:38 PM, Benjamin L. Russell wrote:

...
Is it possible to write a self-referential function in Haskell that modifies itself?

Is it possible to write *any* kind of function in Haskell that modifies *anything*?

While trying to research this issue, I came across a relevant archived thread in Haskell-Cafe, entitled "[Haskell-cafe] haskell and reflection," started by Greg Meredith, dated "Tue, 11 Sep 2007 07:09:22 -0700" (see http://www.mail-archive.com/haskell-cafe@haskell.org/msg29882.html), which at first had me worried. Specifically, Greg wrote as follows:

...
Am i wrong in my assessment that the vast majority of reflective machinery is missing from Haskell? Specifically,

- there is no runtime representation of type available for programmatic representation - there is no runtime representation of the type-inferencing or checking machinery - there is no runtime representation of the evaluation machinery - there is no runtime representation of the lexical or parsing machinery

However, I was somewhat relieved to find that Haskell apparently does support, in at least one GHC extension to Haskell, a limited form of reflection. In the same thread, Reinier Lamers, in his response, dated "Tue, 11 Sep 2007 13:08:38 -0700" (see http://www.mail-archive.com/haskell-cafe@haskell.org/msg29898.html), wrote as follows:

...
Op 11-sep-2007, om 18:43 heeft Greg Meredith het volgende geschreven:

[...]

Template Haskell [1] is a system that lets you write programs that get executed at *compile time*, and that produce parts of the Haskell program to be compiled by manipulating a representation of the program as structured data. It's a form of reflection restricted to compile time, if you'd ask me.

[...]

[1] http://www.haskell.org/haskellwiki/Template_Haskell

According to the site referenced by the above-mentioned link,

...
Template Haskell is an extension to Haskell 98 that allows you to do type-safe compile-time meta-programming, with Haskell both as the manipulating language and the language being manipulated.

This site is even referenced on the site for "The Meta-Programming Project" (see http://www.infosun.fim.uni-passau.de/cl/metaprog/index.php3), as follows:

...
Languages which we are using for meta-programming

* Template Haskell, permits analysis of object programs

Additionally, Don Stewart, in an earlier post in the same thread, dated "Thu, 13 Sep 2007 11:36:11 -0700" (see http://www.mail-archive.com/haskell-cafe@haskell.org/msg30009.html), wrote as follows:

...
...
Haskellians,

Am i wrong in my assessment that the vast majority of reflective machinery is missing from Haskell? Specifically,

* there is no runtime representation of type available for

lgreg.meredith: programmatic

...
representation

...
* there is no runtime representation of the type-inferencing or

checking

...
machinery

...
* there is no runtime representation of the evaluation machinery

...
* there is no runtime representation of the lexical or parsing

machinery

So there is library support for all of this, in various forms:

* lexer, parser, type checker, evaluator: ghc-api hs-plugins

* lexer, parser, pretty printer many parser libs (Language.Haskell, Template Haskell)

* runtime type representation Data.Typeable

* reflecting code to data: Data.Generics

As a sidenote, I discovered an interesting post and associated paper by Lauri Alanko, who in a post in the same thread, dated "Tue, 11 Sep 2007 10:12:09 -0700" (see http://www.mail-archive.com/haskell-cafe@haskell.org/msg29895.html), responded that while both structural and procedural reflection are possible in Haskell, because of static typing, type safety is nevertheless an issue:

...
...
Our analysis suggested the following breakdown

- Structural reflection -- all data used in the evaluation of

On Tue, Sep 11, 2007 at 07:33:54AM -0700, Greg Meredith wrote: programs

...
has a programmatic representation - Procedural reflection -- all execution machinery used in the evaluation of programs has a programmatic representation

[...]

As for Haskell, there are various tools for both (at least Data.Typeable and hs-plugins), but neither are truly type-safe: it is possible to write code that uses these libraries and type-checks, yet crashes. Static typing makes reflection very difficult to support safely.

...
You might be interested in my MS thesis, where I explored these issues in some more length: http://www.cs.helsinki.fi/u/lealanko/alanko04types.pdf

This thesis is entitled "Types and Reflection" (see the above-mentioned URL), and summarizes the problem as follows (see p. 1):

...
This thesis is about reflection in typed programming languages. The central idea of this work, the thesis proper, can be summarized in three points: . Typed reflection is a good thing. . It has not yet been done properly. . It is nevertheless possible.

The basic problem with reflection in a statically typed language seems to be that "reflection wreaks havoc to the basic assumptions that type systems are based on" (see p. 11). Specifically, he explains as follows (see p. 38):

...
[A] type system verifies or infers universal properties about all possible executions of a program by making a context-sensitive syntactic analysis of the program's structure. Usually this is possible because the computational rules for executing the program are simple, tractable and most importantly syntax-directed: the evaluation of each expression proceeds in a predictable fashion that is determined mostly by its syntactic form and only to a limited extent by run-time state. For each expression there are certain invariants that always hold for its evaluation, and these invariants can be expressed in the expression's type.

In practice this means that we can prove the soundness of a type system with structural induction over the terms, using the dynamic semantics of the language to show that the evaluation of each expression will yield a well-typed result.

In the presence of reflective operations this mode of reasoning no longer works. The reason is that the effects of all primitive expressions on computational structures are no longer simple and tractable: an absorption operation turns an arbitrary run-time value into a computational structure, and there are therefore no simple invariants about the operation's behavior.

This is of course an inherent property of reflection. Its idea, after all, is to allow the program more freedom at run-time instead of completely predefining its behavior when the program is written. Yet it is still a rarely used feature and it seems unreasonable that it should make static typing completely unattainable. Thankfully, this proves not to be the case.

In Greg Meredith's solution, he writes as follows (see p. 42):

...
[T]here is a tradeoff to be made between static safety and dynamic flexibility. It turns out that it is possible to do quite sophisticated run-time code manipulation while still retaining fully static safety guarantees both of the original code and the generated code.

In Section 8.3: "Dynamics in Haskell," Meredith elucidates as follows (see p. 62):

...
The language Haskell [H98] has a powerful type system, but the standard version of the language has no support for run-time type operations. However, there is a dynamics library that has for a long time been included in many implementations [LPJ03, Section 8]. The library provides a datatype Dynamic and some machinery for injecting values of different types into it and for extracting them out from it. Unfortunately, the user of the library is required to obey certain programming conventions, and if they are not followed, it is very easy to write code that breaks type safety. Moreover, the library provides only limited support for dynamics. For instance, it is not possible to inject polymorphic functions into a Dynamic.

More recently, Cheney and Hinze [CH02a] and Baars and Swierstra [BS02] have developed more flexible and type-safe frameworks for representing type information at runtime in Haskell. In fact, dynamic values are only one of the possible applications of the frameworks.

Cheney and Hinze's system is then described in more detail. Meredith then concludes as follows (see p. 63):

...
The above system is quite remarkable. The type Rep [tau] bridges the gap between static and dynamic type information while remaining completely type-safe even internally. Indeed, the type representations are very much like reified types. They can be synthesized and analyzed, and the isomorphisms allow a kind of absorption: conversion from run-time to compile-time type information.

Some problems relating to the need for programmer cooperation, the treatment of new named datatypes, and lack of full reflexivity are then described. Nevertheless, Meredith summarizes as follows (see p. 64):

...
Nevertheless, these "lightweight dynamics" are surprisingly powerful, considering that they can be implemented in a statically typed language without extending the type system. For example, Baars and Swierstra demonstrate how to write a type-safe eval function for a simple language so that all type checking is done before the code is evaluated. Although this is not full reflection due to the simplicity of the object language, the result is still encouraging. For one thing, at least now a type can be pretty-printed even without the presence of a value of that type.

Apparently, there is hope for reflection in Haskell with such libraries.

What would be especially interesting would be a specific example of a type-safe Haskell program that could modify itself at runtime. If anyone has any examples to cite, I would be very interested in reading about them in this thread.

-- Benjamin L. Russell -- Benjamin L. Russell / DekuDekuplex at Yahoo dot com http://dekudekuplex.wordpress.com/ Translator/Interpreterhttp://dekudekuplex.wordpress.com/%0ATranslator/Interpreter/ Mobile: +011 81 80-3603-6725 "Furuike ya, kawazu tobikomu mizu no oto." -- Matsuo Basho^

_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

Gregg Reynolds

11:08 a.m.

On Wed, Feb 4, 2009 at 8:18 PM, Richard O'Keefe wrote:

...

On 5 Feb 2009, at 10:20 am, Gregg Reynolds wrote:

...
That's a fairly common representation, seems to work for lots of people, but it caused me no end of trouble. Values are mathematical objects; how, I asked myself, can they possibly /be/ programs that do IO (or actions, or computations, or <your metaphor here>)? It doesn't make sense, says I,

without reference to the rest of your message, of course values can /be/ programs.

Not "programs", but "programs that do IO". The point of the idiom is that there's an external side effect involved. What sticks in my craw is that "a mathematical value with a non-mathematical side effect" is, well, non-mathematical and possibly nonsensical. I know it works for some (most?) people, but for me it lacks Geometry and Theology. -g

David Leimbach

2:20 p.m.

2009/2/5 Gregg Reynolds

...

On Wed, Feb 4, 2009 at 8:18 PM, Richard O'Keefe wrote:

...
On 5 Feb 2009, at 10:20 am, Gregg Reynolds wrote:

...
That's a fairly common representation, seems to work for lots of people, but it caused me no end of trouble. Values are mathematical objects; how, I asked myself, can they possibly /be/ programs that do IO (or actions, or computations, or <your metaphor here>)? It doesn't make sense, says I,

without reference to the rest of your message, of course values can /be/ programs.

Not "programs", but "programs that do IO". The point of the idiom is that there's an external side effect involved. What sticks in my craw is that "a mathematical value with a non-mathematical side effect" is, well, non-mathematical and possibly nonsensical. I know it works for some (most?) people, but for me it lacks Geometry and Theology.

-g

I think the point of the Monad is that it works as a container of stuff, that still allows mathematically pure things to happen, while possibly having some opaque "other stuff" going on. If you have a monadic add operation, and a Monad of some kind that "Contains an Integer", you can call the Monadic add operation on a pair of those monads, and some of the other monadic gluey-stuff that happens in between can combine the "other stuff" in specific ways, depending on how the Monad is defined. If it's the identity monad, it might not be that interesting, but if it's a writer monad, it might log things that are going on. m 1 + m 2 = m3, but what happened inside the "m" is entirely up to how that "m" is defined. Does that make it a little easier to understand? IO could have happened in the "m", but there's still a pure peace.... sometimes :-) (there's nothing stopping you reading an integer from the keyboard and returning it to totally break down that analogy I suppose). At least this is how I like to think of Monads. If you want more guarantees about operations, keep them pure, and then you only have to really scrutinize the monad-using bits to see where your program can get screwy. I realize that might not make the mathematician in you feel tons better, but *shrug*. Dave

...

_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

Andrew Wagner

2:25 p.m.

...

I think the point of the Monad is that it works as a container of stuff,

...
that still allows mathematically pure things to happen, while possibly having some opaque "other stuff" going on.

This at least sounds, very wrong, even if it's not. Monads are not impure. IO is, but it's only _one_ instance of Monad. All others, as far as I know, are pure. It's just that the bind operation allows you to hide the stuff you don't want to have to worry about, that should happen every time you compose two monadic actions.

Miguel Mitrofanov

2:41 p.m.

Ahem... WHAT??? IO monad is impure??? What do you mean? On 5 Feb 2009, at 22:25, Andrew Wagner wrote:

...

I think the point of the Monad is that it works as a container of stuff, that still allows mathematically pure things to happen, while possibly having some opaque "other stuff" going on.

This at least sounds, very wrong, even if it's not. Monads are not impure. IO is, but it's only _one_ instance of Monad. All others, as far as I know, are pure. It's just that the bind operation allows you to hide the stuff you don't want to have to worry about, that should happen every time you compose two monadic actions. _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

David Leimbach

3:21 p.m.

On Thu, Feb 5, 2009 at 11:25 AM, Andrew Wagner wrote:

...

I think the point of the Monad is that it works as a container of stuff,

...
...
that still allows mathematically pure things to happen, while possibly having some opaque "other stuff" going on.

This at least sounds, very wrong, even if it's not. Monads are not impure. IO is, but it's only _one_ instance of Monad. All others, as far as I know, are pure. It's just that the bind operation allows you to hide the stuff you don't want to have to worry about, that should happen every time you compose two monadic actions.

Well all I can tell you is that I can have (IO Int) in a function as a return, and the function is not idempotent in terms of the "stuff" inside IO being the same. Sounds impure to me.

Andrew Wagner

3:25 p.m.

On Thu, Feb 5, 2009 at 3:21 PM, David Leimbach wrote:

...

Well all I can tell you is that I can have (IO Int) in a function as a return, and the function is not idempotent in terms of the "stuff" inside IO being the same.

Sounds impure to me.

Right, thus IO is impure. but as long as the function that returns the IO Int returns the same IO Int every time you provide the same input, it's pure.

David Leimbach

3:27 p.m.

On Thu, Feb 5, 2009 at 12:25 PM, Andrew Wagner wrote:

...

On Thu, Feb 5, 2009 at 3:21 PM, David Leimbach wrote:

...
Well all I can tell you is that I can have (IO Int) in a function as a return, and the function is not idempotent in terms of the "stuff" inside IO being the same.

Sounds impure to me.

Right, thus IO is impure. but as long as the function that returns the IO Int returns the same IO Int every time you provide the same input, it's pure.

Ah yes I see your point... that's true absolutely.

Jonathan Cast

3:27 p.m.

On Thu, 2009-02-05 at 12:21 -0800, David Leimbach wrote:

...

On Thu, Feb 5, 2009 at 11:25 AM, Andrew Wagner wrote: I think the point of the Monad is that it works as a container of stuff, that still allows mathematically pure things to happen, while possibly having some opaque "other stuff" going on.

...

This at least sounds, very wrong, even if it's not. Monads are not impure. IO is, but it's only _one_ instance of Monad. All others, as far as I know, are pure. It's just that the bind operation allows you to hide the stuff you don't want to have to worry about, that should happen every time you compose two monadic actions.

...

Well all I can tell you is that I can have (IO Int) in a function as a return, and the function is not idempotent in terms of the "stuff" inside IO being the same.

Sure it's the same.

...

cmp /bin/cat /bin/cat cp /bin/cat ~ cmp /bin/cat ~/cat

Pretty much the same, anyway. jcc

David Leimbach

4:01 p.m.

On Thu, Feb 5, 2009 at 12:27 PM, Jonathan Cast wrote:

...

On Thu, 2009-02-05 at 12:21 -0800, David Leimbach wrote:

...
On Thu, Feb 5, 2009 at 11:25 AM, Andrew Wagner wrote: I think the point of the Monad is that it works as a container of stuff, that still allows mathematically pure things to happen, while possibly having some opaque "other stuff" going on.

...
This at least sounds, very wrong, even if it's not. Monads are not impure. IO is, but it's only _one_ instance of Monad. All others, as far as I know, are pure. It's just that the bind operation allows you to hide the stuff you don't want to have to worry about, that should happen every time you compose two monadic actions.

...
Well all I can tell you is that I can have (IO Int) in a function as a return, and the function is not idempotent in terms of the "stuff" inside IO being the same.

Sure it's the same.

...
cmp /bin/cat /bin/cat cp /bin/cat ~ cmp /bin/cat ~/cat

Pretty much the same, anyway.

jcc

So if IO represents a program that when executed interacts with the world's state, is it safe to say that when I return (State Int Int), that I'm returning a "State program"? That'd make sense as it really does look like we force the State to be evaluated with runState, evalState or execState. The only difference with IO then is that to get IO programs to run, you have to do it inside another IO program. I hope I'm not making this worse! :-)

Jonathan Cast

5:38 p.m.

On Thu, 2009-02-05 at 13:01 -0800, David Leimbach wrote:

...

On Thu, Feb 5, 2009 at 12:27 PM, Jonathan Cast wrote:

On Thu, 2009-02-05 at 12:21 -0800, David Leimbach wrote: > > > On Thu, Feb 5, 2009 at 11:25 AM, Andrew Wagner > wrote: > I think the point of the Monad is that it > works as a container of stuff, that still > allows mathematically pure things to happen, > while possibly having some opaque "other > stuff" going on.

> This at least sounds, very wrong, even if it's not. Monads > are not impure. IO is, but it's only _one_ instance of Monad. > All others, as far as I know, are pure. It's just that the > bind operation allows you to hide the stuff you don't want to > have to worry about, that should happen every time you compose > two monadic actions.

...

> Well all I can tell you is that I can have (IO Int) in a function as a > return, and the function is not idempotent in terms of the "stuff" > inside IO being the same.

Sure it's the same.

> cmp /bin/cat /bin/cat > cp /bin/cat ~ > cmp /bin/cat ~/cat >

Pretty much the same, anyway.

...

So if IO represents a program that when executed interacts with the world's state, is it safe to say that when I return (State Int Int), that I'm returning a "State program"?

I won't object to it. Othe people might, though.

...

That'd make sense as it really does look like we force the State to be evaluated with runState, evalState or execState.

...

The only difference with IO then is that to get IO programs to run, you have to do it inside another IO program.

Meh. Combining IO sub-programs into larger programs doesn't really `get them to run'. Better to say that an IO value is meaningful only to the computer, and not mathematically (denotationally) useful. jcc

David Leimbach

6:52 p.m.

On Thu, Feb 5, 2009 at 2:38 PM, Jonathan Cast wrote:

...

On Thu, 2009-02-05 at 13:01 -0800, David Leimbach wrote:

...
On Thu, Feb 5, 2009 at 12:27 PM, Jonathan Cast wrote:

On Thu, 2009-02-05 at 12:21 -0800, David Leimbach wrote: > > > On Thu, Feb 5, 2009 at 11:25 AM, Andrew Wagner > wrote: > I think the point of the Monad is that it > works as a container of stuff, that still > allows mathematically pure things to happen, > while possibly having some opaque "other > stuff" going on.

> This at least sounds, very wrong, even if it's not. Monads > are not impure. IO is, but it's only _one_ instance of Monad. > All others, as far as I know, are pure. It's just that the > bind operation allows you to hide the stuff you don't want to > have to worry about, that should happen every time you compose > two monadic actions.

...
> Well all I can tell you is that I can have (IO Int) in a function as a > return, and the function is not idempotent in terms of the "stuff" > inside IO being the same.

Sure it's the same.

> cmp /bin/cat /bin/cat > cp /bin/cat ~ > cmp /bin/cat ~/cat >

Pretty much the same, anyway.

...
So if IO represents a program that when executed interacts with the world's state, is it safe to say that when I return (State Int Int), that I'm returning a "State program"?

I won't object to it. Othe people might, though.

...
That'd make sense as it really does look like we force the State to be evaluated with runState, evalState or execState.

...
The only difference with IO then is that to get IO programs to run, you have to do it inside another IO program.

Meh. Combining IO sub-programs into larger programs doesn't really `get them to run'. Better to say that an IO value is meaningful only to the computer, and not mathematically (denotationally) useful.

jcc

All Haskell programs start as main :: IO () though... so they all get evaluated in the context of another IO () don't they?

Jonathan Cast

7:11 p.m.

On Thu, 2009-02-05 at 15:52 -0800, David Leimbach wrote:

...

On Thu, Feb 5, 2009 at 2:38 PM, Jonathan Cast wrote:

On Thu, 2009-02-05 at 13:01 -0800, David Leimbach wrote: > > > On Thu, Feb 5, 2009 at 12:27 PM, Jonathan Cast > wrote: > > On Thu, 2009-02-05 at 12:21 -0800, David Leimbach wrote: > > > > > > On Thu, Feb 5, 2009 at 11:25 AM, Andrew Wagner > > wrote: > > I think the point of the Monad is > that it > > works as a container of stuff, that > still > > allows mathematically pure things to > happen, > > while possibly having some opaque > "other > > stuff" going on. > > > This at least sounds, very wrong, even if it's not. > Monads > > are not impure. IO is, but it's only _one_ instance > of Monad. > > All others, as far as I know, are pure. It's just > that the > > bind operation allows you to hide the stuff you > don't want to > > have to worry about, that should happen every time > you compose > > two monadic actions.

> > Well all I can tell you is that I can have (IO Int) in a > function as a > > return, and the function is not idempotent in terms of the > "stuff" > > inside IO being the same. > > > Sure it's the same. > > > cmp /bin/cat /bin/cat > > cp /bin/cat ~ > > cmp /bin/cat ~/cat > > > > Pretty much the same, anyway.

> So if IO represents a program that when executed interacts with the > world's state, is it safe to say that when I return (State Int Int), > that I'm returning a "State program"?

I won't object to it. Othe people might, though.

> That'd make sense as it really does look like we force the State to be > evaluated with runState, evalState or execState.

> The only difference with IO then is that to get IO programs to run, > you have to do it inside another IO program.

Meh. Combining IO sub-programs into larger programs doesn't really `get them to run'. Better to say that an IO value is meaningful only to the computer, and not mathematically (denotationally) useful.

All Haskell programs start as

...

main :: IO ()

...

though... so they all get evaluated in the context of another IO () don't they?

Well... Haskell compilers and runhaskell-style interpreters (not regular Hugs/ghci!) take the value of Main.main as `the program'. But that feels (to me --- I could be wrong) like an aspect of a particular hosted environment. REPLs can handle programs that aren't wrapped up in IO at all; and there's no reason why IO has to be the type of IO-performning-things in REPLs, either. You could just as well write a REPL that took, say, tangible values [http://haskell.org/haskellwiki/TV] as input instead, and displayed them. So it's more a matter of Haskell implementations can be given an IO value to run than that combining IO values together somehow runs them. jcc

ChrisK

7:27 p.m.

...

...
All Haskell programs start as

...
main :: IO ()

...
though... so they all get evaluated in the context of another IO () don't they?

True for most cases now, but historically false. Haskell existed and people wrote programs for years before the Monad class and IO were created. A Haskell98 program can be taken to have a "main :: IO ()", but that is not essential. Which is the point jcc made:

...

Well... Haskell compilers and runhaskell-style interpreters (not regular Hugs/ghci!) take the value of Main.main as `the program'. But that feels (to me --- I could be wrong) like an aspect of a particular hosted environment. REPLs can handle programs that aren't wrapped up in IO at all; and there's no reason why IO has to be the type of IO-performning-things in REPLs, either. You could just as well write a REPL that took, say, tangible values [http://haskell.org/haskellwiki/TV] as input instead, and displayed them. So it's more a matter of Haskell implementations can be given an IO value to run than that combining IO values together somehow runs them.

jcc

Tim Newsham

6 Feb 6 Feb

1:34 p.m.

...

So if IO represents a program that when executed interacts with the world's state, is it safe to say that when I return (State Int Int), that I'm returning a "State program"? That'd make sense as it really does look like we force the State to be evaluated with runState, evalState or execState.

Yes, exactly.

...

The only difference with IO then is that to get IO programs to run, you have to do it inside another IO program.

Almost. Add to your mental model a "runIO" that is invoked when your program runs as: "runIO main". Your haskell compiler or interpretter arranges this for you as part of its contract with you.

...

I hope I'm not making this worse! :-)

I dont think so. Tim Newsham http://www.thenewsh.com/~newsham/

wren ng thornton

7:09 p.m.

Tim Newsham wrote:

...

...
The only difference with IO then is that to get IO programs to run, you have to do it inside another IO program.

Almost. Add to your mental model a "runIO" that is invoked when your program runs as: "runIO main". Your haskell compiler or interpretter arranges this for you as part of its contract with you.

Also worth mentioning, the "to get IO to run you must do it from within IO" is not actually "running" ala unsafePerformIO, runState, runST, etc. Instead this transformation is called join :: M(M a) -> M a, which is different from run* :: M a -> ? For join, the monad structure says that more than one M layer can be collapsed into just one layer, but this is separate from being able to get rid of that last layer ("no escape"). For IO the join function can be thought of as inlining the other program or machine into the current one--- which is distinct from running that program/machine and using its results in the current one (that would be staged programming ala TH or MetaOCaml). The join and bind operators can be defined in terms of one another. Category theorists tend to prefer join, but Haskell programmers tend to prefer bind. Either one can be clearer depending on what is being explained, but it's helpful to think about them both. mx >>= f = join (fmap f mx) join mmx = mmx >>= id -- Live well, ~wren

Richard O'Keefe

8 Feb 8 Feb

7:39 p.m.

On 6 Feb 2009, at 5:08 am, Gregg Reynolds wrote:

...

Not "programs", but "programs that do IO". The point of the idiom is that there's an external side effect involved. What sticks in my craw is that "a mathematical value with a non-mathematical side effect" is, well, non-mathematical and possibly nonsensical.

I was introduced to group theory by being shown a real physical cube (a child's building block) and the real physical actions of turning a cube around in physical space that left it looking like the same cube in the same place. These physical actions are the elements of a group because the action "don't do anything" is the identity the combination rule "do X then do Y" is multiplication for every action there is an obvious "undo" (or inverse) action Take away the cube and the group remains: the elements of the group are (representable as) mathematical objects and you can operate on those mathematical objects to your heart's content. Of course nothing actually happens in the real world until you get a real cube and start following the instructions. The analogy: Members of the symmetry group on a cube : IO actions :: an actual real world : the IO state of a program :: someone following the turning orders : a Haskell system is a good one. If you want to say that "a mathematical value with a non-mathematical effect" is nonsensical, more power to you. I said I don't want to get far into White Knight territory. As long as you can agree "A mathematical value INTERPRETED BY a physical engine can have physical effects", we're home and dry. Let's face it, the idea of a Haskell program having physical effects (despite being a mathematical object) is no more (and no less) "non-mathematical and possibly nonsensical" than the idea of a C program (which is just a character string) having such effects, and no more (and no less) "non-mathematical and possibly nonsensical" than the idea of a machine code program (which is just a sequence of bits) having such effects. In all these cases, the program *is* a perfectly good mathematical value, just as good as the number 1, and arguably better than the number pi, and can be manipulated as an mathematical value, even computed as the result of a mathematical process. In all these cases, the program cannot and will not have any effects in the world whatsoever until it is combined with a physical program-interpreting device. Rem

...

I know it works for some (most?) people, but for me it lacks Geometry and Theology.

-g

Gregg Reynolds

9 Feb 9 Feb

3:56 a.m.

On Sun, Feb 8, 2009 at 6:39 PM, Richard O'Keefe wrote:

...

is a good one. If you want to say that "a mathematical value with a non-mathematical effect" is nonsensical, more power to you. I said I don't want to get far into White Knight territory. As long as you can agree "A mathematical value INTERPRETED BY a physical engine can have physical effects", we're home and dry.

Here's an analogy that will make the logical contradiction clear. Forget computers and assume you have been asked to referee a paper containing a proof with the following passage: Let x = ___ (Please fill in the blank) I think you will agree that would be plainly nonsensical. It's logically equivalent to an input operation ("getInt"). Now back to computers. Given a program text containing the symbol '3', the computer will provide a physical representation: an electromagnetic pattern in a bit of silicon. That's a value; the pattern is to be interpreted as a datum; it is not to be executed. For "getChar", the computer will also provide such a pattern, but this pattern is to be interpreted as executable code, not as a datum. Now suppose we also have an ordinary function like "Add2"; it too will be represented as an electromagnetic pattern, to be interpreted as executable code. getChar and Add2 are not data, except in the trivial sense that all code is data. All three "have an effect" only in the trivial sense that they are physically represented. In all three cases, the symbolic representation is isomorphic to the physical representation. The 3 will not be executed. When Add2 is executed, the ensuing process is isomorphic to the mathematical function so defined. But when getChar is executed, the ensuing process is not isomorphic to a mathematical function. The process interacts with the non-mathematical world, which a mathematical function can never do. So it has a side effect along with its ordinary representational effect. The point being that the metalanguage commonly used to describe IO in Haskell contains a logical contradiction. A thing cannot be both a value and a function, but e,g, getChar behaves like a function and has the type signature of a value. I believe this is part of the reason the IO monad is troublesome for beginners (I speak from experience). -g

Tony Morris

4:26 a.m.

-----BEGIN PGP SIGNED MESSAGE----- Hash: SHA1 Gregg Reynolds wrote:

...

The point being that the metalanguage commonly used to describe IO in Haskell contains a logical contradiction. A thing cannot be both a value and a function, but e,g, getChar behaves like a function and has the type signature of a value. getChar has the signature RealWorld -> (RealWorld, Char)

- -- Tony Morris http://tmorris.net/ ********************************************************* * Anteromedial Heterotopic Osseous Impingement Syndrome * ********************************************************* http://www.ajronline.org/cgi/content/full/178/3/601 "can result in chronic ankle pain, especially in athletes and the younger population (15-40 years old)" http://radiographics.rsnajnls.org/cgi/content/figsonly/22/6/1457 "Soft-tissue and osseous impingement syndromes of the ankle can be an important cause of chronic pain, particularly in the professional athlete." -----BEGIN PGP SIGNATURE----- Version: GnuPG v1.4.6 (GNU/Linux) Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org iD8DBQFJj/bcmnpgrYe6r60RAicqAJ9z3f+aM/k+gDv8d5yAaNSCFf9NVQCfX3Qo ItFqQSWPDUE2h9WS+axAXV8= =c8Nw -----END PGP SIGNATURE-----

Lennart Augustsson

5:10 a.m.

Not it doesn't. getChar has the type signature IO Char. The IO type is abstract. GHC happens to implement it by a state monad. But in, e.g., hbc it is implemented in a totally different way, more like a continuation monad. Peeking inside an implementation of IO can be illuminating, but one must remember that IO is abstract. -- Lennart On Mon, Feb 9, 2009 at 10:26 AM, Tony Morris wrote:

...

-----BEGIN PGP SIGNED MESSAGE----- Hash: SHA1

Gregg Reynolds wrote:

...
The point being that the metalanguage commonly used to describe IO in Haskell contains a logical contradiction. A thing cannot be both a value and a function, but e,g, getChar behaves like a function and has the type signature of a value. getChar has the signature RealWorld -> (RealWorld, Char)

- -- Tony Morris http://tmorris.net/

********************************************************* * Anteromedial Heterotopic Osseous Impingement Syndrome * *********************************************************

http://www.ajronline.org/cgi/content/full/178/3/601 "can result in chronic ankle pain, especially in athletes and the younger population (15-40 years old)"

http://radiographics.rsnajnls.org/cgi/content/figsonly/22/6/1457 "Soft-tissue and osseous impingement syndromes of the ankle can be an important cause of chronic pain, particularly in the professional athlete."

-----BEGIN PGP SIGNATURE----- Version: GnuPG v1.4.6 (GNU/Linux) Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org

iD8DBQFJj/bcmnpgrYe6r60RAicqAJ9z3f+aM/k+gDv8d5yAaNSCFf9NVQCfX3Qo ItFqQSWPDUE2h9WS+axAXV8= =c8Nw -----END PGP SIGNATURE-----

_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

Tony Morris

5:14 a.m.

-----BEGIN PGP SIGNED MESSAGE----- Hash: SHA1 You're right - my statement is inaccurate. Implementation details aside, I am referring specifically to the statement "getChar ... has the type signature of a value". It clearly does not. Lennart Augustsson wrote:

...

Not it doesn't. getChar has the type signature IO Char. The IO type is abstract. GHC happens to implement it by a state monad. But in, e.g., hbc it is implemented in a totally different way, more like a continuation monad.

Peeking inside an implementation of IO can be illuminating, but one must remember that IO is abstract.

-- Lennart

On Mon, Feb 9, 2009 at 10:26 AM, Tony Morris wrote: Gregg Reynolds wrote:

...
...
...
The point being that the metalanguage commonly used to describe IO in Haskell contains a logical contradiction. A thing cannot be both a value and a function, but e,g, getChar behaves like a function and has the type signature of a value. getChar has the signature RealWorld -> (RealWorld, Char)

...

Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

...

...

- -- Tony Morris http://tmorris.net/ S, K and I ought to be enough for anybody. -----BEGIN PGP SIGNATURE----- Version: GnuPG v1.4.9 (GNU/Linux) Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org iEYEARECAAYFAkmQAfkACgkQmnpgrYe6r61tmQCcCx42Cz1iunkD7JGubla/z2Pg uhAAoLk5rkjeHnrfc936IhYoBQYO/+0r =6xWk -----END PGP SIGNATURE-----

Lennart Augustsson

5:32 a.m.

But an (IO Char) is a value. You can do all the things with it that you can do with values, e.g., pass it as an argument, stick it in a list, etc. It is a special kind of value, since if it ever "gets in contact with" the top level it will be executed. But the fact that IO types also behave as values makes Haskell a very powerful imperative language. On Mon, Feb 9, 2009 at 11:14 AM, Tony Morris wrote:

...

-----BEGIN PGP SIGNED MESSAGE----- Hash: SHA1

You're right - my statement is inaccurate.

Implementation details aside, I am referring specifically to the statement "getChar ... has the type signature of a value". It clearly does not.

Lennart Augustsson wrote:

...
Not it doesn't. getChar has the type signature IO Char. The IO type is abstract. GHC happens to implement it by a state monad. But in, e.g., hbc it is implemented in a totally different way, more like a continuation monad.

Peeking inside an implementation of IO can be illuminating, but one must remember that IO is abstract.

-- Lennart

On Mon, Feb 9, 2009 at 10:26 AM, Tony Morris wrote: Gregg Reynolds wrote:

...
...
...
The point being that the metalanguage commonly used to describe IO in Haskell contains a logical contradiction. A thing cannot be both a value and a function, but e,g, getChar behaves like a function and has the type signature of a value. getChar has the signature RealWorld -> (RealWorld, Char)

...

Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

...
...
- -- Tony Morris http://tmorris.net/

S, K and I ought to be enough for anybody.

-----BEGIN PGP SIGNATURE----- Version: GnuPG v1.4.9 (GNU/Linux) Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org

iEYEARECAAYFAkmQAfkACgkQmnpgrYe6r61tmQCcCx42Cz1iunkD7JGubla/z2Pg uhAAoLk5rkjeHnrfc936IhYoBQYO/+0r =6xWk -----END PGP SIGNATURE-----

Tony Morris

5:38 a.m.

-----BEGIN PGP SIGNED MESSAGE----- Hash: SHA1 I also agree it is a value. The original post was attempting to make a distinction that does not exist. I deliberately avoided that topic. "A thing cannot be both a value and a function, but e,g, getChar" My original intent was to hope the poster reconsidered the whole post. You've blown my cover :) Lennart Augustsson wrote:

...

But an (IO Char) is a value. You can do all the things with it that you can do with values, e.g., pass it as an argument, stick it in a list, etc. It is a special kind of value, since if it ever "gets in contact with" the top level it will be executed. But the fact that IO types also behave as values makes Haskell a very powerful imperative language.

On Mon, Feb 9, 2009 at 11:14 AM, Tony Morris wrote: You're right - my statement is inaccurate.

Implementation details aside, I am referring specifically to the statement "getChar ... has the type signature of a value". It clearly does not.

Lennart Augustsson wrote:

...
...
...
Not it doesn't. getChar has the type signature IO Char. The IO type is abstract. GHC happens to implement it by a state monad. But in, e.g., hbc it is implemented in a totally different way, more like a continuation monad.

Peeking inside an implementation of IO can be illuminating, but one must remember that IO is abstract.

-- Lennart

On Mon, Feb 9, 2009 at 10:26 AM, Tony Morris wrote: Gregg Reynolds wrote:

...
...
> The point being that the metalanguage commonly used to > describe IO in Haskell contains a logical > contradiction. A thing cannot be both a value and a > function, but e,g, getChar behaves like a function and > has the type signature of a value. getChar has the signature RealWorld -> (RealWorld, Char)

_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

- -- Tony Morris http://tmorris.net/ S, K and I ought to be enough for anybody. -----BEGIN PGP SIGNATURE----- Version: GnuPG v1.4.9 (GNU/Linux) Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org iEYEARECAAYFAkmQB5EACgkQmnpgrYe6r60L5QCfffj1Vy2Yg25adZLsLBReOk/K ZAoAoISEpzQH/9D0AzQOZdxJoxmoKeBj =+ZZx -----END PGP SIGNATURE-----

Lennart Augustsson

6:22 a.m.

Sorry, I should have come down on the original poster too. ;) Functions are values, after all. On Mon, Feb 9, 2009 at 10:38 AM, Tony Morris wrote:

...

-----BEGIN PGP SIGNED MESSAGE----- Hash: SHA1

I also agree it is a value. The original post was attempting to make a distinction that does not exist. I deliberately avoided that topic.

"A thing cannot be both a value and a function, but e,g, getChar"

My original intent was to hope the poster reconsidered the whole post. You've blown my cover :)

Lennart Augustsson wrote:

...
But an (IO Char) is a value. You can do all the things with it that you can do with values, e.g., pass it as an argument, stick it in a list, etc. It is a special kind of value, since if it ever "gets in contact with" the top level it will be executed. But the fact that IO types also behave as values makes Haskell a very powerful imperative language.

On Mon, Feb 9, 2009 at 11:14 AM, Tony Morris wrote: You're right - my statement is inaccurate.

Implementation details aside, I am referring specifically to the statement "getChar ... has the type signature of a value". It clearly does not.

Lennart Augustsson wrote:

...
...
...
Not it doesn't. getChar has the type signature IO Char. The IO type is abstract. GHC happens to implement it by a state monad. But in, e.g., hbc it is implemented in a totally different way, more like a continuation monad.

Peeking inside an implementation of IO can be illuminating, but one must remember that IO is abstract.

-- Lennart

On Mon, Feb 9, 2009 at 10:26 AM, Tony Morris wrote: Gregg Reynolds wrote:

...
>> The point being that the metalanguage commonly used to >> describe IO in Haskell contains a logical >> contradiction. A thing cannot be both a value and a >> function, but e,g, getChar behaves like a function and >> has the type signature of a value. getChar has the signature RealWorld -> (RealWorld, Char)

_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

- -- Tony Morris http://tmorris.net/

S, K and I ought to be enough for anybody.

-----BEGIN PGP SIGNATURE----- Version: GnuPG v1.4.9 (GNU/Linux) Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org

iEYEARECAAYFAkmQB5EACgkQmnpgrYe6r60L5QCfffj1Vy2Yg25adZLsLBReOk/K ZAoAoISEpzQH/9D0AzQOZdxJoxmoKeBj =+ZZx -----END PGP SIGNATURE-----

Gregg Reynolds

6:24 a.m.

On Mon, Feb 9, 2009 at 4:38 AM, Tony Morris wrote:

...

-----BEGIN PGP SIGNED MESSAGE----- Hash: SHA1

I also agree it is a value. The original post was attempting to make a distinction that does not exist. I deliberately avoided that topic.

"A thing cannot be both a value and a function, but e,g, getChar"

My original intent was to hope the poster reconsidered the whole post. You've blown my cover :)

My bad, I restate: a value cannot be both static and dynamic. Or an object and a morphism. Or an element and a function. Sure, you can treat a morphism as an object, but only by moving to a higher (or different) level of abstraction. That doesn't erase the difference between object and morphism. If you do erase that difference you end up with mush. getChar /looks/ like an object, but semantically it must be a morphism. But it can't be a function, since it is non-deterministic. So actually the logical contradiction comes from the nature of the beast. Another reason it's confusing to newcomers: it's typed as "IO Char", which looks like a type constructor. One would expect getChar to yield a value of type IO Char, no? But it delivers a Char instead. This is way confusing. So I take "type IO foo" to mean "type foo, after a side effect". In a sense "getChar :: IO Char" isn't even a true type signature. In any case, many thanks to all who have contributed to the thread. It's sharpened my thinking revealed weaknesses in my terminology, and I expect I'll make my inevitable contribution to the infinite Haskell tutorial on the topic before too long. -gregg

Sittampalam, Ganesh

6:32 a.m.

...

My bad, I restate: a value cannot be both static and dynamic. Or an object and a morphism. Or an element and a function. Sure, you can treat a morphism as an object, but only by moving to a higher (or different) level of abstraction. That doesn't erase the difference between object and morphism. If you do erase that difference you end up with mush. getChar /looks/ like an object, but semantically it must be a morphism. But it can't be a function, since it is non-deterministic. So actually the logical contradiction comes from the nature of the beast.

Another reason it's confusing to newcomers: it's typed as "IO Char", which looks like a type constructor. One would expect getChar to yield a value of type IO Char, no? But it delivers a Char instead. This is way confusing. So I take "type IO foo" to mean "type foo, after a side effect". In a sense "getChar :: IO Char" isn't even a true type signature.

It does yield a value of type IO Char, which it also happens that you can ask the Haskell runtime to interpret by combining it with other IO values using >>= and invoking it from the top-level. *When interpreted in this way* it delivers a Char, but that's precisely the point at which we move to the different level of abstraction you mention above. Ganesh ============================================================================== Please access the attached hyperlink for an important electronic communications disclaimer: http://www.credit-suisse.com/legal/en/disclaimer_email_ib.html ==============================================================================

Gregg Reynolds

7:57 a.m.

On Mon, Feb 9, 2009 at 5:32 AM, Sittampalam, Ganesh < ganesh.sittampalam@credit-suisse.com> wrote:

...

...
My bad, I restate: a value cannot be both static and dynamic. Or an object and a morphism. Or an element and a function. Sure, you can treat a morphism as an object, but only by moving to a higher (or different) level of abstraction. That doesn't erase the difference between object and morphism. If you do erase that difference you end up with mush. getChar /looks/ like an object, but semantically it must be a morphism. But it can't be a function, since it is non-deterministic. So actually the logical contradiction comes from the nature of the beast.

Another reason it's confusing to newcomers: it's typed as "IO Char", which looks like a type constructor. One would expect getChar to yield a value of type IO Char, no? But it delivers a Char instead. This is way confusing. So I take "type IO foo" to mean "type foo, after a side effect". In a sense "getChar :: IO Char" isn't even a true type signature.

It does yield a value of type IO Char, which it also happens that you can ask the Haskell runtime to interpret by combining it with other IO values using >>= and invoking it from the top-level. *When interpreted in this way* it delivers a Char, but that's precisely the point at which we move to the different level of abstraction you mention above.

Right; "implementation of IO" means also an implementation for >>=, not just the IO operators. I hadn't thought about that but it's hugely important for the exposition of monads and IO. "The IO Char indicates that getChar, when invoked, performs some action which returns a character." (Gentle Intro, typical of many expositions.) That, plus the form of \x -> putChar x used with >>=, plus the fact that one can do getChar at the ghci command line, plus all the other stuff - it all adds up to exasperation. Thanks, gregg

David Menendez

12:41 p.m.

2009/2/9 Gregg Reynolds :

...

Right; "implementation of IO" means also an implementation for >>=, not just the IO operators. I hadn't thought about that but it's hugely important for the exposition of monads and IO.

"The IO Char indicates that getChar, when invoked, performs some action which returns a character." (Gentle Intro, typical of many expositions.)

In this case, I think "invoked" is shorthand for "interpreted by the runtime system".

...

That, plus the form of \x -> putChar x used with >>=, plus the fact that one can do getChar at the ghci command line, plus all the other stuff - it all adds up to exasperation.

It's worth noting that ghci, unlike Haskell itself, *does* treat IO specially. It checks the type of the expression you've entered, and behaves differently depending on whether it's equal to a, IO a, or IO (). interp[ e :: IO () ] = e interp[ e :: IO a ] = e >>= print interp[ e :: a ] = print e This is convenient for users, but it has nothing to do with the semantics of Haskell. -- Dave Menendez http://www.eyrie.org/~zednenem/

Tillmann Rendel

12:45 p.m.

Hi Gregg, Gregg Reynolds wrote:

...

Right; "implementation of IO" means also an implementation for >>=, not just the IO operators. I hadn't thought about that but it's hugely important for the exposition of monads and IO.

Indeed, that's very important. Note that the topics "monads in Haskell" and "IO in Haskell" can (and in my opinion should) be understood independently of each other. IO in Haskell is just an abstract data type, with a bunch of functions return :: a -> IO a bind :: IO a -> (a -> IO b) -> IO b getChar :: IO Char putChar :: a -> IO () ... A Haskell runtime system is a somewhat vaguely specified interpreter for (IO a) values. While it would be nice to a have a better specification of that interpreter, it is not part of the semantics of the language Haskell.

...

"The IO Char indicates that getChar, when invoked, performs some action which returns a character." (Gentle Intro, typical of many expositions.)

I guess that "invoked" here means really "interpreted by your Haskell implementation during its interpretation of the (IO a) your main function constructed". Tillmann

Bernie Pope

10 Feb 10 Feb

12:53 a.m.

On 10/02/2009, at 4:45 AM, Tillmann Rendel wrote:

...

A Haskell runtime system is a somewhat vaguely specified interpreter for (IO a) values. While it would be nice to a have a better specification of that interpreter, it is not part of the semantics of the language Haskell.

While not "official", there is always "Tackling the awkward squad: monadic input/output, concurrency, exceptions, and foreign-language calls in Haskell" by Simon Peyton Jones. https://research.microsoft.com/en-us/um/people/simonpj/papers/marktoberdorf/ Another nice aspect of that paper is that it discusses some of the difficulties in coming up with a denotation for values of type IO a, see particularly section 3.1. It suggests a set of event traces as a possible way forward: type IO a = (a, Set Trace) type Trace = [Event] data Event = PutChar Char | GetChar Char | ... (Incidentally, this view is quite useful in a declarative debugger, which emphasises the denotational semantics of a program.) In the end the paper goes for an operational semantics, on the grounds that the author finds it "simpler and easier to understand". Cheers, Bernie.

Lennart Augustsson

9 Feb 9 Feb

6:39 a.m.

Huh? The getChar function does yield a value of type (IO Char), exactly as the type signature says. If you want access to the Char you must use a >>=, just like in any other monad. 2009/2/9 Gregg Reynolds :

...

On Mon, Feb 9, 2009 at 4:38 AM, Tony Morris wrote:

...
-----BEGIN PGP SIGNED MESSAGE----- Hash: SHA1

I also agree it is a value. The original post was attempting to make a distinction that does not exist. I deliberately avoided that topic.

"A thing cannot be both a value and a function, but e,g, getChar"

My original intent was to hope the poster reconsidered the whole post. You've blown my cover :)

My bad, I restate: a value cannot be both static and dynamic. Or an object and a morphism. Or an element and a function. Sure, you can treat a morphism as an object, but only by moving to a higher (or different) level of abstraction. That doesn't erase the difference between object and morphism. If you do erase that difference you end up with mush. getChar /looks/ like an object, but semantically it must be a morphism. But it can't be a function, since it is non-deterministic. So actually the logical contradiction comes from the nature of the beast.

Another reason it's confusing to newcomers: it's typed as "IO Char", which looks like a type constructor. One would expect getChar to yield a value of type IO Char, no? But it delivers a Char instead. This is way confusing. So I take "type IO foo" to mean "type foo, after a side effect". In a sense "getChar :: IO Char" isn't even a true type signature.

In any case, many thanks to all who have contributed to the thread. It's sharpened my thinking revealed weaknesses in my terminology, and I expect I'll make my inevitable contribution to the infinite Haskell tutorial on the topic before too long.

-gregg

_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

egallego＠babel.ls.fi.upm.es

6:50 p.m.

Gregg Reynolds writes:

...

But it can't be a function, since it is non-deterministic.

IMHO, if you assume IO a = World -> (World, a), then getChar is indeed a function and deterministic. It is, there are not w :: World such that getChar w != getChar. The fact that World is too big to be represented in Haskell and we use IO to simulate it is a different matter. With regard to your original question, I like to keep in mind that arrow composition in the Kleisli category (>>= in Haskell) is defined in terms of the monad's join :: m (m a) -> m a. Then, the question is, how many ways can you map an IO (IO a) to an IO a? You will find that you cannot ignore the inner (first) IO in order to obey monad laws. Regards, Emilio

egallego＠babel.ls.fi.upm.es

7:07 p.m.

egallego@babel.ls.fi.upm.es (Emilio Jesús Gallego Arias) writes:

...

IMHO, if you assume IO a = World -> (World, a), then getChar is indeed a function and deterministic. It is, there are not w :: World such that getChar w != getChar.

Sorry I meant: There is not w :: World such that getChar w != getChar w.

Richard O'Keefe

8:19 p.m.

On 10 Feb 2009, at 12:24 am, Gregg Reynolds wrote:

...

My bad, I restate: a value cannot be both static and dynamic.

It's not clear what you mean here, but in what sense are "static" values not a subset of "dynamic" ones?

...

Or an object and a morphism.

Crack open any book on category theory and you will discover that an object CAN be a morphism. Not only can the morphisms of one category be objects of another, but you can build a category where the objects and the morphisms are the same things.

...

Or an element and a function.

An element of _what_? Functions can be elements of sets. Mathematicians routinely deal with function spaces. If you mean that F : S -> S cannot be an element of S, then if you mean a set theoretic function, no, but a Scott domain *can* contain the continuous functions over itself.

...

Sure, you can treat a morphism as an object, but only by moving to a higher (or different) level of abstraction.

False as a generalisation about mathematics. False about functional programming languages, the very essence of which is treating functions ("morphisms") as values ("objects") exactly like any other values.

...

That doesn't erase the difference between object and morphism.

There is no intrinsic difference between objects and morphisms. It's what you DO with something that makes it an object or a morphism (or both).

...

If you do erase that difference you end up with mush. getChar / looks/ like an object, but semantically it must be a morphism.

getChar is an element of an abstract data type in Haskell. PERIOD. Since a morphism is characterised by its source and target objects, and since getChar is not so characterised, in what sense is getChar a morphism? *Within Haskell*, getChar is just some value. For all you or I can tell to the contrary, it might be the letter 'G' or a JPEG image of the planet Mars. It's only as part of a whole system of IO primitives in the context of Haskell that the value is interpreted as a description of the "read a character from standard input" action.

...

But it can't be a function, since it is non-deterministic.

No it isn't. getChar is perfectly deterministic. Whenever you ask for the value of getChar, you get the *same* value. Evaluating getChar does no input whatever. If you compute map (\_ -> getChar) [1..n] you get a list containing n copies of the value of getChar, and NO INPUT WHATSOEVER happens.

...

So actually the logical contradiction comes from the nature of the beast.

There is no logical contradiction because you have mistaken the nature of the beast.

...

Another reason it's confusing to newcomers: it's typed as "IO Char", which looks like a type constructor.

Surely "IO" and "Char" are type constructors, and "Char" and "IO Char" are types.

...

One would expect getChar to yield a value of type IO Char, no?

Yes, that's EXACTLY what it does. The only thing the expression (getChar) ever gives you is an (abstract) value of type IO Char.

...

But it delivers a Char instead.

No it doesn't. getChar delivers, always and only, a value of type IO Char. Call that value Gamaliel. When Gamaliel is *performed* by the Haskell environment, *then* a character is read (the action) and returned. But it's Gamaliel that delivers a Char, not getChar.

...

This is way confusing.

Composer (Haskell program) writes score (computes getChar). Performer (Haskell environment) sings score (performs Gamaliel). Sound happens (a character is read).

...

So I take "type IO foo" to mean "type foo, after a side effect".

No. Mistake not: there COULD be a type system not unlike that. Look up "effect systems". Haskell's is not one of them. By the way, (return 'x') has type IO Char, but never has any side effects. Type "IO foo" can be usefully read as meaning "descriptions of actions that when carried out also yield a value of type foo".

...

In a sense "getChar :: IO Char" isn't even a true type signature.

Yes it is. It is exactly and perfectly true. Have you actually read the classic paper "How to declare an imperative", P. Wadler, ACM Computing Surveys 29, 3 (1997). For me, this was more helpful than any tutorial on monads and monadic I/O that I ever read.

...

wren ng thornton

10 Feb 10 Feb

8:01 p.m.

Richard O'Keefe wrote:

...

Gregg Reynolds wrote:

...
Sure, you can treat a morphism as an object, but only by moving to a higher (or different) level of abstraction.

False as a generalisation about mathematics. False about functional programming languages, the very essence of which is treating functions ("morphisms") as values ("objects") exactly like any other values.

...
That doesn't erase the difference between object and morphism.

There is no intrinsic difference between objects and morphisms. It's what you DO with something that makes it an object or a morphism (or both).

...
This is way confusing.

Composer (Haskell program) writes score (computes getChar). Performer (Haskell environment) sings score (performs Gamaliel). Sound happens (a character is read).

+1. The only difference between objects and morphisms is in the decision by some supreme entity (human reader, Haskell runtime) to treat them differently. There is nothing different between them other than our decisions to treat them differently. As for the concrete example about "3", I define:

...

let 3 = \f x -> f(f(f x))

which is as valid as any other definition. Oh noes, you say, it's a function and therefore a morphism. And certainly it is. However, it's perfectly fine to treat that as a value and define a "real" function like addition:

...

let m + n = \f x -> m f (n f x)

When people see something like "1 + 2 + 3" they choose to think of 1, 2, and 3 as "objects" and choose to think of (+) and (+) as "morphisms", but who cares? Any datum can be encoded as a function, the execution of which enacts the existence of the object the function denotes. And, in functional languages, functions can be passed around and clubbed over the head just like every other value. And therein lies the rub: "the execution of which enacts the existence of the object the function denotes." The only thing that distinguishes objects and morphisms is the decision by some supreme entity to treat them that way. Just as you once said that values don't concatenate, so neither do functions apply. The application of functions can only be observed by some evaluator for the structure generated by application. Application itself has no semantics, it just builds ASTs and uninterpreted terms; only our choice to evaluate ASTs and terms gives them meaning. -- Live well, ~wren

Richard O'Keefe

9 Feb 9 Feb

8:47 p.m.

On 9 Feb 2009, at 9:56 pm, Gregg Reynolds wrote:

...

Here's an analogy that will make the logical contradiction clear. Forget computers and assume you have been asked to referee a paper containing a proof with the following passage:

Let x = ___ (Please fill in the blank)

I think you will agree that would be plainly nonsensical. It's logically equivalent to an input operation ("getInt").

No, I do not agree that it would be nonsensical at all. Why shouldn't a paper describe a family of proofs? (paper :: Int -> Proof)

...

Now back to computers. Given a program text containing the symbol '3', the computer will provide a physical representation: an electromagnetic pattern in a bit of silicon. That's a value; the pattern is to be interpreted as a datum; it is not to be executed.

Who says? It is part of the essence of the stored program computer that the *same* bit pattern may be computed as numbers and executed as code. There have certainly been virtual machines where the bit pattern for the character '+' meant, when executed, ADD.

...

For "getChar", the computer will also provide such a pattern, but this pattern is to be interpreted as executable code, not as a datum.

"The computer" here must be understood as "The composite of a physical machine, HAL/BIOS/whatever-maybe, hypervisor-maybe, operating system- maybe, Haskell compiler, and Haskell libraries. (Yes, I know that I am oversimplifying.) The expression (getChar) may be represented by executable code, but then, Haskell being lazy, so may the expression (1+1) be represented by executable code. Your problem seems to be based on two fundamental assumptions: (1) there is an intrinsic difference between code and data, (2) evaluating getChar reads a character. Neither assumption is true. Code and data are interchangeable. Evaluating getChar yields (without any side effects) a value, let's call it Gamaliel, and it is the environment's performance of Gamaliel that reads a character. So you are seeing a difference when there is none, and not seeing one where there is one.

...

Now suppose we also have an ordinary function like "Add2"; it too will be represented as an electromagnetic pattern, to be interpreted as executable code.

*AND* as data. Ever heard of genetic programming? Genetic programming is a form of evolutionary computing where members of the population are functions. Koza's original book used lisp-style trees to represent these functions (so something was at one and the same time a tree resulting from genetic operations and used as input to genetic operations) and executable code. There have been many variations of the idea since then. Nowadays some GP systems represent functions by native machine code. In such systems, native machine code is - the result of genetic operators - data that is input to genetic operators - native code to be executed all in the same program within a single "generation".

...

getChar and Add2 are not data, except in the trivial sense that all code is data.

The sense in which all code is data is far from trivial. It's what makes things like Windows *possible*. (Try to imagine booting Windows by plugging wires into a city-sized backplane!) It's certainly what makes Genetic Programming possible. The interesting thing here is that since getChar need not be a function, its representation inside a computer need not be machine code.

...

In all three cases, the symbolic representation is isomorphic to the physical representation.

Eh? This is a very strong and extremely dubious claim.

...

The 3 will not be executed.

Who says? I once used (and still love) a computer which had Zero and One instructions. I don't see why you couldn't have a Three instruction.

...

When Add2 is executed, the ensuing process is isomorphic to the mathematical function so defined.

The *process* is isomorphic to the *function*? I think not.

...

But when getChar is executed, the ensuing process is not isomorphic to a mathematical function.

Yes it is. You are confusing two very different things here: Executing (getChar). Performing the result of (getChar). For what it's worth, the analogue of getChar in Clean and Mercury *is* a mathematical function.

...

The process interacts with the non-mathematical world, which a mathematical function can never do.

But a mathematical function can *describe* that process, and a computing engine can have its interactions governed by such a description. And that's what Haskell does.

...

So it has a side effect along with its ordinary representational effect.

No. [The result of] (getChar) is a pure mathematical value. (It might be or contain a function, but it need not. It could be the number 42 in drag.) When the Haskell environment does what that [result] says to do, then reading happens. But the computation of (getChar) and the reading are DIFFERENT events (notionally) carried out by DIFFERENT execution engines and happening at DIFFERENT times.

...

The point being that the metalanguage commonly used to describe IO in Haskell contains a logical contradiction.

No, you have read a contradiction into it, but the contradiction is not there.

...

A thing cannot be both a value and a function,

Yes it can. ALL functions are values.

...

but e,g, getChar behaves like a function and has the type signature of a value.

getChar behaves like a value. You can evaluate getChar 500 million times and not one character will be read.

...

I believe this is part of the reason the IO monad is troublesome for beginners (I speak from experience).

When I read the "How to declare an imperative" paper, I fell about laughing. It was so *simple*, and yet, so astronomically far from anything I could have invented. When you have understood that there really isn't anything magical about getChar (and there most CERTAINLY isn't anything remotely resembling a contradiction or inconsistency or type incorrectness), you will have begun to understand monads.

Lennart Augustsson

5 Feb 5 Feb

2:46 p.m.

You are absolutely right. The statement "The values of the IO monad are programs that do IO. " is somewhat nonsensical. Values don't do anything, they just are. But values of the IO monad *describe* how to do IO; they can be seen as a recipe for doing IO. A recipe doesn't cook a dish, but when the recipe is executed by a cook they creates a dish. An IO values doesn't do IO, but when it is executed by the runtime system IO happens. This is one way of interpreting what the IO type means. (Another one is to say that Haskell is just an imperative programming language, but any imperative actions show up in the type.) -- Lennart 2009/2/4 Gregg Reynolds :

...

On Wed, Feb 4, 2009 at 11:41 AM, Tim Newsham wrote:

...
I put up a small Monad explanation (I wouldn't quite call it a tutorial): http://www.thenewsh.com/~newsham/haskell/monad.html

"The values of the IO monad are programs that do IO. "

That's a fairly common representation, seems to work for lots of people, but it caused me no end of trouble. Values are mathematical objects; how, I asked myself, can they possibly /be/ programs that do IO (or actions, or computations, or <your metaphor here>)? It doesn't make sense, says I, so I must be misunderstanding something about "values"; better spend hours and hours researching and trying to figure this out. But it turns out the answer is simple: they can't. They're not actions, or IO procedures, or anything else other than plain old mathematical values, no different than '2' or Int -> Char. They happen to correspond in some way to the external physical behavior of the program, but that correspondence is an implementation detail beyond the scope of the formal (mathematical) semantics of the language. You don't even need monads for this part; they only enter the picture in order to provide ordered evaluation. In fact there really aren't any "monadic values", since a monad is pure morphism; the values at issue are "functoric values" if anything. It's (the implementation of) getChar the does the IO, not IO Char.

So you could say that the monad itself is a purely mathematical structure that has the felicitous if accidental side effect of imposing temporal sequence on the physical interpretation (events) associated with the program.

-g

_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

Gregg Reynolds

3:03 p.m.

On Thu, Feb 5, 2009 at 1:46 PM, Lennart Augustsson wrote:

...

You are absolutely right. The statement "The values of the IO monad are programs that do IO. " is somewhat nonsensical. Values don't do anything, they just are.

Whew! So I'm not crazy. I was starting to wonder.

...

But values of the IO monad *describe* how to do IO; they can be seen as a recipe for doing IO. A recipe doesn't cook a dish, but when the recipe is executed by a cook they creates a dish. An IO values doesn't do IO, but when it is executed by the runtime system IO happens.

This is one way of interpreting what the IO type means. (Another one is to say that Haskell is just an imperative programming language, but any imperative actions show up in the type.)

Thanks very much to you and everybody who contributed on the thread. It's amazing how much one can learn on this list. -gregg

Jonathan Cast

3:14 p.m.

On Thu, 2009-02-05 at 20:46 +0100, Lennart Augustsson wrote:

...

You are absolutely right. The statement "The values of the IO monad are programs that do IO. " is somewhat nonsensical. Values don't do anything, they just are.

Technically, programs don't do anything either. I think of values of type IO a as being --- conceptually --- arbitrary sequences of machine code instructions. Just like a sequence of machine code instructions can be stored away in /bin/cat, and not do anything, an IO value needn't do anything, either. Until it's stored in memory and the instruction pointer set to its first instruction. At which point, if you want to get really picky, it's still the CPU doing things. Which it is told to do by its fixed microcode. Which tells it to look at your program to see what to do. Which = looking at the `value' of your IO-typed expression to see what to do. jcc

Tim Newsham

3:21 p.m.

...

You are absolutely right. The statement "The values of the IO monad are programs that do IO. " is somewhat nonsensical. Values don't do anything, they just are. But values of the IO monad *describe* how to do IO; they can be seen as a recipe for doing IO. A recipe doesn't cook a dish, but when the recipe is executed by a cook they creates a dish. An IO values doesn't do IO, but when it is executed by the runtime system IO happens.

Just as a recipe describes how to cook something, a program describes how to accomplish something. The program doesnt "do" anything until it is executed. However, we often use the word "do" to describe what a program will do when executed (even though its really the cpu that is actually "doing").

...

This is one way of interpreting what the IO type means. (Another one is to say that Haskell is just an imperative programming language, but any imperative actions show up in the type.)

I don't see the difference between these two interpretations. Wether the program is made up of instructions for a cpu or for an interpreter seems irrelevant.

...

-- Lennart

Tim Newsham http://www.thenewsh.com/~newsham/

5945

Age (days ago)

5952

Last active (days ago)

List overview

Download

56 comments

21 participants

participants (21)

Andrew Wagner
Benjamin L.Russell
Bernie Pope
ChrisK
Dan Piponi
Daryoush Mehrtash
David Leimbach
David Menendez
egallego＠babel.ls.fi.upm.es
Gregg Reynolds
Jonathan Cast
Lennart Augustsson
Max Rabkin
Miguel Mitrofanov
Richard O'Keefe
Sittampalam, Ganesh
Tillmann Rendel
Tim Newsham
Tony Morris
Tymur Porkuian
wren ng thornton