What is a monad?

[tufty]

Doesn't Gödel come round to bite you on that one?

It shouldn't do - there are certain base functions that you have to take to be axiomatic. My formal logic's not so good though.

As I understand it, though, it simply doesn't matter if you can take the base functions as axiomatic. I'm fairly sure it still hits Gödel's second theorem, the whole thing about it being possible to construct unprovable theorems within any sufficently complex axiomatic system. But I may be wrong

[foxyloxy]

It doesn't matter. The problem with the formal specifications used to reason about computer programs come with recursion/looping, and reasoning whether your series will terminate/converge.

You generally get around it by reasoning about everything but the loop/recursion (e.g. if x holds before the loop, then y will hold afterwards, providing the loop terminates), or by formalising certain kinds of 'always terminating' structures, or by eliminating looping/recursion altogether (my favorite solution )

It's suprisingly easy to accidently create a complete system, even when you're trying really hard not to Self-reference is a pain throughout discrete mathematics.

[tufty]

Oh, absolutely. My main point was that I believe teamonkey's statement that ...

If you work in a purely functional style then you can actually prove mathematically that a program will do what you intend it to.

...is only true for a subset of valid programs, whether you program in a functional style or not, although functional programming makes it easier to prove that the subset in question will do what you want them to do.

[piku]

Is it me or is this whole Haskell/monads thing is a waste of time. Its like "Lets come up with so convoluted methods to program in, and call it something strange". It seems to add no value what so ever to current programming paradigms

Maybe it's a waste of your time. Haskell was designed by researchers as a common language for research in pure functional programming, and it has succeeded beautifully in that respect. Also, don't forget that a lot of concepts that are mainstream today were seen as convoluted in the beginning. For instance: object-oriented programming, local variables. And modern languages such as C# 3.0 or Ruby owe a lot to functional programming.

I remember being forced to learn a pure programming language at university called Miranda. It required a certain mindset you had to switch into before you could start getting it to dance. I suspect if you were that type of person, or had come from the correct background (Pure Maths?) it would of been easier for you. The most difficult part was coping with the lack of temp. storage variables and thinking in terms of recursion (which not all problems lend themselves easily to a solution in this vein, if many)

But I'm with sdetoni on this one, what really are the practical benefits of writing in such a language, who really uses this? In the world I come from I write windows applications & websites, I implement everything in nice neat classes.. obviously from my point of view writing something like this would be near impossible in a pure language, but what else can you do with such a creation? a real world example.

This is what I kept banging into when I was at Uni. They tried to teach us Formal Methods using the rather tricky Z Notation (set theory on acid). It also required shifting mental gears before it made sense.

We used to cook up state machines and small systems with it, one assignment being to create a state machine and associated proof for a digital watch.

From someone who writes windows apps and websites, using classes and things, it's quite abstract and alien. I never really saw the point, it didn't appear to be the way the world worked. Maybe if I were writing nuclear power control software I'd seek out to prove the software was correct, but your average windows software isn't that vital.

[teamonkey]

In theory, the rules governing mathematical proof will apply to any purely functional program. You can prove that two functions are equivalent (e.g. for optimising), or that a program behaves exactly like a mathematical formula, or that for a given range of inputs you will get a given range of outputs. The "subset of valid programs" you mentioned are purely functional ones, at least for proofs of this nature.

[tufty]

In theory, the rules governing mathematical proof will apply to any purely functional program. You can prove that two functions are equivalent (e.g. for optimising), or that a program behaves exactly like a mathematical formula, or that for a given range of inputs you will get a given range of outputs. The "subset of valid programs" you mentioned are purely functional ones, at least for proofs of this nature.

That's the thing though, isn't it.

Given a programming system X, we can posit 2 types of programs. those which are "valid" or purely functional, and those which are "invalid" or not purely functional. We'll ignore the "invalid" programs.

Now, programming system X is, as you rightly point out, an axiomatic system, so any valid programs in X must build solely on the axioms at the base of the system.

Let us posit also that X provides axioms (or allows us to derive new programs) which are equivalent to the axioms of a given subset of mathematics, M. We can therefore treat that subset of axioms and programs as the axioms of a meta-system, X'.

It therefore holds that any valid program *solely* constructed using the "axioms" of X' must have an equivalent formulation in M. In short, X' is equivalent to M. anything you can prove in M, you can prove in X', and vice versa. Right?

However, Gödel tells us that of all the possible theorems T in M (where M is sufficiently complex[1]), there must exist a subset of theorems T' which are valid but not provable. And, as X' is equivalent to M, that subset must also exist in X'

I think.

Simon

[1] Capable of expressing Peano arithmetic, if memory serves.

[piku]

Is it time to read this book again?

[teamonkey]

I don't think it's so complex that Godel needs to enter in to it, to be honest. I mean, the objective here isn't to prove that Peano's* axioms are provably true, it's to show the correctness of your program given a set of accepted axioms regardless of whether they can be formally proven or not (hey, I'm a physicst: proof beyond reasonable doubt is more than good enough for me ).

Lambda calculus is a mathematical system and a pure functional language is essentially syntactic sugar around lambda calculus (what a turing machine is to an imperative language, lambda calculus is to a functional language). So in essence you can reason about your program as you would a mathematical formula and most usefully show that two functions are equivalent (or not) even though they're constructed differently.


*