6 ms·

This is a common meme, but I'd like to see some robust empirical evidence either way (the only studies I've seen so far are with e.g. a handful of undergraduate

This is a common meme, but I'd like to see some robust empirical evidence either way (the only studies I've seen so far are with e.g. a handful of undergraduates, implementing a toy problem, well-specified up-front, with no maintenance/feature-drift/etc.) As a trivial counterargument, there's nothing preventing programmers from ignoring even the most advanced type system (see "stringly typed programming", for example). In fact, my experience with "advanced type systems" (e.g. Agda, Idris and Coq), the types have never been a hindrance; it's their totality checking that can be painful (that's why Idris makes it easy to turn that off, either completely or for certain pieces of code).

hota_mazi 8y ago
> This is a common meme, but I'd like to see some robust empirical evidence either way I wouldn't call that datapoint robust nor empirical, but Scala developers have been complaining about the slowness of their builds for more than ten years now, and it's pretty much accepted that the Scala compiler will never get marginally faster than it is today. The Scala 3 compiler is not looking much better either.
- chriswarbo 8y ago
  That sounds like the compiler vs interpreter flamewar, rather than the strong vs weak or static vs dynamic typing flamewars ;) Is there a Scala interpreter to compare performance against? I've not used Scala much, but I know that while Haskell's de facto implementation is the Glasgow Haskell Compiler, there are also (unmaintained) interpreters like HUGS, so compilation isn't a necessity. Plus there's the whole spectrum of Futamura projections, JITs, etc. ;)
- cinnamonheart 8y ago
  Scala's builds from fresh are slow, but this is never a hindrance during development; you just leave `sbt ~compile` running in a terminal, which gives you constant feedback. I find in this case the type system of Scala allows you to quickly reach a sensible solution using the compiler and types to guide you. This allows faster shipping, not slower.
- Drup 8y ago
  What does that has to do with type systems? OCaml is one of the fastest compiler around, and yet it has a very rich type system. Julia also has a very rich type system, but is interpreted/JITed. Many compilers are very slow, even thought their typecheckers barely does anything. The speed of the compiler is related to the design of both the language and the compiler as a whole, not the presence or absence of a decent type system. I would even argue that one of the point to recognize a well designed type system is that it's conceived in a way that admit fast typechecking.
wespiser_2018 8y ago
My thought experiment is this: take a simple, single page app that take user information, runs some calculation, and returns the results. Add login/SSO/or what ever third-party integration. It will be faster to bring value to your customers using a dynamic language (Ruby/Python/PhP), then using (Haskell/Scala). I don't think you really see the benefits of Hindley-Miller type inference, unless you are building complex services (think: compilers, real-time allocation services) that require multiple layers of domain specific abstraction. Advantages of using strongly typed languages for simple SaaS often doesn't hold, and there are very few, if any? successful SaaS start ups that have taken this route. I just think not moving fast enough will kill your start up before you ever get to the point of having to worry about 'tech debt' Note: This could also be true for programming tooling/environmental reasons, and strongly typed languages do help smaller teams handle larger codebases/reduce tests!
- chriswarbo 8y ago
  Again, I haven't seen robust evidence either way about development speed, and any such anecdata will have an equivalent from the other side. One clear failure of dynamic types for Web programming is injection attacks, which are trivially solved by treating HTML, SQL, etc. as separate types (e.g. http://blog.moertel.com/posts/2006-10-18-a-type-based-solution-to-the-strings-problem.html http://blog.moertel.com/posts/2006-10-18-a-type-based-soluti... )
- erdeszt 8y ago
  > It will be faster to bring value to your customers using a dynamic language (Ruby/Python/PhP), then using (Haskell/Scala). If we are talking about a first iteration/mvp then I can agree with you. On the other once you have to maintain/extend/refactor this first iteration you'll start seeing the (imo) enormous benefits of static typing.
seanwilson 8y ago
> This is a common meme, but I'd like to see some robust empirical evidence either way (the only studies I've seen so far are with e.g. a handful of undergraduates, implementing a toy problem, well-specified up-front, with no maintenance/feature-drift/etc.) > In fact, my experience with "advanced type systems" (e.g. Agda, Idris and Coq), the types have never been a hindrance; it's their totality checking that can be painful (that's why Idris makes it easy to turn that off, either completely or for certain pieces of code). A data point: if I'm reading this right, the seL4 formally verified kernel is 14,400 lines of code which required 2.2 person years to write and 20 person years to verify (proofs are done with Isabelle so it's not using types for proofs like e.g. Coq does but you can't escape a similar verification effort): https://www.sigops.org/s/conferences/sosp/2009/papers/klein-sosp09.pdf https://www.sigops.org/s/conferences/sosp/2009/papers/klein-... "The abstract spec took about 4 person months (pm) to develop. About 2 person years (py) went into the Haskell prototype (over all project phases), including design, documentation, coding, and testing. The executable spec only required setting up the translator; this took 3 pm. The initial C translation was done in 3 weeks, in total the C implementation took about 2 pm, for a total cost of 2.2 py including the Haskell effort." "The cost of the proof is higher, in total about 20 py. This includes significant research and about 9 py invested in formal language frameworks, proof tools, proof automation, theorem prover extensions and libraries. The total effort for the seL4-specific proof was 11 py" Why do you think function termination checking is a big factor? I find the majority of loops in apps are of the form "for everything in this collection" or a similar restriction that is simple to check. Either way, if you start pushing complicated program properties into your types, you're very likely to have complicated proofs to solve by hand. What properties were you proving with types where you say they weren't getting in the way?
- chriswarbo 8y ago
  Thanks for the info about seL4, I hadn't seen those effort estimates before. However, I don't think it's relevant to the point I was making. You seem to be talking about formally proving things. If you look through my comment that you're replying to, you'll see that I don't talk about proving anything, let alone "complicated software properties". I was talking about writing programs in languages with 'advanced type systems', as opposed to dynamically typed languages; and that I've not seen compelling evidence to back up common claims like "dynamic languages are faster to program in". You've given compelling evidence that "formally verifying complex properties of large systems is slow and hard", which I think many would already agree with. That doesn't seem relevant to the typed/untyped programming comparison, since formal verification is still a very uncommon thing to do (ignoring language-provided guarantees like memory safety or type safety). > proofs are done with Isabelle so it's not using types for proofs like e.g. Coq does but you can't escape a similar verification effort I don't understand what you mean by "you can't escape a similar verification effort". Not only was I not talking about proving anything, I even stated that the type system can often be ignored and gave "stringly typed programming" as an example (where a program is strongly typed, but almost everything has type `String`, which gives us something quite close to a dynamically typed language; including no guarantees that our variables even have meaningful contents, let alone for any "complicated program properties"!). > Why do you think function termination checking is a big factor? I find the majority of loops in apps are of the form "for everything in this collection" or a similar restriction that is simple to check. I tend to write in a functional programming style, which makes heavy use of recursion. Termination checking (AFAIK) doesn't have the same sort of powerful, composable nature that type checking has, so languages like Coq and Agda (which require termination checking) are very conservative in whether to allow certain forms of recursion or not. It's easy to do "structural recursion", where recursive calls are run on a sub-expression of the argument, e.g. odd Zero = False odd (Succ n) = not (odd n) It's harder to do non-structural recursion, where the recursive call isn't acting directly on part of the argument, e.g. the greatest common divisor algorithm: gcd a 0 = a gcd a b = gcd b (mod a b) This requires ad-hoc proofs to convince the system that the arguments are getting "smaller" by some measure (in this case the sum `a + b` always gets smaller). These can get very hairy, and don't really compose. In this case, for the system to accept the above definition of `gcd` we need to go off and prove theorems about `mod` (i.e. that `b > 0 -> mod a b < b`). The hardest cases I tend to run into are co-termination, which Coq is especially bad at, both in practice (co-recursive calls must be manually unwrapped, and there doesn't seem to be any way to abstract over the raw `cofix` form) and in theory ( https://github.com/coq/coq/issues/5288 https://github.com/coq/coq/issues/5288 https://github.com/coq/coq/issues/6768 https://github.com/coq/coq/issues/6768 ). Agda's co-patterns are nicer to work with, but still require weird type-level hacks (like the "sharp" and "flat" operators, "sized types", etc.) When languages require termination, these sorts of overly-conservative restrictions are inevitable, and we have to deal with them regardless of whether we actually care about termination (or type soundness). That's why I like programming in languages like Idris, where we can selectively ignore termination, and hence the restrictions on what forms we're allowed to write. > What properties were you proving with types where you say they weren't getting in the way? I wasn't talking about proving anything, using types or otherwise. I was specifically talking about not proving things, despite the type system allowing us to do so if we want to (which, if we're happy to consider dynamic types, we probably don't want to). However, when I do happen to be using types to prove things (which, again, is absolutely not required at all, whether or not we're using an 'advanced type system') I find it hard to say that types are "getting in the way", since they're the system of logic for the proofs. We could get such types 'out of the way', but that would also throw away the point of the endeavour. After all, we can 'prove' all sorts of things if we don't allow logic to get in the way ;)

hota_mazi 8y ago

> This is a common meme, but I'd like to see some robust empirical evidence either way I wouldn't call that datapoint robust nor empirical, but Scala developers have been complaining about the slowness of their builds for more than ten years now, and it's pretty much accepted that the Scala compiler will never get marginally faster than it is today. The Scala 3 compiler is not looking much better either.

chriswarbo 8y ago
That sounds like the compiler vs interpreter flamewar, rather than the strong vs weak or static vs dynamic typing flamewars ;) Is there a Scala interpreter to compare performance against? I've not used Scala much, but I know that while Haskell's de facto implementation is the Glasgow Haskell Compiler, there are also (unmaintained) interpreters like HUGS, so compilation isn't a necessity. Plus there's the whole spectrum of Futamura projections, JITs, etc. ;)
cinnamonheart 8y ago
Scala's builds from fresh are slow, but this is never a hindrance during development; you just leave `sbt ~compile` running in a terminal, which gives you constant feedback. I find in this case the type system of Scala allows you to quickly reach a sensible solution using the compiler and types to guide you. This allows faster shipping, not slower.
Drup 8y ago
What does that has to do with type systems? OCaml is one of the fastest compiler around, and yet it has a very rich type system. Julia also has a very rich type system, but is interpreted/JITed. Many compilers are very slow, even thought their typecheckers barely does anything. The speed of the compiler is related to the design of both the language and the compiler as a whole, not the presence or absence of a decent type system. I would even argue that one of the point to recognize a well designed type system is that it's conceived in a way that admit fast typechecking.

wespiser_2018 8y ago

My thought experiment is this: take a simple, single page app that take user information, runs some calculation, and returns the results. Add login/SSO/or what ever third-party integration. It will be faster to bring value to your customers using a dynamic language (Ruby/Python/PhP), then using (Haskell/Scala). I don't think you really see the benefits of Hindley-Miller type inference, unless you are building complex services (think: compilers, real-time allocation services) that require multiple layers of domain specific abstraction. Advantages of using strongly typed languages for simple SaaS often doesn't hold, and there are very few, if any? successful SaaS start ups that have taken this route. I just think not moving fast enough will kill your start up before you ever get to the point of having to worry about 'tech debt' Note: This could also be true for programming tooling/environmental reasons, and strongly typed languages do help smaller teams handle larger codebases/reduce tests!

chriswarbo 8y ago
Again, I haven't seen robust evidence either way about development speed, and any such anecdata will have an equivalent from the other side. One clear failure of dynamic types for Web programming is injection attacks, which are trivially solved by treating HTML, SQL, etc. as separate types (e.g. http://blog.moertel.com/posts/2006-10-18-a-type-based-solution-to-the-strings-problem.html http://blog.moertel.com/posts/2006-10-18-a-type-based-soluti... )
erdeszt 8y ago
> It will be faster to bring value to your customers using a dynamic language (Ruby/Python/PhP), then using (Haskell/Scala). If we are talking about a first iteration/mvp then I can agree with you. On the other once you have to maintain/extend/refactor this first iteration you'll start seeing the (imo) enormous benefits of static typing.

seanwilson 8y ago

> This is a common meme, but I'd like to see some robust empirical evidence either way (the only studies I've seen so far are with e.g. a handful of undergraduates, implementing a toy problem, well-specified up-front, with no maintenance/feature-drift/etc.) > In fact, my experience with "advanced type systems" (e.g. Agda, Idris and Coq), the types have never been a hindrance; it's their totality checking that can be painful (that's why Idris makes it easy to turn that off, either completely or for certain pieces of code). A data point: if I'm reading this right, the seL4 formally verified kernel is 14,400 lines of code which required 2.2 person years to write and 20 person years to verify (proofs are done with Isabelle so it's not using types for proofs like e.g. Coq does but you can't escape a similar verification effort): https://www.sigops.org/s/conferences/sosp/2009/papers/klein-sosp09.pdf https://www.sigops.org/s/conferences/sosp/2009/papers/klein-... "The abstract spec took about 4 person months (pm) to develop. About 2 person years (py) went into the Haskell prototype (over all project phases), including design, documentation, coding, and testing. The executable spec only required setting up the translator; this took 3 pm. The initial C translation was done in 3 weeks, in total the C implementation took about 2 pm, for a total cost of 2.2 py including the Haskell effort." "The cost of the proof is higher, in total about 20 py. This includes significant research and about 9 py invested in formal language frameworks, proof tools, proof automation, theorem prover extensions and libraries. The total effort for the seL4-specific proof was 11 py" Why do you think function termination checking is a big factor? I find the majority of loops in apps are of the form "for everything in this collection" or a similar restriction that is simple to check. Either way, if you start pushing complicated program properties into your types, you're very likely to have complicated proofs to solve by hand. What properties were you proving with types where you say they weren't getting in the way?

chriswarbo 8y ago
Thanks for the info about seL4, I hadn't seen those effort estimates before. However, I don't think it's relevant to the point I was making. You seem to be talking about formally proving things. If you look through my comment that you're replying to, you'll see that I don't talk about proving anything, let alone "complicated software properties". I was talking about writing programs in languages with 'advanced type systems', as opposed to dynamically typed languages; and that I've not seen compelling evidence to back up common claims like "dynamic languages are faster to program in". You've given compelling evidence that "formally verifying complex properties of large systems is slow and hard", which I think many would already agree with. That doesn't seem relevant to the typed/untyped programming comparison, since formal verification is still a very uncommon thing to do (ignoring language-provided guarantees like memory safety or type safety). > proofs are done with Isabelle so it's not using types for proofs like e.g. Coq does but you can't escape a similar verification effort I don't understand what you mean by "you can't escape a similar verification effort". Not only was I not talking about proving anything, I even stated that the type system can often be ignored and gave "stringly typed programming" as an example (where a program is strongly typed, but almost everything has type `String`, which gives us something quite close to a dynamically typed language; including no guarantees that our variables even have meaningful contents, let alone for any "complicated program properties"!). > Why do you think function termination checking is a big factor? I find the majority of loops in apps are of the form "for everything in this collection" or a similar restriction that is simple to check. I tend to write in a functional programming style, which makes heavy use of recursion. Termination checking (AFAIK) doesn't have the same sort of powerful, composable nature that type checking has, so languages like Coq and Agda (which require termination checking) are very conservative in whether to allow certain forms of recursion or not. It's easy to do "structural recursion", where recursive calls are run on a sub-expression of the argument, e.g. odd Zero = False odd (Succ n) = not (odd n) It's harder to do non-structural recursion, where the recursive call isn't acting directly on part of the argument, e.g. the greatest common divisor algorithm: gcd a 0 = a gcd a b = gcd b (mod a b) This requires ad-hoc proofs to convince the system that the arguments are getting "smaller" by some measure (in this case the sum `a + b` always gets smaller). These can get very hairy, and don't really compose. In this case, for the system to accept the above definition of `gcd` we need to go off and prove theorems about `mod` (i.e. that `b > 0 -> mod a b < b`). The hardest cases I tend to run into are co-termination, which Coq is especially bad at, both in practice (co-recursive calls must be manually unwrapped, and there doesn't seem to be any way to abstract over the raw `cofix` form) and in theory ( https://github.com/coq/coq/issues/5288 https://github.com/coq/coq/issues/5288 https://github.com/coq/coq/issues/6768 https://github.com/coq/coq/issues/6768 ). Agda's co-patterns are nicer to work with, but still require weird type-level hacks (like the "sharp" and "flat" operators, "sized types", etc.) When languages require termination, these sorts of overly-conservative restrictions are inevitable, and we have to deal with them regardless of whether we actually care about termination (or type soundness). That's why I like programming in languages like Idris, where we can selectively ignore termination, and hence the restrictions on what forms we're allowed to write. > What properties were you proving with types where you say they weren't getting in the way? I wasn't talking about proving anything, using types or otherwise. I was specifically talking about not proving things, despite the type system allowing us to do so if we want to (which, if we're happy to consider dynamic types, we probably don't want to). However, when I do happen to be using types to prove things (which, again, is absolutely not required at all, whether or not we're using an 'advanced type system') I find it hard to say that types are "getting in the way", since they're the system of logic for the proofs. We could get such types 'out of the way', but that would also throw away the point of the endeavour. After all, we can 'prove' all sorts of things if we don't allow logic to get in the way ;)