User:Uchchwhash

I am Imam Tashdid ul Alam, a physics undergrad at UNSW, Australia, but by the looks of my monotonically decreasing grades, I'm not sure for how long I will be there.

A Haskell enthusiastic, a forever newbie, I don't do Haskell partly because I never took a computing course (officially), and partly because Haskell is cryptic. Yes, cryptic. Even though it has the most lucid lexical and syntactical structure.

I write Java code occasionally (again, for no particular reason, this "new generation"... they are so... lost!) and therefore crave for the functional approach.

My love for Haskell is difficult to explain, I know that because I tried to explain it to my friends every now and then, but I think the reason is that Haskell was the first programming language I came across that took the propositions-as-types (or programs-as-proofs) principle seriously.

So here is my own understanding and criticism of the language.

Errors

Part of life (...sigh...). Haskell is particularly rough here, as far as I can tell. Whenever there is an error "I don\'t know what to do here!" occurs, the program terminates abruptly. This is bad.

Bad, both computationally and logically. Under the isomorphism, $\bot$ ("bottom", or, it's counterpart in Haskell undefined, equivalent to non-termination), is reminiscent of an error. Behold! error and undefined have the respective types a and String -> a, which is not at all funny. If you can prove absurdity (if you have a value of a type that is not inhibited) then you can prove everything, they say.

The designers of Haskell seems to have concluded that making the language logically sound is too hard and they should give it up. They were right.

Now, when you cannot return a value, what type would be the returned value then? Obviously it should have the type $\bot$, which does not have a value. So in Haskell, it makes sense to type it as a, as you better leave any attempts to type it, since there is no type called $\bot$, and there is no type without a value (but... but...)

It just struck me that contructive type thoery is not necessarily extensional. Instead of having just one bottom you can have several phantom types, each one being a distinguishable error. I was so inspired by Ben Rudiak-Gould et al's Haskell is not not ML paper (and Philip Wadler's dual calculus), but nobody seems to be too serious about them. To be totally honest, I have no clue what they talk about.

Even then, my pricipal motivation for going through this pain of writing this down is that in Haskell we have a computing interpretation of all the logical operators (although, interpreting $\land$ is a bit vague because of currying), bar the $\neg$. Why be partial? :-)