This is supported by the parametricity theorem. That is a big word, but it boils down to this: let's say you wrote an identity function of type "a -> a", and it passed the type checker. Then it is correct: you simply can't do much with a value of type "a", because you don't know anything about it.
If an identity function is too simple, consider "compose :: (a -> b) -> (c -> a) -> (c -> b)". I think it can be proven that if you write an implementation that passes the type checker for this signature, the implementation is necessarily correct.
Note the "Safety Inferred" seal of approval on the upper right hand corner of the hackage package http://hackage.haskell.org/packages/archive/lens-family-core... This means it survives a recursive check of dependencies that precludes that kind of nonsense.
I hadn't thought of that. Types serve as a good safety net, but they're not foolproof. Expecting something like that to be correct because it passed through the type checker is like expecting to be served at a restaurant dressed in a gorilla suit because you got through the door.
Hi. I make a living writing code. Also, I'm bad at math other than bit arithmetic and calculating tips. (Edit: I guess I sort of understand sets and basic set operations)
What in the hell are you two talking about and why shouldn't I take this as a sign that I should avoid Haskell at all costs?
You can prove properties in Haskell using the type system, (provided that you can show that the expression you are proving properties about actually terminates).
I was merely pointed out that last part in the most succinct way I knew how.
You should definitely not avoid Haskell at all costs. I would characteristic programming as the process of constructing systems and managing complexity. If you have a greater exposure to languages and paradigms then you have more tools at you disposal for doing your job. A programmer may be able to get by without knowing anything about Haskell or functional programming in general, but that's only because they don't realize when they are kludging something that is so simple if only it was thought about differently.
I'm a grumpy old clisper. I know well the benefits of functional programming. (And Perlis languages in general. If you don't know the c2 page for this, you should feel deep shame.)
Thing is, my fellow lispers, and our scheming siblings too, spent most our time talking about programming or actual code. The former being the means or mode to produce the latter.
Why don't Haskellers ever seem to be talking about programming or actual code when I encounter them in the wild?
Haskell seems to be some mad science project that came about after some grad students happened across an ML manual and a bottle of scotch. (At least you guys didn't make that 31-bit integer mistake. Oof, tagged pointers.)
The emphasis on the type system seems to be a bit revisionist to me. The original (pre-Haskell '98) emphasis was on the laziness really. That turned out to be a huge mistake outside of some cute demonstrations for the purpose of understanding the runtime behavior of your code, so you're choosing to ignore this monstrous mistake and instead promulgate this type safety nonsense as if static analysis has gone anywhere in the last few decades.
So back to my original questions, why don't I ever seem to find you people talking about actual code?
When I encounter fellow Python programmers, they're usually talking about cool libraries, solving interesting problems, neat tools they've discovered or made, best practices, etc.
With Haskell it's more like I've bumped into a rather unpleasant evangelical minister or Amway salesman bred with Doc Brown from Back to the Future. It's like the Haskell community has two modes of operation: proselytization and mathematical gibberish.
I agree that laziness turned out to be a bad default for the reasons you mentioned (other Haskellers may disagree with me on that point), but I don't think that means that it was a mistake to pursue it. It forced the designers to build in purity which turned out to be immensely valuable. Having laziness as a default is also not the kind of decision you can easily revert.
You're right to say that the field of static analysis has been very active. What you're forgetting is that this has been in no small part due to type theory.
I think the reason you don't find people talking about actual code, as you put it, is because actual code and so called mathematical gibberish are one and the same thing.
Lisp is based on the idea that code are data are equivalent, Haskell is based on the idea that code and mathematical gibberish are equivalent.
I didn't intend to imply that you didn't know the benefits of functional programming. I could have worded that better. Do you know the benefits of typed functional programming?
Having recently delved into lisp, I do miss the static analysis that goes on before the program starts. I realized that I used types to plan out the program before I started coding and I miss having the type-checker picking holes in my plans. I'm determined to stick at it though so that I can see what I'm missing in terms of meta-programming and other dynamic features.
>Do you know the benefits of typed functional programming?
Yes, that's how I know what ML and the tragedies of tagged pointers are.
SBCL supports type annotations, and Racket has a Typed Racket dialect that does type checking insofar as you've provided the types.
Part of the problem that Lispers and Schemers have is that they can add the static analysis to their programs anytime they want through the macro system (hence typed racket). They don't have to hack up the compiler or anything.
The other problem is cultural. Lispers resent implementation-level obligation to a set of rules that were made ignorant of any given problem they may be solving. What if you need to resolve something at runtime? What if you need to resolve something at compile-time? Lisp lets you choose where each should happen.
I feel similarly about purity. I think it makes for a nice default, but I think the degree to which immutability is forced on you in Clojure and Haskell are pretty damned awkward for expressing a variety of problems and not just ones related to IO. It seems especially silly since a lot of code in Common Lisp will by default be pure because it'll just return results based on inputs absent mutation.
Regarding your delvings into Lisp, since you're not unfamiliar with the benefits of functional programming I'd like to recommend a book that will help you break ground with a dynamically typed, multiple-dispatch Lisp with an object system. Get "Art of the Metaobject Protocol". Hopelessly specific to Lisp but glorious nonetheless.
The book doesn't get as deep as I'd like, but it's considered one of the best books on the subject nevertheless.
One of the things I don't like about Haskell is that it has a really complicated type system because it isn't (and couldn't realistically become) dependently typed. This is one of the things that drew me to lisp, you can choose which type system you use.
I must disagree with you on purity though. Purity allows you to apply equational reasoning, it allows compilers to apply optimizations that wouldn't otherwise be possible. It makes multi-threading, if not possible then substantially easier. You do get some of these advantages from having purity by default, but if it's not enforced, you can't get most of them. For me, I see this as an acceptable compromise (actually I don't see it as a compromise at all, if all I got from purity was equational reasoning I'd still use it), but as you point out, the culture amongst lispers is different.
Thanks for the book recommendation, I must admit that I already have a number of books to get through before I'll be able to look into it (including LiSP and "Compiling with continuations"), but I surely will do.
My dream programming language is actually a Lisp with static-by-default typing that was powerful and useful. If you end up implementing something, PLEASE post it on HN or let me know, I'd love to check it out. :)
This is how I know about Typed Racket despite not being that keen on Scheme dialects (other than call/cc), I was very excited to see how compile-time typing could work in a Lisp/Scheme.
> If you don't know the c2 page for this, you should feel deep shame.
Consider me shamed, mind sharing a link? I know the quote from Alan Perlis you're talking about, but the Google search results for "perlis languages" is dominated by Fogus's blog post with the same title, and your comment is the first result for "perlis languages c2", followed by a few other wiki pages.
That is true, but the proposition is one that is encoded in the type. There are many derivations of certain proofs. Consider:
map :: (a -> b) -> [a] -> [b]
And [a] is shorthand for a recursive type: \forall a . \mu l . (a * l) + ().
And the translation of types to propositions means that the sum type -- either I have () or I have a list, translates to a logical connective of "or". The product type -- I have an a and the rest of the list -- translates to "and" .
The proposition is therefore that, for all a, for all b, if a implies b, then true or (a and list of a) implies true or (b and list of b).
There are several proofs of this proposition, and some of them are useless.
The standard one:
map f [] = []
map f (x:xs) = f x : map f xs
Is what we want.
There's another one, though:
map f [] = []
map f (x:xs) = [f x]
And many others that aren't so useful as the standard one.
Anyway, this has been a long and roundabout way of saying that, while a good type system give you a lot of nice static properties about a program, you simply cannot ignore dynamic semantics and rely on the types. Well-typed programs are correct in that they will not reach a state where evaluation is undefined / get stuck ("I'm supposed to do what? These are Strings, not Ints!"), but they do not imply correctness of the program, even though they do provide a proof of a proposition!
There are a lot of other Haskell features you can use. Term-level recursion works:
f :: a -> b
f = f
Type-level recursion works, even without explicit term-level recursion:
data T a b = C (T a b -> (a -> b))
q :: T a b -> (T a b -> (a -> b))
q (C f) = f
w :: T a b -> (a -> b)
w x = (q x) x
f :: a -> b
f = w (C w)
This is basically encoding Russell's paradox at the type level. You can write out f explicitly, just so that it doesn't look like you might somehow still be applying w to itself recursively:
g :: a -> b
g = (\x -> ((\(C f) -> f) x) x) (C (\x -> ((\(C f) -> f) x) x))
There are even ways of doing this using highly impredicative definitions involving GADTs and type families, without involving any explicit recursion at all:
If an identity function is too simple, consider "compose :: (a -> b) -> (c -> a) -> (c -> b)". I think it can be proven that if you write an implementation that passes the type checker for this signature, the implementation is necessarily correct.