At Thu, 10 Dec 2009 12:07:32 +0000, Magnus Therning wrote:

As I understand it it all started with laziness. I don't know if laziness is impossible without purity

More or less. Haskell is a language where anything can be evaluated lazily by default. Unlike say Scheme, where if you want something to be evaluated lazily you have to be explicit about it, in Haskell it's the opposite - if you want something to be evaluated _strictly_ you have to be explicit about it. If you write an impure expression in Haskell (e.g. using unsafePerformIO) the side-effects of it might be executed once, twice, or never, depending on the Haskell implementation in use, the optimisation flags, or even other Haskell code in the system. And the side-effects might be executed at unpredictable times, in an unpredictable order, and only some of them might occur. Now, this might be fine for debugging purposes, where you want to see what is being done under the hood - but for most other side-effects, you really want them to occur in a more controllable way. Hence, to answer John's question, a lazy language _has_ to be pure (apart from the unsafe functions) because laziness (or, to be more technically correct, non-strict evaluation) is incompatible with good control of the side-effects arising from impure code. Both Clean and Haskell deal with side-effects by allowing the programmer to write imperative code in a pure way - in Haskell, by using monads or FRP, and in Clean by using world-passing and uniqueness types. Now, that answer probably suffices for a Haskell beginner. Of course eventually you realise time and space usage is a side-effect, and _that_ needs to be controlled as well... but despite this, I think my answer is basically right. However, that's not the _only_ reason why you might want purity. Even in a strict language, purity makes it easier to reason about code, because you don't have to consider the environment, only the parameters that are passed in. Of course, it gets more complicated with monads, because the Environment monad and the IO monad both give you implicit environments at the level of "running the monadic actions". But even then, it's supposed to be easier to reason about (once you get the hang of it), and I'd broadly agree with this. -- Robin

On Thu, Dec 10, 2009 at 9:13 AM, John D. Earle wrote:

Most of the discussion centers on the benefits of functional programming and laziness. Haskell is not merely a lazy functional language. It is a pure lazy functional language. I may need to explain what laziness is. Laziness is where you work through the logic in its entirely before acting on the result. In strict evaluation the logic is worked out in parallel with execution which doesn't make complete sense, but it does allow for an architecture that is close to the machine.

Just to roil the waters a bit: no programming language can ever hope to be "purely functional", for the simple reason that real computation (i.e. computation involving IO, interactivity) cannot be functional. "Functional programming" is an unfortunate misnomer. On the other hand, languages can be algebraic. The whole point is provability, not function-ness. More generally: judging by the many competing proposals addressing the issue of how to think formally about real computation (just google stuff like hypercomputation, interactive computation, etc.; Jack Copelandhttp://www.hums.canterbury.ac.nz/phil/people/copeland.shtml#articleshas lots of interesting stuff on this) is still an open question. Soare has three essential papers http://www.people.cs.uchicago.edu/%7Esoare/History/on the subject. I guess the moral of the story is that the concepts and the terminology are both still unstable, so lots of terms in common use are rather ill-defined and misleading (e.g. functional programming). Lazyness is just a matter of how one attaches an actual computation to an expression; a better term would be something like "delayed evaluation" or "just-in-time computation". You don't have to work through any logic to have laziness. Just think about how one reads a mathematical text - you need not actually compute subformulae or even analyze them logically in order to work with them. This applies right down to expressions like "2+3" - one probably would compute "5" on reading that, but what about "12324/8353"? You'd leave the computation until you absolutely had to do it - i.e. one would probably try to eliminate it algebraically first. -gregg

On Thu, Dec 10, 2009 at 11:16 AM, John D. Earle wrote:

Dear Gregg,

You wrote, "Just think about how one reads a mathematical text - you need not actually compute subformulae or even analyze them logically in order to work with them." I hate to have to say this, but do you realize that algebra is concerned with functions among other things and it is the fact that these expressions are functions and not that they are algebraic that gives them this property?

Hi John, I'd say algebra is mostly concerned with equalities and substitutions and doesn't much care about functions. The equation for a circle is not a function but that doesn't mean we can't use algebra to manipulate it. Algebras might use the concept of function but they are not necessarily _about_ functions. One could even argue that the lambda calculus isn't "about" functions - it's just a calculus, after all. Haskell goes by the rules of that calculus; whether the expressions involved denote functions is not relevant. The computer is just performs symbol calculus. Generally all formal semantics can be reduced to syntactic calculus as far as I can see.

Functional programming is not a misnomer. It is called functional programming because you are quite literally working with functions.

Except when you're not. IO operations are never functions, for example, so IO expressions never denote functions. FP languages do not (and cannot) eliminate the side effectful nature of such operations; the best they can do is what Haskell does, namely circumscribe them so that they are well-behaved and thus can be properly managed (algebraically). But that doesn't make them functions. So for me at least "algebraic" better describes how Haskell works; what you're working with is expressions and you reason about them algebraically. You can do this reliably not because everything is a function but because non-functions are well-behaved.

Functions have a profound simplifying effect.

No argument there. But the expressive power that comes with first-class functions is not what distinguishes Haskell et al. - lots of non-FP languages support them these days.

The truth is as Haskell has demonstrated that much of the complexity in computer programming is artificial and doesn't need to be there. It makes having to prove correctness a lot easier, but that is not the only motivation behind Haskell and other functional programming languages. The push has been getting performance up to a point where the language may be regarded as respectable.

Sure, but that's only possible because the properties of programs are provable, which is what makes it possible to reliably transform a program into an equivalent but more efficient form. -Gregg

Magnus, thank you. It at least gives me a lead. I can focus on the significance of laziness and what role it may have on purity. That the language is lazy gives me no anxiety as I see laziness as natural. I see Haskell as having proven that laziness is viable; a language can be lazy and fast and memory efficient. I am trying to put the puzzle pieces together and from what I can gather purity may be a perceived outcome of combinatory logic with Occam's razor. So perhaps the motivation is scientific. Unless you absolutely must don't go there. Science is an evolutionary process. You go from Newtonian mechanics to Relativity. Relativity is more complicated than Newtonian mechanics, but it was proven that the additional complexity was needed. -------------------------------------------------- From: "Magnus Therning" Sent: 10 Thursday December 2009 0507 To: "John D. Earle" Cc: "Haskell Cafe" Subject: Re: [Haskell-cafe] Why?

On Thu, Dec 10, 2009 at 12:01 PM, John D. Earle wrote:

...

This is a matter that I genuinely at the present time do not grasp and I am hoping that some of you who are more familiar with the Haskell language may be able to help enlighten me. I feel the question to be an important one. What material benefit does Haskell derive from being a "pure" functional language as opposed to an impure one? Please provide examples as I require instruction.

The following is what I believe to be true at the present time. It seems to be that the decision was made because it was a matter of taste under the belief that computer scientists can and often are superstitious and their superstitions can and often do materially interfere with progress. What I am saying is that at the present time perhaps due to my ignorance I am unfamiliar with how this benefits the language in a material sense. It appears to be a philosophical matter, a matter of identity, what Haskell stands for.

The sort of decision that Apple computer and Microsoft made not to go down the POSIX road seems relevant. Historically, Apple did not embrace POSIX. Windows continues to stand for Windows, that is the graphical user interface.

As I understand it it all started with laziness. I don't know if laziness is impossible without purity, but talks and papers tend to say something like "laziness has kept Haskell pure".

/M

-- Magnus Therning (OpenPGP: 0xAB4DFBA4) magnus＠therning．org Jabber: magnus＠therning．org http://therning.org/magnus identi.ca|twitter: magthe

On 10/12/09 12:07, Magnus Therning wrote:

As I understand it it all started with laziness. I don't know if laziness is impossible without purity, but talks and papers tend to say something like "laziness has kept Haskell pure".

This is true, but laziness has its own advantages. Suppose I have two modules, Foo and Bar. Foo generates a data structure which is then consumed by Bar (possibly with some other component calling both of them). In a strict language I have to choose between one of these three options: 1. Foo generates the structure all at once, and some kind of reference is then passed to Bar. This is nice, simple and modular, but it only works for small structures. There can also be a problem if the structure is slow to generate but is only consumed a bit at a time (e.g. by the user interface) because Bar can only start work once Foo has finished the whole thing. You may also find the Foo is doing lots of unnecessary work building bits of the structure that Bar uses only rarely. 2. Foo and Bar are built together in a single module with their functionality interleaved. This means that Foo can build a bit of the structure, have Bar process it, and so on. However it also destroys any modularity the system might have had. If Bar is part of the user interface, for instance, it means that core functionality gets mixed up. 3. Implement some kind of generator object. This takes a lot of code and makes the logic of Foo and Bar harder to follow. For instance the version of Foo from option 1 might have had a loop of the form "foreach i in xs". Now "i" has to be turned into some kind of member variable with logic to move to the next instance. Of course what you are really doing is creating an ad-hoc hand-coded version of lazy evaluation. Different applications are going to require different choices. Worse yet, the right answer can change. For instance you may start with option 1, then discover that the program runs too slowly. Or marketing decide that the maximum size of the data structure has to be increased. So at that point you have to rewrite a big chunk of code. Or else you go with option 2 or 3 because the designer thought it was necessary for efficiency when in fact option 1 would have done nicely. Of course with lazy evaluation you get option 3 all the time automatically. So its just not a problem. This makes the design much simpler because things that previously had to be decided by a human are now decided by the compiler. Paul.

Hello Sebastian, Thursday, December 10, 2009, 4:27:49 PM, you wrote:

The killer app for that, IMO, is parallelism these days

btw, are you seen Google App Engine? it's python/java ATM, but i think that haskell will be ideal fit there. it's all about computations-in-cloud, or more precisely hosting-in-a-cloud, like Amazon EC2 so, both individual cpus and largest servers now are multi-threaded, it just need some time so EC2/GAP developers will realize Haskell potential -- Best regards, Bulat mailto:Bulat.Ziganshin@gmail.com

On Dec 10, 2:38 pm, Bulat Ziganshin wrote:

Hello Sebastian,

Thursday, December 10, 2009, 4:27:49 PM, you wrote:

...

The killer app for that, IMO, is parallelism these days

btw, are you seen Google App Engine? it's python/java ATM, but i think that haskell will be ideal fit there. it's all about computations-in-cloud, or more precisely hosting-in-a-cloud, like Amazon EC2

I think the first language which would come to mind, is acutally Erlang. As a cloud server process and cloud database backend might be physically distributed, it's more logical to send messages between them asynchronously, than share state in parallel. But yes, Haskell fit's this pattern well, through the Control.Concurrent library.

so, both individual cpus and largest servers now are multi-threaded, it just need some time so EC2/GAP developers will realize Haskell potential

-- Best regards,  Bulat                            mailto:Bulat.Zigans...@gmail.com

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

C'mon Andrew - how about some facts, references? 2009/12/10 Andrew Coppin :

1. Code optimisation becomes radically easier. The compiler can make very drastic alterations to your program, and not chance its meaning. (For that matter, the programmer can more easily chop the code around too...)

Which code optimizations?

From a different point of view, whole program compilation gives plenty of opportunity for re-ordering transformations / optimization - Stalin (now Stalinvlad) and MLton often generated the fastest code for their respective (strict, impure) languages Scheme and Standard ML.

Feel free to check the last page of the report here before replying with the Shootout - (GHC still does pretty well though easily beating Gambit and Bigloo): http://docs.lib.purdue.edu/ecetr/367/

2. Purity leads more or less directly to laziness, which has several benefits:

Other way round, no?

2a. Unecessary work can potentially be avoided. (E.g., instead of a function for getting the first solution to an equation and a seperate function to generate *all* the solutions, you can just write the latter and laziness gives you the former by magic.)

Didn't someone quote Heinrich Apfelmus in this list in the last week or so: http://www.haskell.org/pipermail/haskell-cafe/2009-November/069756.html "Well, it's highly unlikely that algorithms get faster by introducing laziness. I mean, lazy evaluation means to evaluate only those things that are really needed and any good algorithm will be formulated in a way such that the unnecessary things have already been stripped off." http://apfelmus.nfshost.com/quicksearch.html

2b. You can define brand new flow control constructs *inside* the language itself. (E.g., in Java, a "for" loop is a built-in language construct. In Haskell, "for" is a function in Control.Monad. Just a plain ordinary function that anybody could write.)

Psst, heard about Scheme & call/cc?

2c. The algorithms for generating data, selecting data and processing data can be seperated. (Normally you'd have to hard-wire the stopping condition into the function that generates the data, but with lazy "infinite" data structures, you can seperate it out.)

Granted. But some people have gone quite some way in the strict world, e.g.: http://users.info.unicaen.fr/~karczma/arpap/FDPE05/f20-karczmarczuk.pdf

2d. Parallel computation. This turns out to be more tricky than you'd think, but it's leaps and bounds easier than in most imperative languages.

Plenty of lazy and strict, pure and impure languages in this survey: http://www.risc.uni-linz.ac.at/people/schreine/papers/pfpbib.ps.gz

3. It's much harder to accidentally screw things up by modifying a piece of data from one part of the program which another part is still actually using. (This is somewhat similar to how garbage collection makes it harder to free data that's still in use.)

In a pure language I'd like to think its impossible... Best wishes Stephen

...

...

2b. You can define brand new flow control constructs *inside* the language itself. (E.g., in Java, a "for" loop is a built-in language construct. In Haskell, "for" is a function in Control.Monad. Just a plain ordinary function that anybody could write.)

Psst, heard about Scheme & call/cc?

But, very importantly, purity allows you to *restrict* the flow constructs that client code has available. If you have continuations + mutable state you can do anything, but the more code can *do*, the less you *know* about it. For example, providing parser combinators as an applicative functor offers more power than a traditional parser generator, but not enough that we can no longer parse efficiently.

Exactly my fear over unsafePerformIO in 3rd party Haskell libraries :-). One can present an interface in Haskell that looks safe, but it can be very unsafe in its implementation. Dave

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

2009/12/10 Luke Palmer :

I always meet with armies of resistance when I say this...

The troops arrive.

...but unsafePerformIO should die a horrible, unforgiven death. "Well what if you want blah blah blah with a pure interface?" My response: too fscking bad!

Wouldn't removing `unsafePerformIO` just force us, in many cases, to write the same thing in C and then import it? Or would you amend the FFI so "math.h sin" could not be imported pure? There are plenty of bad ways to use `unsafePerformIO`, this is true; but as we already have a tool for binding to native code in a way that trusts it to be pure, I don't see how having a way to bind to nominally side-effecting Haskell code in a way that trusts it to be pure adds anything to our troubles. -- Jason Dusek

On Fri, Dec 11, 2009 at 4:55 PM, Jason Dusek wrote:

2009/12/10 Luke Palmer :

...

I always meet with armies of resistance when I say this...

 The troops arrive.

...

...but unsafePerformIO should die a horrible, unforgiven death. "Well what if you want blah blah blah with a pure interface?" My response: too fscking bad!

 Wouldn't removing `unsafePerformIO` just force us, in many  cases, to write the same thing in C and then import it? Or  would you amend the FFI so "math.h sin" could not be imported  pure?

This is not the sort of resistance I expected :-). Naturally my unrealistic argument applies to FFI as well; sin, if imported from C, would have to return in an appropriate structure. Not necessarily IO (I don't like the idea of a universal sin-bin -- I'd rather introduce a family of structures with well-defined meanings), but the same idea. Support for commutative monads (once we understand them) may relieve some of the pain of this approach. The idea being that any code that is pure could be evaluated anywhere with a very simple interpreter. If you have pure code, you can trace it back and evaluate it in a sandbox where you don't need a C runtime, a linker, or really anything but the simplest substitution engine. *All* effects bubble their way up to the top level, so that we know from the type signature of a value the machinery we will need to run it. Pure functional code as the minimal essence of pure computation -- everything else an EDSL. Of course I am not talking about Haskell anymore. Haskell is a firm, maturing language and has no room for such radical changes. This argument applies to an eventual spiritual successor of Haskell (it is probably too liberal for Haskell' even). Luke

2009/12/11 Luke Palmer :

The idea being that any code that is pure could be evaluated anywhere with a very simple interpreter. If you have pure code, you can trace it back and evaluate it in a sandbox where you don't need a C runtime, a linker, or really anything but the simplest substitution engine. *All* effects bubble their way up to the top level, so that we know from the type signature of a value the machinery we will need to run it.

This sounds good but there is something puzzling about it. Where do we draw the line between "machinery" and "packages"? The types don't tell us what libraries we need. They don't tell us how much RAM/CPU we need, either.

Pure functional code as the minimal essence of pure computation -- everything else an EDSL.

Partial or total code? -- Jason Dusek

Stephen Tetley wrote:

C'mon Andrew - how about some facts, references?

Facts I can do. References? Not so much...

...

1. Code optimisation becomes radically easier. The compiler can make very drastic alterations to your program, and not chance its meaning. (For that matter, the programmer can more easily chop the code around too...)

Which code optimizations?

In a pure language, substituting a function call with the corresponding RHS is guaranteed to not alter the program. Eliminating common subexpressions is guaranteed not to alter the meaning of the program. Something like stream fusion which replaces a data structure in memory with a loop in the program code is guaranteed not to alter the meaning of the program. Should I continue? On the other hand, turn up the optimisation settings on a C compiler high enough and the program breaks. Somewhere the compiler elides a second call to a function which actually happens to have some side-effect that the compiler isn't aware of, and your stream is now one byte out of alignment, or whatever. Fiddling with optimisation settings in GHC may make your program slow to a crawl rather than go faster, but it *never* makes it segfault on startup.

...

From a different point of view, whole program compilation gives plenty of opportunity for re-ordering transformations / optimization - Stalin (now Stalinvlad) and MLton often generated the fastest code for their respective (strict, impure) languages Scheme and Standard ML.

I didn't say it's impossible to optimise impure languages. I said it's much harder.

...

2. Purity leads more or less directly to laziness, which has several benefits:

Other way round, no?

A philosopher once asked: Do we gaze at the stars because we are human? Or are we human because we gaze at the stars? Pointless, really. Is Haskell pure because it's lazy, and being impure in a lazy language would be a hellish nightmare? Or is it lazy because in a pure language, there's no reason to be strict?

...

2a. Unecessary work can potentially be avoided. (E.g., instead of a function for getting the first solution to an equation and a seperate function to generate *all* the solutions, you can just write the latter and laziness gives you the former by magic.

Didn't someone quote Heinrich Apfelmus in this list in the last week or so:

http://www.haskell.org/pipermail/haskell-cafe/2009-November/069756.html

"Well, it's highly unlikely that algorithms get faster by introducing laziness. I mean, lazy evaluation means to evaluate only those things that are really needed and any good algorithm will be formulated in a way such that the unnecessary things have already been stripped off."

Writing an algorithm custom-optimised to every possible use-case is probably more efficient than using laziness. On the other hand, using laziness is probably radically less typing, and arguably not that much slower. (And then you can invoke the notion of the Sufficiently Sophisticated Compiler...)

...

2b. You can define brand new flow control constructs *inside* the language itself. (E.g., in Java, a "for" loop is a built-in language construct. In Haskell, "for" is a function in Control.Monad. Just a plain ordinary function that anybody could write.)

Psst, heard about Scheme & call/cc?

No. Should I have?

...

2c. The algorithms for generating data, selecting data and processing data can be seperated.

Granted. But some people have gone quite some way in the strict world, e.g.:

http://users.info.unicaen.fr/~karczma/arpap/FDPE05/f20-karczmarczuk.pdf

...

2d. Parallel computation. This turns out to be more tricky than you'd think, but it's leaps and bounds easier than in most imperative languages.

Plenty of lazy and strict, pure and impure languages in this survey: http://www.risc.uni-linz.ac.at/people/schreine/papers/pfpbib.ps.gz

All of these seem to be of the form "you can do this in an impure language". I didn't say you can't. I said it's easier.

...

3. It's much harder to accidentally screw things up by modifying a piece of data from one part of the program which another part is still actually using. (This is somewhat similar to how garbage collection makes it harder to free data that's still in use.)

In a pure language I'd like to think its impossible...

Agreed. But - unless your program involves no I/O at all - you would be wrong... :-( Haskell programs can and sometimes do involve mutable state internally as well. And in that case, it's up to you to not accidentally do something dumb.

On Thu, Dec 10, 2009 at 4:42 PM, Stephen Tetley wrote:

C'mon Andrew - how about some facts, references?

2009/12/10 Andrew Coppin :

...

1. Code optimisation becomes radically easier. The compiler can make very drastic alterations to your program, and not chance its meaning. (For that matter, the programmer can more easily chop the code around too...)

Which code optimizations?

Anything permitted by free theorems for one. That gives you a whole lot of code motion possibilities. Purity also gives the compiler freedom to increase sharing. It lets GHC rely on 'almost correct' ways to evaluate thunks on multiple cores with blackholing that has a vanishingly small but still existent race condition, which is FAR faster than the version they would have to use if they were more concerned about accidentally duplicating effects.

...

From a different point of view, whole program compilation gives plenty of opportunity for re-ordering transformations / optimization - Stalin (now Stalinvlad) and MLton often generated the fastest code for their respective (strict, impure) languages Scheme and Standard ML.

Feel free to check the last page of the report here before replying with the Shootout - (GHC still does pretty well though easily beating Gambit and Bigloo): http://docs.lib.purdue.edu/ecetr/367/

...

2. Purity leads more or less directly to laziness, which has several benefits:

Other way round, no?

Laziness pushes you in the direction of purity, if only because it provides you with the freedom you need to recover usable efficiency, but I would argue that the converse is also true to some extent. When you are designing a pure language, you can't do as much in a strict setting as you can in a lazy setting. Laziness allows you to tie the knot without mutation -- or rather using only the mutation intrinsic to thunk-evaluation in call-by-need. A pure strict language is also often faced with some kind of fun/val distinction, leading to ml like syntactic warts, and eta-reduction isn't always sound, so EDSLs wind up carrying extra ()'s or need pointful plumbing ala f#'s |>.

...

2a. Unecessary work can potentially be avoided. (E.g., instead of a function for getting the first solution to an equation and a seperate function to generate *all* the solutions, you can just write the latter and laziness gives you the former by magic.)

Didn't someone quote Heinrich Apfelmus in this list in the last week or so:

http://www.haskell.org/pipermail/haskell-cafe/2009-November/069756.html

"Well, it's highly unlikely that algorithms get faster by introducing laziness. I mean, lazy evaluation means to evaluate only those things that are really needed and any good algorithm will be formulated in a way such that the unnecessary things have already been stripped off."

I mean, lazy evaluation means to evaluate only those things that are really needed and any good algorithm will be formulated in a way such that

Continuing that quotation seems to say quite the opposite. the unnecessary things have already been stripped off. But laziness allows to simplify and compose algorithms. Not only that but the surrounding example is the classic 'take 5 . qsort', which DOES change its asymptotics in the face of laziness. When you are writing the algorithm from scratch, I agree that it is the case that you probably derive nothing from laziness. The nice thing about laziness is that it permits you to avoid this tedium and makes it easier to grab a widget from the standard library and just have it suit your purposes. Another non-intuitive asymptotic changing difference is that laziness provides a side-effect free way to describe memoization and dynamic programming over certain domains. http://apfelmus.nfshost.com/quicksearch.html

...

2b. You can define brand new flow control constructs *inside* the language itself. (E.g., in Java, a "for" loop is a built-in language construct. In Haskell, "for" is a function in Control.Monad. Just a plain ordinary function that anybody could write.)

Psst, heard about Scheme & call/cc?

To be fair, most scheme control structures are implemented using macros, and call-by-macro-expansion is a form of call-by-name: http://en.wikipedia.org/wiki/Evaluation_strategy#Call_by_macro_expansion

...

2c. The algorithms for generating data, selecting data and processing data can be seperated. (Normally you'd have to hard-wire the stopping condition into the function that generates the data, but with lazy "infinite" data structures, you can seperate it out.)

Granted. But some people have gone quite some way in the strict world, e.g.:

http://users.info.unicaen.fr/~karczma/arpap/FDPE05/f20-karczmarczuk.pdfhttp://users.info.unicaen.fr/%7Ekarczma/arpap/FDPE05/f20-karczmarczuk.pdf

Given. But then people have written some amazing things in brainfuck too. That doesn't mean that I want to subject myself to working in such a sufficient computing environment :) -Edward Kmett

-Edward Kmett On Mon, Dec 14, 2009 at 2:20 PM, Jason Dusek wrote:

2009/12/14 Edward Kmett :

...

[...] That doesn't mean that I want to subject myself to working in such a sufficient computing environment :)

Sufficient?

That word was meant to be surrounded by big sarcasm quotes. By sufficient I meant that it is Turing complete, and so in some sense sufficient to general purpose programming -- even if it is not a desirable environment in which to code. -Edward Kmett

On Friday 11 December 2009 3:24:03 am pbrowne wrote:

The issue of *purity* in Haskell and this thread has confused me.

At value level (not type level) is this linked with *equational reasoning*? Are the operational semantics of Haskell similar but not the same as equational logic?

Why are theorem provers such as Haskabelle need? http://www.mail-archive.com/haskell-cafe@haskell.org/msg64843.html

The use of equational reasoning in a language like Haskell (as advocated by, say, Richard Bird) is that of writing down naive programs, and transforming them by equational laws into more efficient programs. Simple examples of this are fusion laws for maps and folds, so if we have: foo = foldr f z . map g . map h we can deforest it like so: foldr f z . map g . map h = (map f . map g = map (f . g)) foldr f z . map (g . h) = (foldr f z . map g = foldr (f . g) z) foldr (f . g . h) z now, this example is so simple that GHC can do it automatically, and that's a side benefit: a sufficiently smart compiler can use arbitrarily complex equational rules to optimize your program. But, for instance, Bird (I think) has a functional pearl paper on incrementally optimizing a sudoku solver* using equational reasoning such as this. Now, you can still do this process in an impure language, but impurity ruins most of these equations. It is not true that: map f . map g = map (f . g) if f and g are not pure, because if f has side effects represented by S, and g has side effects represented by T, then the left hand side has side effects like: T T T ... S S S ... while the right hand side has side effects like: T S T S T S ... so the equation does not hold. This is all, of course, tweaking programs using equational rules you've checked by hand. Theorem provers are for getting machines to check your proofs. Hope that helps. -- Dan * If you check the haskell wiki page on sudoku solvers, there's an entry something like 'sudoku ala Bird', written by someone else (Graham Hutton, comes to mind), that demonstrates using Bird's method.

On Fri, Dec 11, 2009 at 10:04 AM, pbrowne wrote:

Two questions 1) Is this correspondence between operational and logical semantics a desirable property of *purity* in the Haskell world?

2) What, if anything, prevents the execution of a Haskell term from being a proof in equational logic?

It seems that Haskells type system has this logical purity[4]

My motivation for such questions is that I am researching various *algebraic styles* such as Haskell, OCAML, Maude, and CafeOBJ. My current general research question is; how closely do executable terms in these languages match their *logical* meaning. For example, languages like Java need additional logical scaffolding (like JML[3]) to give them logical machine readable meaning.

I admit that I don't fully know what you are talking about. What do you mean by logical meaning -- as opposed to what other sort of meaning? The equational reasoning in Haskell comes from its denotational semantics (which, mind, is not completely formally specified -- but once you expand typeclasses to dictionary passing style, you get a standard DCPO semantics). If terms are equal in denotation, then they are equal by observation (modulo efficiency). So it is not equations that directly define the semantics of Haskell, but rather mapping the syntax to mathematical objects. We derive Haskell's equational reasoning from the equational reasoning in the semantic domain. That's how I see it as a user of the language. At the most abstract level, omitting some of the practical details of the language (such as the built-in numeric types), Haskell's reduction follows beta reduction with sharing, and so at that level I think the answer to (2) is "nothing". Luke

I *guess* that the gap between operational and logical semantics is rather less in Haskell that in Java, and I further *guess* that the gap less again in Maude or CafeOBJ. I think a good answer to question 2) would remove the *guess* from the Haskell case.

Pat [1] http://rewriting.loria.fr/documents/plaisted.ps.gz [2]http://www.forsoft.de/~rumpe/icse98-ws/tr/0202Diaconescu.ps [3] http://www.eecs.ucf.edu/~leavens/JML/ [4]http://www.haskell.org/haskellwiki/Type_arithmetic

Dan Doel wrote:

...

The use of equational reasoning in a language like Haskell (as advocated by, say, Richard Bird) is that of writing down naive programs, and transforming them by equational laws into more efficient programs. Simple examples of this are fusion laws for maps and folds, so if we have:

    foo = foldr f z . map g . map h

we can deforest it like so:

    foldr f z . map g . map h       = (map f . map g = map (f . g))     foldr f z . map (g . h)       = (foldr f z . map g = foldr (f . g) z)     foldr (f . g . h) z

now, this example is so simple that GHC can do it automatically, and that's a side benefit: a sufficiently smart compiler can use arbitrarily complex equational rules to optimize your program. But, for instance, Bird (I think) has a functional pearl paper on incrementally optimizing a sudoku solver* using equational reasoning such as this.

Now, you can still do this process in an impure language, but impurity ruins most of these equations. It is not true that:

    map f . map g = map (f . g)

if f and g are not pure, because if f has side effects represented by S, and g has side effects represented by T, then the left hand side has side effects like:

    T T T ... S S S ...

while the right hand side has side effects like:

    T S T S T S ...

so the equation does not hold.

This is all, of course, tweaking programs using equational rules you've checked by hand. Theorem provers are for getting machines to check your proofs.

Hope that helps. -- Dan

* If you check the haskell wiki page on sudoku solvers, there's an entry something like 'sudoku ala Bird', written by someone else (Graham Hutton, comes to mind), that demonstrates using Bird's method.

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

Luke Palmer wrote:

I admit that I don't fully know what you are talking about. What do you mean by logical meaning -- as opposed to what other sort of meaning?

Consider Maude's rewrite logic RWL[1] which has similar inference rules as equational logic(EL), but without the symmetry rule. From [1], the *logical* meaning in RWL regards the rules of rewriting logic as meta-rules for correct deduction in a logical system. Logically, each rewriting step is a logical entailment in a formal system. Note that the particular logic may vary (e.g. EL,FOPL, RWL). [1]http://maude.cs.uiuc.edu/maude1/manual/maude-manual-html/maude-manual_62.htm...