God, get the frak out of my Barne's and Nobel section.

Scientists, please, I beg you, stop with this God vs Science bull already.

I went into my local Barne's and Nobel today, and started to casually browse through my favorite section of the bookstore--

The Science Section.

Last time I checked, Books about God fell under the "Religion" category. Furthermore, I am pretty sure that Science, in fact, is not religion. Now, I like reading philosophical books, religious texts, etc, just as much as the next guy -- heck, I even like reading things like the Bible or the Koran. But why the hell does my community feel it necessary to invade on religion's ground? Leave God alone, I don't want to hear about him, I don't want books about him in my section of the bookstore.

Scientists reading this right now are screaming something like, "But Jooooe! They do it to us all the time!!!" Here's my reply, Let them. If they feel that they, in order to be validated, need to shove their beliefs down other peoples throats, treat them like they act. You don't get a toddler to stop whining about not getting what they want. Religious types want you to believe what they believe. The way you teach a toddler to stop crying about not getting their way is by letting them cry themselves out. If you continuously argue with them, they will lose. The people slamming science don't take time to be unbiased about science, and unfortunately, I think that most of the people slamming Religion back are not taking the time to be unbiased about religion either. Aren't we, as scientists, supposed to be unbiased about all ideas?

I'm annoyed that people who call themselves scientists are wasting there time on this whole God business, I'm annoyed that the religious community isn't reigning in the idiots who are stepping outside there bounds. It's a community's responsibility to regulate itself. So, Science community, consider yourselves regulated. Religious community, take a hint.

~~Joe

Annoyances with Blogger.

I'm Mildly annoyed that blogger does not seem to recognized that when I put in some indented code, it replaces things with &nbsp's and other gibberish. The same thing occurs with other punctuation. It's bothersome.



C'est la vie.





~~Joe

Programming Languages Part I: Syntactic Similarity

I like languages. when I was younger, I remember reading The Hobbit and spending more time reading the first two preface pages about the Moon Runes, A gussied up version of the Futhark, than actually reading the book. For a good bit of time after that, I wanted to be a Linguist, and not a mathematician.

But Alas, over time my interests went from Natural Language to Formal, from Formal Language to Abstract Language, and from there to the wide world of Algebra and Logic. A good transition, I think. Nevertheless I still love Languages, and that love has now been turned to specifically Programming languages. I like these languages because they are first and foremost utilitarian. They are designed from the start to do one thing, get a point across to an idiot. Lets face it, Programmers and Computers alike are pretty damn dumb. The language is the smart thing. A Programmer has no capability to tell a computer what to do without the help of a good language, and a Computer can't do anything it isn't told to do. So the most fundamental piece of Computer Technology is that of the Language, the layer that binds Programmer with Programmee.

I love languages, but I often hate them too. Take, for instance, Java. Java is an exceptionally pretty language, but it's also ugly as your Aunt Anita Maykovar (May - ko - var). Java effectively boils down to one syntactic structure, the class. Every Java file revolves around it, and in some ways, this is really good. The fundamental commonality this structure brings allows Java code to be easier to learn to read. Your brain is good at processing things that are similar, the pathways it has to draw are all about the same-- so it's easier to optimize up there. The issue I have with Java actually is that, sometimes its too good at looking the same. To the point where I forget where I am. I get lost in my own neural pathways while I try to figure out whether I'm looking at an Abstract class or an Interface, or if I'm looking at a dirty hack of a databearing class or if I'm looking at something more legitimate. C/C++ is great at making this distinction, but it's also, IMO, ugly as shit, uglier even. I like C often for its ability to compartmentalize things, but I think it takes it to far, nothing looks alike, even if it should. One of my peeves with C vs Java is they're taking extreme views on something which should be easily decided. I'd like to sum it up as a fundamental rule I want to see in all programming languages (though that will probably never happen). Here it is:

Syntacticly similar things should be Semantically similar things, and vice versa, according to the proportion of similarity.

That is, If I want to create an object called "List" which implements a linked list, and then I want to create an interface (which is really just a Type Class, I've come to realize, but thats a story for another day.) called "Listable" which, when implemented, forces a object to have list-like properties. These things should have some similar structure. However, this is not to say we should copy Java. Java takes this too far, I think. In that, Java follows the rule: "If things are Semantically similar, they are Structurally almost Identictal." This is bad, Interfaces should look different than Classes, but only in a minor way. I'd like Java Interfaces, heck, Java in general if I could specify type signatures ala Haskell. I think Haskell has got it right when it comes to how types should work syntactically. The brilliance of this comes in when you try to write a Java Method with this Type Sig ala Haskell type syntax, here's Fibonacci:

fib :: public, static :: int -> int

fib(nth) {
(nth == 1) ? 1 : fib(nth-1) + fib(nth-2);
}

(I think that'll work, but it's been a while, so I might have it wrong.)

Granted, there are issues with this. Notably, Java has things like side effects, but these could be built into the type signatures. I think that the ultimate benefit of this kind of type signaturing is a separation of concerns syntactually. I think that overall, this would make the language as a whole a lot cleaner. As interfaces would no longer have stubs like:

public static int fib(int nth);

which, though nice, doesn't carry the same amount of information that could be held in something like:

fib :: public, static :: int -> int

Syntactually, the latter structure is more extensible, it could allow for the incorporation things like side effect tracking, or thread signatures, which might look like:

fib :: public, static, threaded :: int -> (int, int, ...) -> int

which says that effectively fib is a method with takes a int to a unspecified number of threads, to an integer.

I'm really just spitballing at the end here, with some neat ideas I think that a small change in Java's syntactic structure could bring.

Just my thoughts.

PS: I don't know if the Syntactic/Semantic Similarity rule is well known, but either way, its a damn good idea.

Haskell: The Good, Bad, and Ugliness of Types

I've started to learn Haskell, for those who don't know, Haskell is a wonderful little language which is based on Lazy Evaluation, Pure Functional Programming, and Type Calculus.

Effectively, this means that, like Erlang and other sister languages, If I write a function foo in Haskell, and evaluate it at line 10 in my program. Then I evaluate it again at Line 10000, or 10000000, or any other point in my code. It will-- given the same input-- always return the same value. Furthermore, if I write a function to generate an arbitrary list of one's, like this:

listOfOnes = 1 : listOfOnes

Haskell just accepts it as valid. No Questions asked. Schemer's and ML'ers of the world are probably cowering in fear. Recursive data types are scary in an Eager language, But Haskell is lazy. Where the equivalent definition in scheme:

(define list-of-ones
(cons 1 list-of-ones))

would explode and probably crash your computer, (that is, if the interpreter didn't catch it first.) in Haskell, its not evaluated till its needed, so until I ask Haskell to start working on the listOfOnes structure, it won't. I like Languages like that, IMO, if a language is at least as lazy as I am, its good.

The third really neat thing about Haskell, and what really drew me to it in the first place, is the Type Checker. I've used Scheme for a while now, and I love it to death. Sometimes, though- Scheme annoys me. For instance, I was working on a function like this once:

;count-when-true : [bool] x [num] -> num
;supposed to be a helper for filter, I want do a conditional sum. So I pass in (filter foo some-list-of-numbers) and some-list-of-numbers,
; and I should get out a sum of the elements
(define (count-when-true list-of-bools list-of-numbers)
;or-list : ([a] -> bool) x [[a]] -> bool
;applys a filter across a list of lists and ors the results
(cond [(or-list nil? (list-of-bools list-of-numbers)) 0]
[(car x) (+ (car list-of-number) (count-when-true (cdr list-of-bools) (cdr list-of-numbers)))]
[else (count-when-true (cdr list-of-bools) (cdr list-of-numbers))]))

This probably has bugs in it, doesn't work right, etc. but the idea is to return a conditional sum, now. I want to use this on lists, thats how its defined, but sometimes the calling function would try to call it on atoms, instead of lists. Big problem? not really, pain in the ass to find, you bet. The issue was, when I was trying to figure out what was wrong, Scheme didn't realize that the type of the inputs were wrong. This would have made the error obvious, but Scheme doesn't care about types, thats it's principle strength, until it starts making bugs hard to find. I HATE it when its hard to find bugs.

Lets face it, as programmers, we suck, we write lots of buggy functions, things are generally done wrong the first (two or three... thousand) times. Programming is a recursive process, we write some code, run it, check for bugs, fix bugs, run it, check, fix, etc. Until we get tired of finding bugs/the program doesn't come up with any. IMO, languages should not be designed to force programmers to write bug-free code, which seems to be the consensus today. At least, thats what I gather from the interweb and such. The goal should be to make all bugs so blatently obvious, that when the programmer sits down and trys to debug his program, he can't help but to smack himself in the face and proclaim, "!@#$, I missed that!" This is where Haskell Shines.

When I write Scheme, I typically don't want to be burdened by knowing which types go where. Scheme is great at this, however, it takes things to far, I think, in that it forces you to never have types. Sure, typed schemes exist, but most of them suck, because scheme isn't designed for types. Don't get me wrong, typed schemes are wicked cool, I've used types in CL too, and they're great, especially when you want to compile. So to solve the problem of not having types, we invented contracts, which are cool. For the unenlightened: a contract is a specification of what the given datastructure or function does in terms of its arguments. eg:

+ : num * num -> num
toASCII : string -> num
toCHAR : num ->; string

etc.

These can be read as follows:

literally:

+ is num cross num to num
etc

in english

+ is a function which takes two numbers and returns another number.


In Scheme, these contracts are basically comments, so Type checking is left to the programmer. This is all well and good, but I find it often leads to the practice of what I like to call single-typing. In which the programmer attempts to force all of his data to have the same type, or lists of the same type, or lists of lists, or etc. Typically, this results in convoluted datastructures which give FP in general a bad name. I've seen some horrible code written by single-typers, its bad, horrific even, It makes me want to gauge out my eyes with a pencil and tear my brain out... Okay, maybe its not that bad. Still, single-typing is most often bad. So how does Haskell fix it?

By not changing a thing.

Contracts are a wonderful Idea, they work, they just don't work in Scheme. Because it was designed that way. Haskell has type inference, you don't ever need to touch the Type Calculus capabilities of Haskell, You can-- more or less-- literally translate Scheme to Haskell with minimal difficulty. (Though, it may be easier just to write scheme in haskell.) But the brilliance of haskell is this:

Heres the Standard Factorial function in Scheme:

;Fac : int -> int

(define (fac x)
(cond [(= 0 x) 1]
[else (* n (fac (-n 1)))]))

Here it is in Haskell:

fac :: Int -> Int
fac(x)
| (x == 0) 1
| otherwise x * fac(x - 1)

(I used a ML style to make things look the same.)

The only real difference (besides some syntax changes) is the lack of the semicolon in front of the contract.

But what does all this do? Well, the difference comes during evaluation, watch this:

In Scheme:

(fac 1.414)

we have an infinite recursion, because:

(fac 1.414) -> 1 * fac(0.414) -> 1 * 0.414 * (fac -0.586) ...



In Haskell:

fac 1.414

is a type error, and the whole thing kersplodes. Over, Evaluation Done, Haskell has Denied your function the right to evaluate.

In short, you have been rejected.Enough about the wonderfulness of the Type system. My title says the Good -> Bad -> Ugliness, obviously we've seen the good. How about the Bad?

Type Errors in Haskell:

Type errors in haskell suck, easy as that. They're hard to understand, and in general, not very helpful. Further, alot of the differences between types are very subtle. For instance, consider the factorial function again, (just the type contracts for succinctness)

fac0 :: Int -> Int
fac1 :: Num -> Num


The look equivalent, right? Wrong. Num != Int, it includes Reals too.* So no lovely type errors here. These things are unfortunate, yes, but nothings really perfect. I could deal with this, but what I can't deal with is exactly the problem I hoped to solve with Haskell, My bugs are hard to find. Not only that, they're not hard to locate, I know exactly where they are, I just can't decipher the cryptic text from the Haskell error stream to know exactly what the bug is. So I have to resort to piecing through the code bit by bit, trying to figure it out.

Silly.

Type Signatures are Ugly:

I Like Contracts, but Haskell doesn't technically use them. Haskell has type signatures. Which are different.

So far, I've written contracts like this:

F : S * T * U * ... -> D

I could also have:

F : S * T * ... -> (D1, D2, ...)

or if I wanted HOF's

F : (G : X -> Y) * ... -> (D, ...)

these are all pretty easy to understand, (if you know how to read the shorthand). We know exactly what the arguments should be, elements of the set of elements of type S, or T etc. We also know exactly what the return types are, elements of the typed-set D, or ordered k-tuples of elements of typesets D1 through Dn, etc. Equivalent signatures in Haskell are:

(assuming f = F, and any capital letter is a valid type, and that ...'s would be replaced with types in the end result.)**

f :: S -> T -> U -> ... -> D
f :: S -> T -> ... -> (D1, D2, ...)
f :: (X -> Y) -> ... -> (D, ...)

Now, I understand that, since Haskell is Lazily evaluated, we want the type signatures to be heavily curried, hence the load of arrows. Honestly though, how hard is it to convert all that to a form Haskell can use? I'm not saying get rid of the arrow version, maybe just add an option to provide a "normal form" version, I shouldn't have to add these in my code as comments, solely so I can understand whats going on. I understand that the implication method more accurately reflects what the compiler is doing, but as a programmer, I don't really give a rats ass what the compiler is doing. As a mathematician,

foo :: Int -> String -> Num -> Bool

looks ugly, do I know what it means? Yes. Do I like the way it looks? No. I grasp that, as a Haskell Compiler, reading these type of signatures in makes things easier, and further, that these definitions make things easier to prove correct*** but damnit Haskell, I'm a mathematician, not a miracle worker, I want to be able to read those definitions intuitively, and not have to muddle around trying to figure out exactly what that signature represents. It's ugly, fix it.



On that note, I am beginning to work on some Haskell Code which will convert a Type Signature of the form:

f :: S^n1 * T^n2 * ... -> (D1,D2, ... Dn)

to the form:

f :: S -> S -> .. n1 times .. -> T -> T -> ..n2 times.. -> (D1, D2, ... Dn)

and hopefully, given some user input, the latter to the former as well. (This is not harder, sortof, but I can't know what the normal form of the type signature should be without some user input about the in-arity (arity) and out-arity (ority) of the function.

Anywho, Haskell is awesome, go play with it.

~~Joe







*= Aside: I'm quite glad Haskell calls them Reals and not
something silly like Float (though that is allowed) or Double. Us
Mathematicians have had these names for years, IEEE can call the format
Double precision floating point of w/e the hell they want, they're
reals, not doubles. Silly computer scientists...

Edit: Note that in fact I understand that floats != reals, but its about state of mind. I know I'm working on a computer, and so I'm not going to treat things as reals, but I want to be thinking as if I'm not limited, so that when I work with my code, I'm not tuning the algorithm to work with the computer, I'm tuning the computer to work with my algorithm. In this way, the problem becomes a problem of making the compiler better, rather than hacking my algorithm to work.

**= Haskell doesn't really like capitalized function names.

***= Proofs of correctness are done through the Curry-Howard Isomorphism, which effectively states that if the contract of a given function is a valid statement of Logic, then the function is correct, otherwise its not. Note that this requires the Signature to be correctly written, ie:

concatString :: String -> String -. String as a signature for a function which zipped two strings together would be "correct" but only in the sense that the contract would be satisfied. A Proof of correctness means that the function of that type can exist, there are other methods related to this Isomorphism which allow for a better proof of the semantic correctness, as opposed to the more syntactual flare of Curry-Howard