Strong functional programming | Hacker News Reader

Strong functional programming

etorreborre.blogspot.com.au

83 pointsDanielRibeiro18 comments

Here is some relevant discussion: http://lambda-the-ultimate.org/node/2003

Also, codata doesn't solve everything. You still can't filter infinite data. Filtering with \x -> x > 0 won't terminate for all infinite lists of numbers since [0 0 0 0 0 ...] is a potential case.

Interesting. I am not that familiar with ML languages, but isn't the situation equivalent to division by 0 in arithmetic? Division by 0 is undefined, because assigning it to any natural number would yield a contradiction. Alternatively, one could define x/0=⊥, like Haskell does, but then every other operator in arithmetic would have to handle ⊥.

Mathematicians have chosen to keep division by 0 undefined (except in special contexts), and I am inclined to agree. I suspect that the primary reason for the existence of ⊥ in Haskell is because of the Hindley Miller type system's insistence on giving a type to everything.

Any comment appreciated.

⊥ exists because you can't easily write a program that doesn't have it. If Haskell didn't provide an "error" or "undefined" function, you could just write "undefined = undefined" and use that. Short of guaranteeing termination (which you can't do in a fully general language), you can't eliminate ⊥ from the language.

That said, I often wish that Haskell would learn something from the Java world and require all functions intentionally throwing an exception to have an explicit "throws" specification as part of the type. Then, you could use the type system to require catching exceptions, and treat any unexpected exception as cause for an immediate abort.

Java has a type and effect system. Methods return type * effect - this causes problems, a big one in Java is that effects can't be polymorphic.

Anyway, I wouldn't like to see an effect system in Haskell (though, seems like Scala is getting one). We already express IO and State as a type. How about we express exceptions as types? Easy:

http://hackage.haskell.org/packages/archive/mtl/1.1.0.2/doc/...

Java has two types of exceptions: checked exceptions and runtime exceptions.

In Haskell, there is a parallel to this: things like error and undefined are much like runtime exceptions. They are what you would use for conditions that should never come up like division by 0 or infinite loops. You wouldn't want to have to deal explicitly with potential errors every time you used division--it would be useless in most cases. The default behavior with these is to immediately abort.

Haskell also has a parallel to checked exceptions: Either (also Maybe and ErrorT and probably others). If a function returns an Either value, it forces you to check whether the result was valid using the type system, just like a checked exception. So `int f(int a) throws SomeError` can be written as `Int -> Either SomeError Int` in Haskell.

The Haskell approach actually has some advantages, mainly stemming from the fact that Either is not baked into the language. This means the type system can be simpler: in Java, you have both the return value and the "effect" (e.g. throws), which are different concepts with the latter baked into the language and inflexible; in Haskell, you just have a different return type that is defined in a library. This also gives you greater flexibility: you can easily encode your own "effect" by defining your own type, and it can behave in the same way as Either.

There are also IO exceptions, but I haven't actually used them for anything, so I can't say much about them.

I do agree with you that you can encode exceptional conditions via mechanisms like Either, Maybe, and ErrorT; similarly, you can encode C errors via return values, NULL pointers, and errno. However, ever so often you still run across a Haskell library that decides to use exceptions for error handling, and in such cases, the types do not tell you what exceptions can occur. I'd argue that having those exceptions encoded in the type would make sense as well.

If Haskell's "runtime exceptions" only existed to abort the program, and you couldn't catch them, then I'd agree that encoding them in the type doesn't seem necessary. However, since you can catch them, and often do need to, encoding them in the type would help.

So your request is that Haskell force programmers to not throw unchecked exceptions when a checked type could work? That's a PEBKAC, not a language issue.

Not my point at all. I like the Haskell exception system for some types of error handling, and I think in some cases it works better than Either, ErrorT, or similar mechanisms. I'd still like to have those exceptions reflected in the type. That doesn't mean I'd like an Either or an ErrorT; those don't work like thrown exceptions.

The Haskell approach sounds pretty neat. How well does it work in practice? I thought that C++ introduced exceptions to get away from having to check every single return value, and to be able to handle the condition at the appropriate caller level.

It actually works rather well in practice. `Either` and `Maybe` are monads. In hand-wavy terms, this means you can control how functions returning Either values (that is, functions that can have an error) are composed. This means that the semantics for propagating an error are basically encoded in the `Either` type.

In practice, this means that if you have code that should either act on a valid value or just return the error if given an error, you don't have to write anything special at all. A concrete example: let's imagine yourFunc needs to get a bunch of values that could be errors; you could write code like this:

     do a <- couldError "1"
        b <- couldError "2"
        c <- couldError "3"
        return [a, b, c]

This will then work much like an exception: if either a, b or c are an error, the end result will be that error; if they are all normal values, the end result will be a normal value. You only ever have to pattern match when you want to handle errors in some different way and extract the normal type from the Either type. This is exactly the same as a catch statement for exceptions.

Since these types are first-class citizens, it's also really easy to add other functions to operate on them. For example, you can use the existing <|> operator to alternate between possible cases.

    result = one <|> two <|> three <|> Left "all failed"

(Left is the part of Either that is used to hold errors; the reason it isn't named error is that Either can actually be used for other sorts of control flow as well.) This code will return the first of one, two, three that is not an error or give you "all failed" as the error.

Another useful function is `optional`. This does exactly what it sounds like: it allows you to mark some particular function as "optional", so that if it errors out that error gets ignored.

I think code like this is clearer and easier to read than the alternative with exceptions would be.

However, the important part is not the particular functions, but that you can add your own. Both <|> and optional are library functions that are not even specific to error handling--they work on a bunch of other types like parsers.

I think having error handling be first class like this is very useful and makes writing code with it much nicer.

Note that bottom is a theoretical concept. If you actually evaluate (1/0) in the haskell interpreter, you get an error message

   *** Exception: Ratio.%: zero denominator

Similarly, if you run an infinite loop in the interpreter, it just loops forever. (Well, in certain special cases it can figure that out and throw an exception). The implementation never creates an actual "bottom" value that has to be handled by e.g. arithmetic operators.

The issue of bottom comes up when you try to define precisely what the meaning of a program is (in the jargon, when you give a denotational semantic). It is clear that the expression (1+1) should "mean" 2, but what is the meaning of an infinite loop? Answer: a special "error value" which we call bottom.

You may wonder why most traditional mathematics doesn't make a fuss about bottom values, and just get away with saying "this is a partial function". This is because most everyday mathematical functions are defined by e.g. simple structural recursion, so issues of termination are seldom very complicated. Once you have general recursion, you need to be more careful.

Thank you, that cleared things up.

Does Haskell allow you to assert that a function (like, say, the Sieves of Eratosthenes algorithm) does terminate, so that it may use that info to make additional simplifications?

That's a good question that i had previously noted for followup, but I never followed up.

slide 50: how does agda check termination.

http://www.seas.upenn.edu/~sweirich/ssgip/main.pdf

http://research.microsoft.com/en-us/news/features/terminator...

Not exactly. There's multiple types to divide by multiple kinds of zero, and multiple ways to accomplish it. Remember they're Num, they're not integers

http://stackoverflow.com/questions/9354016/division-by-zero-...

http://www.reddit.com/r/haskell/comments/m7agm/why_doesnt_ha...

I don't know if anyone else noticed, but I appreciated this little joke from the article: in saying that 0 = 1 "allowed you to prove anything" he created a circular reference from the article to itself and then stated that the reference itself evaluated to `#fail`. :D

One of my web dev bosses talked a lot about how nobody really needs Turing completeness and how most data-processing algorithms really just do a case dispatch on a structured non-recursive data set, so that you can quickly prove that it halts and be done with it. It was persuasive, and we wrote our data structures in terms of themselves, but I am not sure that I would want to write in a programming language designed for that. I'm glad that HTML and CSS halt, for example; but I'm glad that when I want to write a recursive factorial program in JS that it doesn't blow up.

I'm still working my way through what this all looks like in Haskell. Thanks for linking it!

Edit: this is the second greatest infinite loop ever:

    data Silly a = Very (Silly -> a)
    bad a :: Silly a -> a
    bad (Very f) = f (Very f)
    ouch :: a
    ouch = bad (Very bad)

It is second only to the infinite loop in Chef: "Bake the potato. Wait until baked."

Hmm... it may be a little too late to comment on this and still be noticed, but from what I understand, not all forms of recursion are created equal, and you can do most things using total functions, that can be guaranteed to terminate. In fact, the compiler can check it automatically without any modification to your code, using a couple of known proof strategies, the simplest ones being inductive and lexicographic convergence.

[slightly OT] Does anyone think that Implicit Computational Complexity should be explored in some "real" programming language?

Although current achievements are probably far away from being really meaningful in practice, I see some potential. For instance, I think it would be cool for a cloud provider to have bounds on the running time of programs sent by clients, just because code is written in a certain language.

If we equate haskells Int type to a mathematical integer, then (loop 0) -> 1 + 1 + ...

1 + 1 + ... = 1 + (1 + 1 + ...)

We can still use equational reasoning, it's just that equational reasoning is different for divergent non-terminating equations

Reply on news.ycombinator.com