So what if it can't prove things like a proof assistant. The Haskell type system has proven to ba a practical tool for real world programming more than anything else. Yes, I've used "type system" and "practical" in the same sentence, because that's what it is, really, and you can only appreciate Haskell when you us it for your everyday tasks instead of writing Fibonaccis.
Haskell's type system is really a way to make the compiler conscious of the code you're writing, and point out where you're not making sense. Sure, it catches only trivial bugs like when a function expects a list of lists and you're calling it on a flat list, but that's exactly the sweet spot. More refined type safety would bloat code and make it harder to change (compare Coq programming with C), bloat the compile times, probably cost money (like all quality code analysis tools do), have convoluted unhelpful error messages (like Haskell does with the fancy language extensions turned on) etc. "Take care of the trivial bugs and let me think about the big picture" is what is needed from a compiler 90% of the time and that's exactly what Haskell's type system gives you.
>>5 Possessive pronouns are never used with articles in the English language. "The your Sussman" would be a blatant mistake.
Name:
Anonymous2016-09-18 10:51
This may sound odd, but I think my dog is Gerald Jay Sussman. It all started when I came home from work one day to find my computer with Emacs running with lisp.; Odd because I turn my computer off when I leave for work. The next I came home, my computer was off, but my dog was on my couch reading SICP. I swear, he was lying there with the book open. I don't even own a copy. I took it from him and he tried to bite me. A few days later, I got a letter in my mail sent to Gerald Jay Sussman. Some university wanting him to teach a class on lisp. Another strange thing, is that when he barks, it almost sounds like he's yelling 'cudder' for some odd reason. He also somehow burned a CD with 'We conjure the spirits of the computer with our spells' song. When ever I have to take him in the car he has to play it. Can someone help me?
Ah, I liked the way how he derived absurd from data families, quite elegant.
But not only that is unsafe. Exceptions are inherently unsafe in haskell. The GenericNewtypeDeriviation extension is unsafe. Lazy IO is unsafe in certain contexts. It is not Agda or Coq, you can shoot yourself in your foot and the language is not meant as proof assistant.