I fear that Haskell is doomed to succeed. — Tony HoareI ♥ Lisp. I think it's the best tool we have, at the moment, for many applications.
I don't really love Haskell that much, but I track its progress with awe. (When I say Haskell, I'm not only speaking about Haskell per se, but also about all the FP languages in its halo, like Ωmega, Agda, Epigram, ...)
And when I look at Haskell, it seems obvious to me that it's out to eat Lisp's lunch. In fact, eat all other languages' lunches.
The gist of this post is: In the not-so-far future, Haskell will be able to do everything Lisp can do now (and more), but in an adjustably-safe, statically-verified manner.
What do I mean by that?
Adjustably-safe: In this mythical, not yet-existing, but clearly on-the-horizon "Haskell", you'll be able to choose how much safety you want. You'll have "knobs" for increasing or decreasing compile-time checks for any property and invariant you desire. Or don't desire. You'll be able to switch between Lisp-style dynamic typing, Haskell-style static typing, and probably even C-style weak/no-typing. In the same program.
Statically-verified: Haskell is clearly moving towards dependent typing, which in theory, allows the expression of arbitrary invariants that are maintained statically, without having to run the program. Dependent typing is the weirdest and most awesome thing to expect of programming, this side of quantum computers.
Lisp, as it stands, can't do any of that, and won't be able to do any of that. That's simply a fact. Why? Because it's coming at the problem from the wrong direction. Trying to graft an interesting type system or verification onto Lisp is simply too heroic and ill-specified a task. Lisp starts with ultimate freedom/unsafety, and you can't constrain it. Haskell starts with ultimate bondage/safety, and then, piece by piece, adds that freedom back. On a theoretically well-founded basis.
Right now, Lisp has certain advantages. As a command or scripting language where ultimate dynamism is desired (Emacs), it's still clearly superior. But Haskell is encroaching on its habitat from all sides, just like it's encroaching on the habitats of all other languages. Right now it may appear pointy-headed and harmless. But I think it's unstoppable, and doomed to succeed.
How does that make Lisp a big hack? If my theory is right, then once Haskell will be able to do everything Lisp can do now (and more), all the while maintaining adjustable safety and static verification, I think it will be justified to call Lisp a big hack - because it lacks the possibility of this safety and verification, in principle. (Of course you have to subscribe to the idea that this safety and verification is something that's good and superior. I do.)
(HN, Reddit)
19 comments:
safety, and even adjustable, is by far not the most important point in programming. It's snake oil actually ;)
What do you think about Typed Racket?
Well, really is impossible/impractical the opposite way (start with no static verification and add it progresively and optionally)?
Racket has attempted to do it...
http://docs.racket-lang.org/ts-guide/index.html
i'd like to know your opinion more in depth about this trend in lisps..
Yeah, I think you're right about Lisp being a big hack. I always thought of Lisp as the dual of Forth - also a clever hack.
But I don't know enough about Haskell to know if it will in fact eat Lisp's lunch. Because no programmer *I* know is willing to give up the freedom to shoot himself, his teammates and his business in the foot by giving up duck typing. Safe programming isn't going to happen - ever - if it was, it would have happened with Ada. ;-)
Haskell and the FP language cater to a niche segment and always will. :) I also love Lisp.
@Anonymous: Why do you think it is snake-oil? Getting guarantees from your programming environment is extremely helpful and saves a lot of testing effort (even if not all of it).
@Bogus: Haskell's type system is much stronger and more interesting than Ada's. Haskell's type-classes support what some people call "duck typing", without the dynamism and unsafety.
@hyperyoda: That remains to be seen :-)
@peaker: In fairness, Haskell typeclasses support a *form* of duck-typing, but you still have to have a "class Duck" describing the actions of a Duck. That's not quite the same thing as saying "anything with a quack method will work"; you instead have to say "anything with a Duck instance defining the quack method will work".
However, with type classes you can add your own Duck instance without touching the original code - scoped fixing of the other implementor not naming their method quack, or not implementing quack, or whatever else. I think that's preferable to both monkey patching and method confusion.
>Haskell will be able to do everything Lisp can
Haskell doesnt have macros, its syntax isnt uniform.
>graft an interesting type system or verification onto Lisp
Not everybody likes "static typing" or cares about "type safety".
>Haskell starts with ultimate bondage/safety, and then, piece by piece, adds that freedom back. On a theoretically well-founded basis.
"Any sufficiently complicated Haskell program contains an ad hoc, informally-specified, bug-ridden, slow implementation of half of Lisp."
Other than that, you can create DynamicType class in C++, but...
Haskell will be able to do everything Lisp can do now
And then it will be written in S-expressions... ;-)
I don't know too much about it, but Qi (lambdassociates.org) is a Lisp with a type system that the author claims is even more powerful than Haskell's, because it is Turing-complete. Type checking in Qi is optional.
Maybe you should take a look at Qi.
@Vitor: Yes, I think so, too. ;)
See also ACL2, a lisp with a proof checker. State the properties of your program directly rather than encoding them into a type system.
A proof that a piece of code has a certain property and a type declaration are similar in that they both annotate the code and are used in an automated fashion by later program analysis.
In some ways, ACL2 starts with even more bondage/safety than Haskell. For example, a function definition is not admitted without a proof that it terminates. Can this property be enforced with Haskell's type system?
Here's an article about the growing Haskell community: http://steve-yegge.blogspot.com/2010/12/haskell-researchers-announce-discovery.html
The best programming language in the world is (should be (will be)) Spoken English.
Everything else is a hack.
What the today's compilers do most of the time? They sit idly by, while a "programmer" churns out specialised code geared towards easing up the compiler's job.
What the true compiler/programming aid should be doing? Letting a designer think aloud in higher abstraction terms, capturing their intent, explicating and verifying the model, constantly churning out the specialised code realising set goals under specified constraints with progressively more and more efficient routines, recompiling/relinking the program all the time as it is used, discovering the use patterns, bottlenecks, optimizing them constantly - in short, an active, aware intelligent design support system. Writing its internal routines in whatever internal language it has at its disposal. Lisp, most probably.
The great promise of equational reasoning got lost somewhere on Haskell's road to success, which it was supposed to avoid at all costs, getting bogged down in implementational details for functions which were supposed to get compiled out into thin air in the first place.
Question: what will the following specification get compiled into, by your favorite Haskell compiler?
fun n m = sum $ take n $ cycle $ [1..m]
Macros!
"You cannot procede from the informal to the formal by formal means." — Alan Perlis
The real power of lisps are s-expressions.
One can invent lisp with all haskell goddies, be it types, monads and laziness.
But one can't invent haskell with s-exp.
Post a Comment