6 ms·

Has anyone here used Haskell in a production environment? I want a language that is small, clean, and can provide a lot of static guarantees. I know many peopl

Has anyone here used Haskell in a production environment? I want a language that is small, clean, and can provide a lot of static guarantees. I know many people find static guarantees and unacceptable curtailment of their "programming freedom", but frankly I think it's the answer to many of the problems we face in software today. Small is another thing. E.g. Go and Scheme are small. C++ and Scala are large. You know what I mean.. Now, static typing is just one kind of static assertion[1] I'd like to have. Side effect isolation (i.e. language-enforced purity) would be another feature I'd like to see become common. For example, the D programming language has a "pure" keyword that lets you mark a function as side-effect free. (In Haskell, all function are pure by default, and you escape the confines of purity via monads.) I'd like to do research into (inventing) other forms of static assertions. One thing that's been on my mind lately, has been static "complexity assertion" for programs. I don't know if this even possible, but it would be nice to be able to ascertain before running a program, certain time & space complexity bounds on it. This would perhaps require us to drop the programming language itself to some level "slightly below" Turing machines -- but this in itself could be achieved via a keyword like D's "pure" or something more elegant. (Note: my point is not that we're going to make the entire language non-Turing complete -- but rather that we'll have subsets of the language that are not, and this reduction of power would/could bring with it a greater possibility for statically asserting stuff.) [1] FYI I made this term up. Let me know if there's something better that describes this.

scott_s 13y ago
User thirsteh talked about his experiences with Haskell in production yesterday: https://news.ycombinator.com/item?id=6278588 https://news.ycombinator.com/item?id=6278588
obeattie 13y ago
> it would be nice to be able to ascertain before running a program, certain time & space complexity bounds on it I don't know about knowing what "space" a program will consume ahead of time, but I believe the halting problem[1] means there'd be no way of computing a time requirement. [1] http://en.wikipedia.org/wiki/Halting_problem http://en.wikipedia.org/wiki/Halting_problem
- scott_s 13y ago
  The halting problem assumes a program from a Turing-complete model of computation. Not all computational models are Turing-complete. The parent is pointing out that if you limit yourself to a language or a sub-set of a language that is not Turing-complete, then you can make static assertions about things such as halting. A trivial example would be a programming language that did not allow any loops or explicit backward branches. You would be able to provide upper bounds on how many operations such programs can perform.
  - winter_blue 13y ago
    I was just going to make the same reply. > if you limit yourself to a language or a sub-set of a language that is not Turing-complete, then you can make static assertions about things such as halting There's already something that is non-Turing complete, but comes with a halting guarantee -- it's called total functional programming[1]. This paper (linked below) is actually what got me thinking about this whole thing. The author argues in it how functions in functional programming languages aren't really like mathematical functions, because they have the possibility to execute infinitely (never halt) and thus not have a proper return value. To mitigate that, he creates "total functional programming". Total functions are guaranteed to have a return value (i.e. terminate eventually), but they could take very long to run. If we could actually have complexity bounds, or be able to determine a given function's complexity, that would be a great boon to software engineering (i.e. assuming they adopt it... which is a whole different matter). The author also makes a very good point that most parts of your program are meant to terminate (i.e. the vast set of functions and algorithms that comprise you program). Only the top-level needs to be Turing-complete, the rest can at least be total. I actually want to see if it's possible to push this concept further, to create a ring-like hierarchy of languages -- the lowest one being the weakest and the one we can extract the most static assertions out of, and so on. There's a language called Hume[2] that sounds like it accomplishes at least part of this goal, but I haven't really looked into it. [1] http://www.jucs.org/jucs_10_7/total_functional_programming/jucs_10_07_0751_0768_turner.pdf http://www.jucs.org/jucs_10_7/total_functional_programming/j... [2] https://en.wikipedia.org/wiki/Hume_%28programming_language%29 https://en.wikipedia.org/wiki/Hume_%28programming_language%2...
sridharvembu 13y ago
Your point on "slightly below" Turning machines caught my attention - exactly the same terminology I have used. I want as many proofs (assertions) as possible about code, and Rice's Theorem is a problem, so slightly below Turing is on the radar. If you are interested, we can discuss this. Shoot me an email at svembu at zoho ...
kenko 13y ago
"(In Haskell, all function are pure by default, and you escape the confines of purity via monads.)" This is not true. Nothing about monads, in themselves, allows you to write impure functions.
- lmartel 13y ago
  It's pretty common on HN for people to say "monads" when they mean IO. For some reason.
creatio 13y ago
For the "complexity assertion" I think you may be referring to something like this: http://resourceanalysis.cs.ru.nl/ http://resourceanalysis.cs.ru.nl/ Maybe its not totally exactly what you meant, but it can do basic analysis for loops.
chas 13y ago
Total functional programming (and the associated analysis of codata has already been touched on), so I'll just address your interest in static guarantees for space usage. The Virgil programming language[1] has been designed with exactly this in mind. It is aimed at embedded systems where memory is extremely constrained and running out of memory could kill people. Heap allocation is not possible in the language and all data structures are initialized during compilation (like C++ templates, but more sophisticated). The compiler can use the initialization information for advanced optimization and analysis as well as serving as a bound on the memory usage. [2] The language also has some interesting static typing ideas, but they are not as distinct from other languages. Further discussion on LtU: http://lambda-the-ultimate.org/node/2131 http://lambda-the-ultimate.org/node/2131 [1] https://code.google.com/p/virgil/ https://code.google.com/p/virgil/ [2] http://compilers.cs.ucla.edu/virgil/overview.html http://compilers.cs.ucla.edu/virgil/overview.html
- e12e 13y ago
  I wonder if a restricted subset of a stack based language like Forth might also work?
doublec 13y ago
Inch [1] has an example using complexity annotations, showing that a red-black tree insert/delete are linear in the black height. ATS [2] is my go-to language for static guarantees with C's efficiency. Not sure if it counts as small but the implementation is not big. [1] https://github.com/adamgundry/inch https://github.com/adamgundry/inch [2] http://www.ats-lang.org http://www.ats-lang.org

scott_s 13y ago

User thirsteh talked about his experiences with Haskell in production yesterday: https://news.ycombinator.com/item?id=6278588 https://news.ycombinator.com/item?id=6278588

obeattie 13y ago

> it would be nice to be able to ascertain before running a program, certain time & space complexity bounds on it I don't know about knowing what "space" a program will consume ahead of time, but I believe the halting problem[1] means there'd be no way of computing a time requirement. [1] http://en.wikipedia.org/wiki/Halting_problem http://en.wikipedia.org/wiki/Halting_problem

scott_s 13y ago
The halting problem assumes a program from a Turing-complete model of computation. Not all computational models are Turing-complete. The parent is pointing out that if you limit yourself to a language or a sub-set of a language that is not Turing-complete, then you can make static assertions about things such as halting. A trivial example would be a programming language that did not allow any loops or explicit backward branches. You would be able to provide upper bounds on how many operations such programs can perform.
- winter_blue 13y ago
  I was just going to make the same reply. > if you limit yourself to a language or a sub-set of a language that is not Turing-complete, then you can make static assertions about things such as halting There's already something that is non-Turing complete, but comes with a halting guarantee -- it's called total functional programming[1]. This paper (linked below) is actually what got me thinking about this whole thing. The author argues in it how functions in functional programming languages aren't really like mathematical functions, because they have the possibility to execute infinitely (never halt) and thus not have a proper return value. To mitigate that, he creates "total functional programming". Total functions are guaranteed to have a return value (i.e. terminate eventually), but they could take very long to run. If we could actually have complexity bounds, or be able to determine a given function's complexity, that would be a great boon to software engineering (i.e. assuming they adopt it... which is a whole different matter). The author also makes a very good point that most parts of your program are meant to terminate (i.e. the vast set of functions and algorithms that comprise you program). Only the top-level needs to be Turing-complete, the rest can at least be total. I actually want to see if it's possible to push this concept further, to create a ring-like hierarchy of languages -- the lowest one being the weakest and the one we can extract the most static assertions out of, and so on. There's a language called Hume[2] that sounds like it accomplishes at least part of this goal, but I haven't really looked into it. [1] http://www.jucs.org/jucs_10_7/total_functional_programming/jucs_10_07_0751_0768_turner.pdf http://www.jucs.org/jucs_10_7/total_functional_programming/j... [2] https://en.wikipedia.org/wiki/Hume_%28programming_language%29 https://en.wikipedia.org/wiki/Hume_%28programming_language%2...

sridharvembu 13y ago

Your point on "slightly below" Turning machines caught my attention - exactly the same terminology I have used. I want as many proofs (assertions) as possible about code, and Rice's Theorem is a problem, so slightly below Turing is on the radar. If you are interested, we can discuss this. Shoot me an email at svembu at zoho ...

kenko 13y ago

"(In Haskell, all function are pure by default, and you escape the confines of purity via monads.)" This is not true. Nothing about monads, in themselves, allows you to write impure functions.

lmartel 13y ago
It's pretty common on HN for people to say "monads" when they mean IO. For some reason.

creatio 13y ago

For the "complexity assertion" I think you may be referring to something like this: http://resourceanalysis.cs.ru.nl/ http://resourceanalysis.cs.ru.nl/ Maybe its not totally exactly what you meant, but it can do basic analysis for loops.

chas 13y ago

Total functional programming (and the associated analysis of codata has already been touched on), so I'll just address your interest in static guarantees for space usage. The Virgil programming language[1] has been designed with exactly this in mind. It is aimed at embedded systems where memory is extremely constrained and running out of memory could kill people. Heap allocation is not possible in the language and all data structures are initialized during compilation (like C++ templates, but more sophisticated). The compiler can use the initialization information for advanced optimization and analysis as well as serving as a bound on the memory usage. [2] The language also has some interesting static typing ideas, but they are not as distinct from other languages. Further discussion on LtU: http://lambda-the-ultimate.org/node/2131 http://lambda-the-ultimate.org/node/2131 [1] https://code.google.com/p/virgil/ https://code.google.com/p/virgil/ [2] http://compilers.cs.ucla.edu/virgil/overview.html http://compilers.cs.ucla.edu/virgil/overview.html

e12e 13y ago
I wonder if a restricted subset of a stack based language like Forth might also work?

doublec 13y ago

Inch [1] has an example using complexity annotations, showing that a red-black tree insert/delete are linear in the black height. ATS [2] is my go-to language for static guarantees with C's efficiency. Not sure if it counts as small but the implementation is not big. [1] https://github.com/adamgundry/inch https://github.com/adamgundry/inch [2] http://www.ats-lang.org http://www.ats-lang.org