5 ms·

I have always gotten the impression there was a failure of communication when (without lose of generality) Haskell programmers would tell (also, without loss of

by hawkice 12y ago

I have always gotten the impression there was a failure of communication when (without lose of generality) Haskell programmers would tell (also, without loss of generality) Python programmers that Python only has one type, 'object', which appears to violate the understanding of the Python programmer thoroughly enough that there isn't really even a conversation about what is meant by the comment. The first point dissolves this conversation (because clearly neither the Haskell nor Python programmers are confused about the execution of actual programs). Notably, it dissolves it in a way where that pesky third issue doesn't pop up (which is perhaps the worst of them all, sans _maybe_ the last).

hcarvalhoalves 12y ago
Well, that's an interesting comment. I have almost a decade experience in Python, and having recently picked up Haskell, I clearly see the value of having (or not) a static type system. I have noticed that during all these years I would just "type-check" the various APIs in my mind, or with the aid of the REPL, but it's not as easy when programmers with less experience join the project. I would often have to explain tracebacks about type errors (e.g., tried to call a missing method on `None`, but the programmer didn't expect that API to return `None`). Strong typing avoids errors from propagating, but without static checking only gets you half-way there. I would still use Python (or other dynamic language) to introduce someone to programming - not having to reason about types lowers some barriers - but nowadays I'm not sure it pays off for a project expected to be maintained.
- crdoconnor 12y ago
  I was always on the fence about static typing because I figured that it automatically led to more verbose code (clearly a significant down side), but after looking at Haskell and F# I'm not so sure that's true for them, even though it definitely is for C++ and Java. I'm still unconvinced that additional testing is required to overcome bugs that a static type checker would catch, though. In my experience all of those "call a missing method on None" issues get caught relatively quickly by a test that you would have to write anyway even if you were using a language with static typing.
  - eru 12y ago
    > In my experience all of those "call a missing method on None" issues get caught relatively quickly by a test that you would have to write anyway even if you were using a language with static typing. There are lots of bugs that you still have to test for in a language with a typesystem like Haskell's. But it's not this class of bugs. Pattern matching (and completeness checks) should take care of that.
    - crdoconnor 12y ago
      I know, but my point was that in my experience this class of bug is nearly always a problem at its heart in requirements anyway (i.e. an unspecified edge case), meaning you have to test it in whichever language you use to be confident of the program's correctness. E.g. you'll still need to write a test for your haskell code to determine that the behavior is correct if the IP address is missing, and in your python code if you don't specify behavior it is the kind of thing that will likely lead to one of those nasty "cannot call a method on none" errors. Since the act of testing which is necessary anyway catches it or confirms correct behavior, the additional benefit of a static type checker confirming the presence of such a bug is perhaps lower than it might appear at first glance. This is clearly not true of weakly typed languages where you have to write a myriad number of extra tests just to achieve the same confidence in your code to cover all the unexpected use cases caused by weird type conversions you didn't even realize you were doing.
      - mightybyte 12y ago
        I believe eru's point was that those kinds of tests are not necessary in Haskell because if a function takes something of the type IpAddress, None simply isn't possible. So everywhere IpAddress is used, you don't have to do any of those tests. It sounds like your point is that even in Haskell there will inevitably be boundaries where the None case is an issue. And that's true, namely the point where you call: parseIpAddress :: String -> Maybe IpAddress Somewhere your app will be sucking in a string and you need to have a test for the empty string case. That's true. But the surface area of the application that is susceptible to this problem is reduced (often dramatically). All code that works with IpAddress is free and clear. Whereas in most other languages, every function that takes an IpAddress probably needs to be tested with the None case. If you try to argue that you don't need to test every one, then you're plagued by the difficulty of knowing which need it and which don't. Haskell's types solve that for you completely.
jrochkind1 12y ago
What's the "pesky third issue" again?
- AnimalMuppet 12y ago
  From the article, "Patronizing those outside the faith".
juliangamble 12y ago
The 'uni-typed' argument is interesting, but seems to fall down under further examination. This is a comment from some guys at the University of Indiana, who are neither Python or Haskellers, but are working on advanced type systems: ... however Sam Tobin-Hochstadt argues the uni-typed classification is not very informative in practice. The uni-typed theory reveals little about the nature of programming in a dynamically typed language; it's mainly useful for justifying the existence of "dynamic" types in type theory. Projects like Typed Racket were invented precisely to discover and model the implicit type information utilised by programmers in such languages. Often types are quite accurate, and shows there's a lot more going on than meets the eye. http://stackoverflow.com/a/23286279/15441 http://stackoverflow.com/a/23286279/15441
- tel 12y ago
  You bring up a very interesting point here. The "unityped" argument is a trivializing one, invented to try to draw bright lines between the worlds of static and dynamic typing. But it's ultimately a minimal argument instead of an interesting one. A dynamically typed fragment of code can be interpreted as a program in a statically typed world. From here we can attempt to use inference to partially recover real static information and use it during compilation. This is as old as dynamic languages---typed specialization! It's also a genuinely sophisticated static type system imposed on a genuinely dynamic language. That's an interesting POV from the compiler's perspective, and it should not be ignored. The other interesting perspective, though, and the one of more modern excitement, is that it's less about whether or not a program technically has a particular type but whether or not failure to be expressible at "good" types should be brought to the programmers attention immediately! You can see a statically typed language as a gradually typed language which refuses to compile whenever `any` gets inferred, for instance.
seanmcdirmid 12y ago
To be fair, the type community makes a distinction between types (static entities) and tags (dynamic entities). From their perspective, Python is definitely "tagged" in the sense that tags are checked dynamically, and memory safety is preserved. On the types mailing list, I think Bob Harper conceded the point that maybe it is more useful to use "type" to refer to dynamic tags when talking to practicing programmers; it is just that in the types community, type has a well defined specific meaning (I can't find a link right now since I'm behind the GFW, but can dig it up later if you are interested).
- djur 12y ago
  An alternate viewpoint is that static typing advocates invented a novel categorization that allows them to dismiss typing systems they disagree with. "Tag" doesn't have a consistent theory meaning "type determined at runtime"; on the other hand, "type determined at runtime" has been referred to simply as a "type" for decades.
  - eli_gottlieb 12y ago
    The first type theories by Russell and Church were invented decades before practical computers allowed for programming languages high-level enough to even speak of their being typed or untyped. Type theory is primarily a constructive/computational foundation for mathematics, and secondarily a way of statically proving that programs will not exhibit undefined behavior.
    - tel 12y ago
      (I find it tremendously amusing when people think that computer languages invented types instead of participated in a late-set convergent evolution with type theory.)
      - seanmcdirmid 12y ago
        Type is such a generic word though. You can use the word just by its basic definition (a category of people or things having common characteristics) and everyone would mostly understand what you are talking about. What Russell invented was a theory with types of a more formal definition.

by hawkice 12y ago

hcarvalhoalves 12y ago

Well, that's an interesting comment. I have almost a decade experience in Python, and having recently picked up Haskell, I clearly see the value of having (or not) a static type system. I have noticed that during all these years I would just "type-check" the various APIs in my mind, or with the aid of the REPL, but it's not as easy when programmers with less experience join the project. I would often have to explain tracebacks about type errors (e.g., tried to call a missing method on `None`, but the programmer didn't expect that API to return `None`). Strong typing avoids errors from propagating, but without static checking only gets you half-way there. I would still use Python (or other dynamic language) to introduce someone to programming - not having to reason about types lowers some barriers - but nowadays I'm not sure it pays off for a project expected to be maintained.

crdoconnor 12y ago
I was always on the fence about static typing because I figured that it automatically led to more verbose code (clearly a significant down side), but after looking at Haskell and F# I'm not so sure that's true for them, even though it definitely is for C++ and Java. I'm still unconvinced that additional testing is required to overcome bugs that a static type checker would catch, though. In my experience all of those "call a missing method on None" issues get caught relatively quickly by a test that you would have to write anyway even if you were using a language with static typing.
- eru 12y ago
  > In my experience all of those "call a missing method on None" issues get caught relatively quickly by a test that you would have to write anyway even if you were using a language with static typing. There are lots of bugs that you still have to test for in a language with a typesystem like Haskell's. But it's not this class of bugs. Pattern matching (and completeness checks) should take care of that.
  - crdoconnor 12y ago
    I know, but my point was that in my experience this class of bug is nearly always a problem at its heart in requirements anyway (i.e. an unspecified edge case), meaning you have to test it in whichever language you use to be confident of the program's correctness. E.g. you'll still need to write a test for your haskell code to determine that the behavior is correct if the IP address is missing, and in your python code if you don't specify behavior it is the kind of thing that will likely lead to one of those nasty "cannot call a method on none" errors. Since the act of testing which is necessary anyway catches it or confirms correct behavior, the additional benefit of a static type checker confirming the presence of such a bug is perhaps lower than it might appear at first glance. This is clearly not true of weakly typed languages where you have to write a myriad number of extra tests just to achieve the same confidence in your code to cover all the unexpected use cases caused by weird type conversions you didn't even realize you were doing.
    - mightybyte 12y ago
      I believe eru's point was that those kinds of tests are not necessary in Haskell because if a function takes something of the type IpAddress, None simply isn't possible. So everywhere IpAddress is used, you don't have to do any of those tests. It sounds like your point is that even in Haskell there will inevitably be boundaries where the None case is an issue. And that's true, namely the point where you call: parseIpAddress :: String -> Maybe IpAddress Somewhere your app will be sucking in a string and you need to have a test for the empty string case. That's true. But the surface area of the application that is susceptible to this problem is reduced (often dramatically). All code that works with IpAddress is free and clear. Whereas in most other languages, every function that takes an IpAddress probably needs to be tested with the None case. If you try to argue that you don't need to test every one, then you're plagued by the difficulty of knowing which need it and which don't. Haskell's types solve that for you completely.

jrochkind1 12y ago

What's the "pesky third issue" again?

AnimalMuppet 12y ago
From the article, "Patronizing those outside the faith".

juliangamble 12y ago

The 'uni-typed' argument is interesting, but seems to fall down under further examination. This is a comment from some guys at the University of Indiana, who are neither Python or Haskellers, but are working on advanced type systems: ... however Sam Tobin-Hochstadt argues the uni-typed classification is not very informative in practice. The uni-typed theory reveals little about the nature of programming in a dynamically typed language; it's mainly useful for justifying the existence of "dynamic" types in type theory. Projects like Typed Racket were invented precisely to discover and model the implicit type information utilised by programmers in such languages. Often types are quite accurate, and shows there's a lot more going on than meets the eye. http://stackoverflow.com/a/23286279/15441 http://stackoverflow.com/a/23286279/15441

tel 12y ago
You bring up a very interesting point here. The "unityped" argument is a trivializing one, invented to try to draw bright lines between the worlds of static and dynamic typing. But it's ultimately a minimal argument instead of an interesting one. A dynamically typed fragment of code can be interpreted as a program in a statically typed world. From here we can attempt to use inference to partially recover real static information and use it during compilation. This is as old as dynamic languages---typed specialization! It's also a genuinely sophisticated static type system imposed on a genuinely dynamic language. That's an interesting POV from the compiler's perspective, and it should not be ignored. The other interesting perspective, though, and the one of more modern excitement, is that it's less about whether or not a program technically has a particular type but whether or not failure to be expressible at "good" types should be brought to the programmers attention immediately! You can see a statically typed language as a gradually typed language which refuses to compile whenever `any` gets inferred, for instance.

seanmcdirmid 12y ago

To be fair, the type community makes a distinction between types (static entities) and tags (dynamic entities). From their perspective, Python is definitely "tagged" in the sense that tags are checked dynamically, and memory safety is preserved. On the types mailing list, I think Bob Harper conceded the point that maybe it is more useful to use "type" to refer to dynamic tags when talking to practicing programmers; it is just that in the types community, type has a well defined specific meaning (I can't find a link right now since I'm behind the GFW, but can dig it up later if you are interested).

djur 12y ago
An alternate viewpoint is that static typing advocates invented a novel categorization that allows them to dismiss typing systems they disagree with. "Tag" doesn't have a consistent theory meaning "type determined at runtime"; on the other hand, "type determined at runtime" has been referred to simply as a "type" for decades.
- eli_gottlieb 12y ago
  The first type theories by Russell and Church were invented decades before practical computers allowed for programming languages high-level enough to even speak of their being typed or untyped. Type theory is primarily a constructive/computational foundation for mathematics, and secondarily a way of statically proving that programs will not exhibit undefined behavior.
  - tel 12y ago
    (I find it tremendously amusing when people think that computer languages invented types instead of participated in a late-set convergent evolution with type theory.)
    - seanmcdirmid 12y ago
      Type is such a generic word though. You can use the word just by its basic definition (a category of people or things having common characteristics) and everyone would mostly understand what you are talking about. What Russell invented was a theory with types of a more formal definition.