Daniel Fischer wrote:

I don't have a CS degree either, so someone please correct me if I'm wrong (or confirm if I'm right). In Haskell, reducing a term to whnf (which e.g. seq is for) means evaluating it far enough that its top level constructor is known (or it's found to be bottom). For some types like Int, that means complete evaluation, for others it's far less. A list is in whnf if you know whether it's bottom, [] or h:t, where you might or might not know something about h and t. A Maybe term is in whnf if you know if it's bottom, Nothing or Just whatever. A function is in whnf if you know if it's bottom or \x -> rhs.

That's correct, but be careful with your use of the term bottom. Most bottoms are never "found to be bottom", but instead, the program runs forever trying to find the top-level constructor. Another thing: you do not need seq to evaluate something to whnf, you can just pattern match on the top-level constructor instead. seq is there for polymorphic values where you cannot pattern match since you don't know the possible constructors. Pattern matching is the main mechanism in Haskell to trigger evaluation. Tillmann

Daniel Fischer wrote:

Distinguish between findable and unfindable bottoms? The difference in practice is clear, but is there also a theoretical difference?

That depends on the theory you choose. If you're only interested in non-bottom results anyway, you can choose to use a simple theory (that is: a simple formal semantic) which doesn't distinguish between non-termination and other errors. If you're interested in modeling error-handling, you should probably use a semantic which does distinguish different kinds of errors. A denotational semantics which takes errors into account could use the error monad similar to how you use it in Haskell for explicit error handling. In fact, monads in CS where first introduced for denotational semantics, before they where applied to functional programming. That means that you have a choice: Avoid findable bottoms by using explicit error handling with error monads in your program, so that you can use a simpler semantics to understand your code. Or use findable bottoms to encode errors, and use an error monad to upgrade your semantics to cope with them. I prefer to use the monads in my Haskell code, and not in my head (where the semantics is processed in the code understanding cycles of my programming process). Tillmann

Am Mittwoch, 27. August 2008 18:43 schrieb Rafael Gustavo da Cunha Pereira Pinto:

...

You can find a definition at http://burks.bton.ac.uk/burks/foldoc/53/126.htm It's not entirely helpful if you don't know some lambda-calculus.

Thanks Daniel,

Is there any easy to follow Lambda Calculus (intro-level) tutorial?

I don't know any :( The wikipedia article might be helpful and also some of the links at the bottom. I took a look at some of them and found none entirely convincing, but also none definitely bad. Cheers, Daniel