9 ms·

What this article ignores is that in practice one must read the source code to understand the function. You can be reasonably certain that the Python function d

What this article ignores is that in practice one must read the source code to understand the function. You can be reasonably certain that the Python function doesn't harm your grandmother that way. I understand that strong functional programming is going to catch type errors at compile time and force constraints on the values in your program but it's quite rare that I've encountered a type error in a Python program. What I most often encounter are logic errors. We don't write formal specifications for safety-critical code often enough. Your program will still have errors of this kind if you don't think clearly enough before you start writing code. There are nice things strong, static typing of the functional variety offers certainly -- but it's not a hammer that is particularly useful at cutting boards. There are plenty of cases where a dynamic type system is good enough or even ideal.

mej10 11y ago
With languages like Haskell you can lift many types of logic errors into the realm of type errors.
- cle 11y ago
  At what cost? What are the tradeoffs? (this is a question I'm genuinely curious about)
  - 15155 11y ago
    > At what cost? Directly related to the typechecker? Non-incremental (cold) compile times.
  - nickbauman 11y ago
    Defining those types and the rules of their interaction with a greater type system is also cognitive load you must do up front. In most cases, we must develop systems with incomplete knowledge and must show some progress before all the rules are defined. So you will be changing a lot more code as you learn more than you would in a dynamically typed system.
    - dllthomas 11y ago
      In my experience, this is not the case. In my current project, I am parsing and analyzing a dialect of SQL. As you say, "we must develop systems with incomplete knowledge". Had it been necessary that I get my rules right up front, there would be tremendous pain - the documentation is inconsistent, incomplete, and incorrect. Tremendous agreement there. This is no case for foregoing types. In order to write code we must be defining expectations of how our system works. Even ideally loosely coupled, code depends on the behavior of other code. When we learn that a given interface is no longer going to work, we need to find and change everywhere that relied on that interface. Working in Haskell I was able to sketch out a preliminary and incomplete set of rules; as I found them not to work I could change them - with tremendous assistance in finding exactly the points that needed to change in tandem. Working in Python earlier this year, much smaller changes to much simpler code has been substantially more painful.
      - tome 11y ago
        > In my experience, this is not the case. Not my experience either. We commonly hear the refrain "Haskell does not allow you to do exploratory programming". Personally I prefer exploratory programming in Haskell to any other language.
  - phamilton 11y ago
    There's usually a cost to runtime inspection and metaprogramming. In order to guarantee things at compile time they must not be possible at runtime. Languages are getting better at type inference, but things like JSON parsing are more rigid and explicit. It just feels jobbish at times.
  - ridiculous_fish 11y ago
    I have a Python script runs as both Python 2 and Python 3, using runtime checks to determine which methods to call. This sort of thing is much harder in Haskell. A more ambitious example: imagine the web with JavaScript replaced by Haskell. Your code compiles and typechecks in your browser, but that doesn't guarantee that it will do the same in mine, or a different version of yours, or tomorrow's new browser. So these static type guarantees are very weak because they only apply to a single runtime environment. The less control you have over the runtime environment, the more important dynamic typechecks become. You can also have static type checking, but you have to be prepared for the fact that your static types will be different at runtime. This property confounds most languages with static type systems, including Haskell.
    - guiraldelli 11y ago
      > A more ambitious example: imagine the web with JavaScript replaced by Haskell. Your code compiles and typechecks in your browser, but that doesn't guarantee that it will do the same in mine, or a different version of yours, or tomorrow's new browser. So these static type guarantees are very weak because they only apply to a single runtime environment. Wait... What? Are you saying that natural numbers in South America in 1990 century is different from natural numbers in Europe 2010? So how can types be different depending on browsers? Of course, if the browser implements a "compiler" that doesn't follow the basic principles reported in the standard of the language, it'll happen. If some joker wants to call `Int` a `String`, problems will happen. Otherwise, it is not true.
      - nickbauman 11y ago
        Ah, that's right. Everyone implements the compiler spec the same way every time, because we live in a perfect world.
- pron 11y ago
  Basically yes. The question is what exactly it buys you. In general, the proving power of Haskell's type system is that of a finite-state-machine/regular expression (i.e. you can verify behavior of an FSM), and the proving power of Idris is that of a full Turing Machine, but in general we know that verifying a program property has a lower complexity bound of Ω(# of program states), i.e. exponential in the size of the source code, regardless of the language used (actually, the more expressive the language, the harder the problem becomes, but just by a bit). The question is, then, given that all approaches are bound by the same complexity bounds for complete proof, which approach is cheaper in practice based on property type, program type and required confidence? Sadly, we don't have the answer to that question, but answering it would require some expensive empirical studies.
phamilton 11y ago
I'd argue that a rich type system shifts logic errors into syntax error. An easy example is time arithmetic. Adding seconds to minutes can be problematic. If you have proper types defined (in any language, pythons types do fine for this) then you need to confirm that addition of minutes and seconds is correct in one place, and the type system will guarantee it's done correctly throughout your code. A richer type system allows you to move more logic into type system.
- paulddraper 11y ago
  s/syntax/type/
  - deleted 11y ago
    [deleted]
  - agumonkey 11y ago
    Somehow somewhere it's the same, there's some expressions that you cannot write based on the rules you declared.
    - paulddraper 11y ago
      Typically, a syntax is specified by BNF or similar. Every programming language has syntax, not every programming language has static types. I think you can separate these pretty cleanly.
      - dllthomas 11y ago
        > I think you can separate these pretty cleanly. You can, and probably should, but it's more of an engineering distinction than a theoretical one. Syntax and types are both rules for how phrases can fit together. And sometimes it blurs - I understand that at least one C++ compiler parses with an overly general parser, collecting several results and disambiguating with type information. > Every programming language has syntax, not every programming language has static types. Not every programming language has "static syntax" - some allow you to adjust the parser, and some don't do any checking of the whole file (much less the whole program) before they start running the first bits of it.
rtpg 11y ago
The other restrictions brought by languages like Haskell catch classes of error you do see in Python. For example, with django's forms, you are forced to call validation (`form.is_valid()`) before you can get the result of said validation (`form.cleaned_data`) So referencing `form.cleaned_data` before `form.is_valid()` is incorrect.... If you had to port something like Django's forms to Haskell, you could instantly get rid of this issue because such behaviour is impossible to express in the language. In Haskell you would likely write a `validate` function that takes a form, and returns either a validation error or the validated data itself: `let maybeCleanedData = validate form` The type system that makes effects explicit (really, the immutable nature of everything, but one and the other usually synergise well) means that your API is forced to be a saner one. You can take what you learn from these type systems and bring it back to Python though. Like you said, most errors are logic errors. But logic errors can often be helped along by dangerous APIs. Types and removal of stateful code can give you the boundaries to rule out many designs that can come back to bite you.
nickbauman 11y ago
Here's the thing. You're not going to forgo your tests, right? But testing in a statically typed language is much harder to get right. But you still need them. So the question of static or dynamic typing is moot.
- chadaustin 11y ago
  Why is testing harder in a statically typed language? Seems about the same to me.
  - phamilton 11y ago
    Monkey patching is often difficult in a statically types language, but is quite useful in testing.
    - chadaustin 11y ago
      Ah, fair enough! Though monkey patching is only possible in some dynamic languages, namely the ones where classes and modules are mutable hash tables. Note that in ES6, unless you insert some special code via something like babel-rewire, imports can't be monkey patched. Also, Scheme is dynamically-typed and has no monkey patching. Anyway, I agree monkey patching in tests can be pretty convenient! But I personally think it's also a bad idea because it means that your tests are now coupled to the internal implementation of the code under test. That is, if you refactored the implementation, the test could break. Passing testable dependencies explicitly avoids this problem and avoids the need to monkey patch in tests.
      - phamilton 11y ago
        That seems like more of an argument against mocking in general. Even if you DI you are still expecting X method to be called on the mock object and have created that coupling. I think DHH describes a great example that illustrates a big difference in philosophy around this: http://david.heinemeierhansson.com/2012/dependency-injection-is-not-a-virtue.html http://david.heinemeierhansson.com/2012/dependency-injection...
gnuvince 11y ago
> It's quite rare that I've encountered a type error in a Python program. What is your definition of a type error? The point of more advanced type systems is to allow programmers to express more information about the program in the types so that the compiler can check them and report mistakes. I've done my share of Python coding and many of my errors were definitely type errors (even if they didn't necessarily raise TypeError).
chadaustin 11y ago
it's quite rare that I've encountered a type error in a Python program I hear that relatively frequently from people who consider types to be things like functions, strings, integers, and other "representation types". But the benefit of type systems, especially type systems as expressive as Haskell, is that you, many times, can encode your logical invariants in the type system by introducing new nominal types. For example, you can introduce a new type for each type of ID in your system, like CustomerID, ExperimentID, EventID, which prevents you from mixing those up. You can use types to distinguish between mutable and immutable data structures. It's perfectly okay to use object identity when comparing immutable data structures, but it's usually a bug if the data structure is mutable. When you take a more expansive view of what type systems can offer, they're more useful.
- jdmichal 11y ago
  > It's perfectly okay to use object identity when comparing immutable data structures, but it's usually a bug if the data structure is mutable. I don't understand this statement. The only thing immutability provides here is the ability to know that an object didn't change by knowing that it's the same object. There's no guarantee of value equality from identity unless all objects are interned.
  - chadaustin 11y ago
    Ah, yeah, perhaps I should have elaborated more. It's a subtle issue, but it's one that comes up all the time when optimizing React by removing unnecessary renders. With immutable data structures, you know that x == y implies, even if x was initialized a while ago, that the data is the same. With mutable data, that's not true -- perhaps the values referenced by x have changed value in the meantime, so x == y does not imply that the data is the same.
- agentultra 11y ago
  Encoding an invariant in the type system is definitely a strong benefit of Haskell and other similar languages. You can do more than simple identity/immutability with types. I find the flexibility of the type system to share some similar properties with C++'s more advanced features. Used sparingly they can be quite powerful but come with a complexity that few mortals will be able to comprehend. In a distributed system, for example, you can encode an invariant in the type system that will constrain the execution to only valid states. This is immensely powerful. However you can also model arbitrarily complex computations into the type system which will make sense to no one but the author who wrote it. One thing I do miss in Python that a type system gives you is the compiler's ability to do exhaustive pattern matching. Forcing you to deal with every case explicitly is a huge advantage. In fact, I'm currently working on a formal specification of eventlet's Semaphore class as an exercise (I'm in the process of learning) as we've found just such a bug in a large Python code base where a particular exception is not caught and locks up the whole system. An exhaustive pattern search would have forced the authors to deal with that exception and this bug wouldn't have surfaced.
kpmah 11y ago
You're making an argument from your experience, so permit me to make an argument from mine: I've been using Python and Ruby professionally for about 10 years. The most common error I make myself is typos, but those are often (but not always) fixed quickly. The most common mistake I see getting to production is not handling a return value or an exception because it was assumed it couldn't happen. Types can help with both of these things, and tests less so - because often if you're making an assumption about the return value of a function, it's because you haven't considered the possibility and you don't write a test for it. A dynamic language can certainly be good enough, but in my opinion never ideal.
- toolslive 11y ago
  Just take any large python project and search the bug trackker for : "AttributeError: 'NoneType' object has no attribute ..." You'll find plenty of those. So people are wasting time tracking and fixing something that could have been found by a machine (a compiler in this case) in microseconds. A colleague of mine once stated: "unit tests are a poor man's compiler".
- agentultra 11y ago
  Well if you want to get out the yard sticks I've been writing Python for more than 10 years. Exhaustive case matching is very useful, I agree. It is a common error in Python code (and in a similar fashion, to catch all exceptions however inappropriate). > A dynamic language can certainly be good enough, but in my opinion never ideal. If I think about it scientifically there are many cases where Python is ideal. For example the scientific Python stack, Jupyter, etc is very popular and, "ideal," in the sense that people frequently use it to get real work done. They don't have to categorize every expression and can instead focus on the data and transformations. As a data-exploration tool Python can be said to be ideal. It seems ideal too as the implementation language of OpenStack where the community supports over 4+ million lines of Python code. Could OpenStack have been better written in Haskell? Maybe. However thousands of contributors seem quite comfortable with Python and the process around developing reliable infrastructure software seems to catch critical errors in practice. I believe that strongly-typed functional languages are awesome. There are many situations where I'd prefer one over the other. However I don't deal in absolutes and don't believe Haskell is going to be the hammer that screws every dowel.

mej10 11y ago

With languages like Haskell you can lift many types of logic errors into the realm of type errors.

cle 11y ago
At what cost? What are the tradeoffs? (this is a question I'm genuinely curious about)
- 15155 11y ago
  > At what cost? Directly related to the typechecker? Non-incremental (cold) compile times.
- nickbauman 11y ago
  Defining those types and the rules of their interaction with a greater type system is also cognitive load you must do up front. In most cases, we must develop systems with incomplete knowledge and must show some progress before all the rules are defined. So you will be changing a lot more code as you learn more than you would in a dynamically typed system.
  - dllthomas 11y ago
    In my experience, this is not the case. In my current project, I am parsing and analyzing a dialect of SQL. As you say, "we must develop systems with incomplete knowledge". Had it been necessary that I get my rules right up front, there would be tremendous pain - the documentation is inconsistent, incomplete, and incorrect. Tremendous agreement there. This is no case for foregoing types. In order to write code we must be defining expectations of how our system works. Even ideally loosely coupled, code depends on the behavior of other code. When we learn that a given interface is no longer going to work, we need to find and change everywhere that relied on that interface. Working in Haskell I was able to sketch out a preliminary and incomplete set of rules; as I found them not to work I could change them - with tremendous assistance in finding exactly the points that needed to change in tandem. Working in Python earlier this year, much smaller changes to much simpler code has been substantially more painful.
    - tome 11y ago
      > In my experience, this is not the case. Not my experience either. We commonly hear the refrain "Haskell does not allow you to do exploratory programming". Personally I prefer exploratory programming in Haskell to any other language.
- phamilton 11y ago
  There's usually a cost to runtime inspection and metaprogramming. In order to guarantee things at compile time they must not be possible at runtime. Languages are getting better at type inference, but things like JSON parsing are more rigid and explicit. It just feels jobbish at times.
- ridiculous_fish 11y ago
  I have a Python script runs as both Python 2 and Python 3, using runtime checks to determine which methods to call. This sort of thing is much harder in Haskell. A more ambitious example: imagine the web with JavaScript replaced by Haskell. Your code compiles and typechecks in your browser, but that doesn't guarantee that it will do the same in mine, or a different version of yours, or tomorrow's new browser. So these static type guarantees are very weak because they only apply to a single runtime environment. The less control you have over the runtime environment, the more important dynamic typechecks become. You can also have static type checking, but you have to be prepared for the fact that your static types will be different at runtime. This property confounds most languages with static type systems, including Haskell.
  - guiraldelli 11y ago
    > A more ambitious example: imagine the web with JavaScript replaced by Haskell. Your code compiles and typechecks in your browser, but that doesn't guarantee that it will do the same in mine, or a different version of yours, or tomorrow's new browser. So these static type guarantees are very weak because they only apply to a single runtime environment. Wait... What? Are you saying that natural numbers in South America in 1990 century is different from natural numbers in Europe 2010? So how can types be different depending on browsers? Of course, if the browser implements a "compiler" that doesn't follow the basic principles reported in the standard of the language, it'll happen. If some joker wants to call `Int` a `String`, problems will happen. Otherwise, it is not true.
    - nickbauman 11y ago
      Ah, that's right. Everyone implements the compiler spec the same way every time, because we live in a perfect world.
pron 11y ago
Basically yes. The question is what exactly it buys you. In general, the proving power of Haskell's type system is that of a finite-state-machine/regular expression (i.e. you can verify behavior of an FSM), and the proving power of Idris is that of a full Turing Machine, but in general we know that verifying a program property has a lower complexity bound of Ω(# of program states), i.e. exponential in the size of the source code, regardless of the language used (actually, the more expressive the language, the harder the problem becomes, but just by a bit). The question is, then, given that all approaches are bound by the same complexity bounds for complete proof, which approach is cheaper in practice based on property type, program type and required confidence? Sadly, we don't have the answer to that question, but answering it would require some expensive empirical studies.

phamilton 11y ago

I'd argue that a rich type system shifts logic errors into syntax error. An easy example is time arithmetic. Adding seconds to minutes can be problematic. If you have proper types defined (in any language, pythons types do fine for this) then you need to confirm that addition of minutes and seconds is correct in one place, and the type system will guarantee it's done correctly throughout your code. A richer type system allows you to move more logic into type system.

paulddraper 11y ago
s/syntax/type/
- deleted 11y ago
  [deleted]
- agumonkey 11y ago
  Somehow somewhere it's the same, there's some expressions that you cannot write based on the rules you declared.
  - paulddraper 11y ago
    Typically, a syntax is specified by BNF or similar. Every programming language has syntax, not every programming language has static types. I think you can separate these pretty cleanly.
    - dllthomas 11y ago
      > I think you can separate these pretty cleanly. You can, and probably should, but it's more of an engineering distinction than a theoretical one. Syntax and types are both rules for how phrases can fit together. And sometimes it blurs - I understand that at least one C++ compiler parses with an overly general parser, collecting several results and disambiguating with type information. > Every programming language has syntax, not every programming language has static types. Not every programming language has "static syntax" - some allow you to adjust the parser, and some don't do any checking of the whole file (much less the whole program) before they start running the first bits of it.

rtpg 11y ago

The other restrictions brought by languages like Haskell catch classes of error you do see in Python. For example, with django's forms, you are forced to call validation (`form.is_valid()`) before you can get the result of said validation (`form.cleaned_data`) So referencing `form.cleaned_data` before `form.is_valid()` is incorrect.... If you had to port something like Django's forms to Haskell, you could instantly get rid of this issue because such behaviour is impossible to express in the language. In Haskell you would likely write a `validate` function that takes a form, and returns either a validation error or the validated data itself: `let maybeCleanedData = validate form` The type system that makes effects explicit (really, the immutable nature of everything, but one and the other usually synergise well) means that your API is forced to be a saner one. You can take what you learn from these type systems and bring it back to Python though. Like you said, most errors are logic errors. But logic errors can often be helped along by dangerous APIs. Types and removal of stateful code can give you the boundaries to rule out many designs that can come back to bite you.

nickbauman 11y ago

Here's the thing. You're not going to forgo your tests, right? But testing in a statically typed language is much harder to get right. But you still need them. So the question of static or dynamic typing is moot.

chadaustin 11y ago
Why is testing harder in a statically typed language? Seems about the same to me.
- phamilton 11y ago
  Monkey patching is often difficult in a statically types language, but is quite useful in testing.
  - chadaustin 11y ago
    Ah, fair enough! Though monkey patching is only possible in some dynamic languages, namely the ones where classes and modules are mutable hash tables. Note that in ES6, unless you insert some special code via something like babel-rewire, imports can't be monkey patched. Also, Scheme is dynamically-typed and has no monkey patching. Anyway, I agree monkey patching in tests can be pretty convenient! But I personally think it's also a bad idea because it means that your tests are now coupled to the internal implementation of the code under test. That is, if you refactored the implementation, the test could break. Passing testable dependencies explicitly avoids this problem and avoids the need to monkey patch in tests.
    - phamilton 11y ago
      That seems like more of an argument against mocking in general. Even if you DI you are still expecting X method to be called on the mock object and have created that coupling. I think DHH describes a great example that illustrates a big difference in philosophy around this: http://david.heinemeierhansson.com/2012/dependency-injection-is-not-a-virtue.html http://david.heinemeierhansson.com/2012/dependency-injection...

gnuvince 11y ago

> It's quite rare that I've encountered a type error in a Python program. What is your definition of a type error? The point of more advanced type systems is to allow programmers to express more information about the program in the types so that the compiler can check them and report mistakes. I've done my share of Python coding and many of my errors were definitely type errors (even if they didn't necessarily raise TypeError).

chadaustin 11y ago

it's quite rare that I've encountered a type error in a Python program I hear that relatively frequently from people who consider types to be things like functions, strings, integers, and other "representation types". But the benefit of type systems, especially type systems as expressive as Haskell, is that you, many times, can encode your logical invariants in the type system by introducing new nominal types. For example, you can introduce a new type for each type of ID in your system, like CustomerID, ExperimentID, EventID, which prevents you from mixing those up. You can use types to distinguish between mutable and immutable data structures. It's perfectly okay to use object identity when comparing immutable data structures, but it's usually a bug if the data structure is mutable. When you take a more expansive view of what type systems can offer, they're more useful.

jdmichal 11y ago
> It's perfectly okay to use object identity when comparing immutable data structures, but it's usually a bug if the data structure is mutable. I don't understand this statement. The only thing immutability provides here is the ability to know that an object didn't change by knowing that it's the same object. There's no guarantee of value equality from identity unless all objects are interned.
- chadaustin 11y ago
  Ah, yeah, perhaps I should have elaborated more. It's a subtle issue, but it's one that comes up all the time when optimizing React by removing unnecessary renders. With immutable data structures, you know that x == y implies, even if x was initialized a while ago, that the data is the same. With mutable data, that's not true -- perhaps the values referenced by x have changed value in the meantime, so x == y does not imply that the data is the same.
agentultra 11y ago
Encoding an invariant in the type system is definitely a strong benefit of Haskell and other similar languages. You can do more than simple identity/immutability with types. I find the flexibility of the type system to share some similar properties with C++'s more advanced features. Used sparingly they can be quite powerful but come with a complexity that few mortals will be able to comprehend. In a distributed system, for example, you can encode an invariant in the type system that will constrain the execution to only valid states. This is immensely powerful. However you can also model arbitrarily complex computations into the type system which will make sense to no one but the author who wrote it. One thing I do miss in Python that a type system gives you is the compiler's ability to do exhaustive pattern matching. Forcing you to deal with every case explicitly is a huge advantage. In fact, I'm currently working on a formal specification of eventlet's Semaphore class as an exercise (I'm in the process of learning) as we've found just such a bug in a large Python code base where a particular exception is not caught and locks up the whole system. An exhaustive pattern search would have forced the authors to deal with that exception and this bug wouldn't have surfaced.

kpmah 11y ago

You're making an argument from your experience, so permit me to make an argument from mine: I've been using Python and Ruby professionally for about 10 years. The most common error I make myself is typos, but those are often (but not always) fixed quickly. The most common mistake I see getting to production is not handling a return value or an exception because it was assumed it couldn't happen. Types can help with both of these things, and tests less so - because often if you're making an assumption about the return value of a function, it's because you haven't considered the possibility and you don't write a test for it. A dynamic language can certainly be good enough, but in my opinion never ideal.

toolslive 11y ago
Just take any large python project and search the bug trackker for : "AttributeError: 'NoneType' object has no attribute ..." You'll find plenty of those. So people are wasting time tracking and fixing something that could have been found by a machine (a compiler in this case) in microseconds. A colleague of mine once stated: "unit tests are a poor man's compiler".
agentultra 11y ago
Well if you want to get out the yard sticks I've been writing Python for more than 10 years. Exhaustive case matching is very useful, I agree. It is a common error in Python code (and in a similar fashion, to catch all exceptions however inappropriate). > A dynamic language can certainly be good enough, but in my opinion never ideal. If I think about it scientifically there are many cases where Python is ideal. For example the scientific Python stack, Jupyter, etc is very popular and, "ideal," in the sense that people frequently use it to get real work done. They don't have to categorize every expression and can instead focus on the data and transformations. As a data-exploration tool Python can be said to be ideal. It seems ideal too as the implementation language of OpenStack where the community supports over 4+ million lines of Python code. Could OpenStack have been better written in Haskell? Maybe. However thousands of contributors seem quite comfortable with Python and the process around developing reliable infrastructure software seems to catch critical errors in practice. I believe that strongly-typed functional languages are awesome. There are many situations where I'd prefer one over the other. However I don't deal in absolutes and don't believe Haskell is going to be the hammer that screws every dowel.