13 ms·

Talking about “types”

152 points by jashkenas 12y ago

egonschiele 12y ago
Oh good, a discussion on typed vs untyped. I expect this will be a solid exchange of ideas, with each side trying to learn something from the other side.
- untothebreach 12y ago
  Did you read the article? It is actually quite refreshing in it's tone: Patronising those outside the faith If somebody stays away from typed languages, it doesn't mean they're stupid, or lack education, or are afraid of maths. There are entirely valid practical reasons for staying away. Please drop the condescending tone.
  - egonschiele 12y ago
    Regarding that particular section, I agree with this comment: http://www.reddit.com/r/haskell/comments/2ijwwz/seven_deadly_sins_of_talking_about_types_cross/cl2u82b http://www.reddit.com/r/haskell/comments/2ijwwz/seven_deadly... And overall I agree with this: http://www.reddit.com/r/programming/comments/2ijt11/seven_deadly_sins_of_talking_about_types/cl2slxn http://www.reddit.com/r/programming/comments/2ijt11/seven_de... > People who I enjoy discussing issues with bow out of the discussion the same way they do when people bring up emacs vs. vim. They know they aren't going to hear anything new, so why bother? That's how I felt after reading this: "why did I bother?"
deleted 12y ago
[deleted]
emotionalcode 12y ago
> Now that I've ranted my heart out, here's a coda that attempts to be constructive. As I mentioned, part of the problem is that we equivocate when talking about “types”. Instead of saying “type” or “type system”, I encourage anyone to check whether anything from the following alternative vocabulary will communicate the intended meaning. Deciding which term is appropriate is a good mental exercise for figuring out what meaning is actually intended. > * data abstraction > * data type > * predicate, proposition > * proof, proof system > * interface specification [language] > * [compile-time] checker > * specification, verification > * invariant (the thing that “types” are usually specifying!) I add precondition, postcondition, state. As well, I think the space in between has importance: map, transformer, relation, command. Formalization is tricky, from my understanding.
jashkenas 12y ago
This is a bit of a nit to pick, but once again, I'm mystified as to why the HN front page mods changed the title of this submission. I had it as: "The Seven Deadly Sins of Talking About Types", which also happens to be the title of the blog post itself, give or take a definite article. What gives?
- GeneralMayhem 12y ago
  My guess would be it's an application of: >If the original title begins with a number or number + gratuitous adjective, we'd appreciate it if you'd crop it. E.g. translate "10 Ways To Do X" to "How To Do X," and "14 Amazing Ys" to "Ys." Exception: when the number is meaningful, e.g. "The 5 Platonic Solids." https://news.ycombinator.com/newsguidelines.html https://news.ycombinator.com/newsguidelines.html
  - titanomachy 12y ago
    These guidelines are really strict, but I have to say I like the results in general. I can usually tell by the title if something is likely to contain information that's interesting to me, unlike with many news sites.
  - jashkenas 12y ago
    > Exception: when the number is meaningful As it is in this case: http://en.wikipedia.org/wiki/Seven_deadly_sins http://en.wikipedia.org/wiki/Seven_deadly_sins If a (some might say, literary) allusion has no place on Hacker News, just because it happens to have a number in it, then the small-minded literalists have really taken over this joint.
    - forthefuture 12y ago
      You don't need to know the seven deadly sins to know anything about types. They could have had 5 or 8 sins having to do with types and the content wouldn't have changed. That's pretty much the definition of unnecessary.
z3t4 12y ago
Doesn't all modern programming languages has Loose typing? It allows more abstraction. Like for example in JavaScript where a object can be anything!
- AnimalMuppet 12y ago
  No. Some (more or less) modern languages have loose typing. Some modern languages have quite strict typing (Haskell for instance, but there are others).
- steveklabnik 12y ago
  'loose' typing isn't a word normally used when talking about type systems. Most people work with a two-axes "strong" vs "weak" and "dynamic" vs "static" system. But very, very few languages are 'weakly' typed, to the point of it almost being a silly way to talk about them. Ruby, for example, is Dynamic and Strong. Then there's the 'types' vs 'tags' issue...
  - kyllo 12y ago
    But very, very few languages are 'weakly' typed, to the point of it almost being a silly way to talk about them. Like Perl and PHP? Perhaps few (in number) languages are weakly typed, but they're also a few of the most commonly used languages in existence.
    - chrisseaton 12y ago
      There's no good accepted definition of weak vs strong typing in the literature, but I don't think many people would agree that PHP or Perl are weakly typed. I would say they are both strongly, and dynamically, typed. Can you argue otherwise?
      - kyllo 12y ago
        Here's a trivial example of what I mean by strong vs. weak typing in dynamic languages: Python (strongly typed): >>>1 + "1" Traceback (most recent call last): File "<stdin>", line 1, in <module> TypeError: unsupported operand type(s) for +: 'int' and 'str' Ruby (also strongly typed): irb(main):001:0> 1 + "1" TypeError: String can't be coerced into Fixnum from (irb):1:in `+' from (irb):1 from C:/Ruby193/bin/irb:12:in `<main>' PHP (weakly typed): echo 1 + "1"; 2 Perl (also weakly typed): print 1 + "1"; 2
StefanKarpinski 12y ago
Bravo. This is the best thing I've read anywhere about the general issue of types, both static and dynamic. It is even-handed, acknowledging the benefits and limitations of both static and dynamic languages, and incredibly well-informed. I now have something to send to the next person that threatens to send me a copy of PFPL.
- tome 12y ago
  But unfortunately it doesn't say anything concrete about what the benefits and limitations of static and dynamic languages are.
  - brandonbloom 12y ago
    s/But unfortunately/One of the best things about this article is that/
  - yogthos 12y ago
    That's because we don't actually have any concrete evidence one way or the other. This is the biggest problem with the whole static/dynamic debate. Until there are studies that clearly demonstrate that projects written in statically typed languages have statistically less defects, are developed faster, or are easier to maintain, it's all anecdotal evidence. There are tons of large real world projects developed in both static and dynamic languages, there's very little indication that projects developed in dynamic languages have significantly more defects or that they're more difficult to maintain. In fact, some of the largest and most robust applications are written in Erlang. See the paper from Joe Armstrong as an example (https://www.sics.se/~joe/thesis/armstrong_thesis_2003.pdf https://www.sics.se/~joe/thesis/armstrong_thesis_2003.pdf).
    - mpweiher 12y ago
      > That's because we don't actually have any concrete evidence one way or the other. We do have some evidence that if there are differences in safety, they appear to be less than overwhelming, see http://blog.metaobject.com/2014/06/the-safyness-of-static-typing.html http://blog.metaobject.com/2014/06/the-safyness-of-static-ty... One can debate how viable the evidence is, but at least it is some evidence. However, there does appear to be some evidence that static typing helps with program comprehension/navigation, for example: http://dl.acm.org/citation.cfm?id=2568299 http://dl.acm.org/citation.cfm?id=2568299 Again, not overwhelming, but some evidence.
kazinator 12y ago
> If somebody stays away from typed languages, ... These people who stay away from typed languages, who are they and what are they using? Shell? Awk? Assembler? When is a language untyped: is it when you can misuse an operand by applying the wrong operation, with no diagnosis and strange, non-portable consequences? Or is when the character string "1.3" can be used as an arithmetic operand, automatically becoming a floating-point approximation of "1.3"? (If that is "untyped", how is it that "1.3" is identified as a character string, and how is the context identified as requiring an arithmetic operand?) Or is it untyped when wrong type operands do something unpredictable, but dumb? Bash: $ string=abcd echo $(( string + 3 )) 3 $ number=4 $ echo $(( number + 3 )) 7 That must be untyped. No?
- freyrs3 12y ago
  > When is a language untyped There's the formal definition of type and there's the colloquial definition of type. A type in the context of the article means a formal type, it is an syntactic classifier that is part of the static semantics of the language. The properties you describe ( string/number exceptions ) are part of the dynamics of the language, which is a separate concept. Dynamically typed languages quite often use boxed values with an attached runtime tags which are colloquially referred to as "types" even though they have nothing to do with static types. If you read the article in the context of "type" meaning "static type" it will make more sense.
  - kazinator 12y ago
    Does that mean I can search and replace every occurrence of "type" in the article with "static type"? Are you sure dynamic types have nothing to do with static types? What about compilers for dynamic languages which reason about type, like that if the program calls (symbol-name x), it is inferred that x must hold a string, so that a subsequent (cos x) is inconsistent? Is such a compiler is reasoning about something which has nothing to do with static type?
    - kd0amg 12y ago
      Are you sure dynamic types have nothing to do with static types? "Static type" does not really mean "class of values." That is a common use of static types, but they can also be used for things like tracking what resources are available/released or describing what exceptions a function might raise.
mej10 12y ago
"Rich Hickey's transducers talk gave a nice example of how patterns of polymorphism which humans find comprehensible can easily become extremely hard to capture precisely in a logic." I haven't watched his talk, but Rich Hickey also commented on /r/Haskell with the types. It doesn't seem like it was that difficult to capture. There are also other comments that approach the types from different angles and achieve some success. Maybe this isn't a good example for this thesis? http://www.reddit.com/r/haskell/comments/2cv6l4/clojures_transducers_are_perverse_lenses/cjjyay7 http://www.reddit.com/r/haskell/comments/2cv6l4/clojures_tra...
- swannodette 12y ago
  I don't think anything in that Reddit thread was conclusive, nor did they capture all of their properties (early termination, cleanup step).
  - deleted 12y ago
    [deleted]
  - bkirwi 12y ago
    Yep, that's right. There seem to be a few factors involved: - Most of that discussion happened before a full description of transducers was up anywhere, so a lot of these details are just completely missing. - Haskell's type system is not expressive enough to capture certain interesting properties, like linearity. (To be clear, it's quite possible to translate any arbitrary transducer into Haskell -- but the type system will not prevent all the mistakes it is possible to make.) - There are different classes of transducers that Haskell people actively would not want to have identical types. (ie. stateful vs. stateless, early-terminating vs. unbounded) Many of the discussions revolve only one or a few of these classes -- typically the stateless unbounded version, which turns out to have a particularly simple encoding, but it definitely varies.
  - tel 12y ago
    Those, I believe, are fairly easy to capture in the `Moore b r -> Moore a r` formulation. It also captures linearity. That said, I think the more general formulation is something like Fold or Traversal in Lens which operates polymorphically over the whole thing with a type that a refinement of Profunctor p => p a b -> p s t where such a type generalizes all of the concrete Haskell formulations.
colanderman 12y ago
This article says many things that need to be said, but I take issue with this: > No sane person can argue that we want to bifurcate a programming language into distinct base-level and type-level fragments. Well, I must be insane then. I much prefer writing type expressions in a language free from, say, mutation and iteration. Restricting languages aids not only computers which analyze programs, but also humans which create programs. It's much easier to remember, say, "I'm not allowed to mutate anything, there's no syntax for it", than, "I can use mutation, but if I use it in such-and-such a way, then compiler won't be able to statically determine the type, unless I have version 4.2.3 or later".
- imanaccount247 12y ago
  I think most of the article is as bad as the part you are criticizing. The part you refer to is just particularly bad in it's presentation. Making unsupported claims while declaring oneself correct and anyone who disagrees is not sane is not helpful or productive.
  - ubernostrum 12y ago
    There is precedent that these types of splits don't make things as safe as advocates believe. Amusingly, the precedent is part of the foundational bits of modern theoretical CS :)
    - colanderman 12y ago
      Care to explain? Keep in mind I'm not talking about safety; I'm talking about usability.
      - ubernostrum 12y ago
        The short version is to look at the early twentieth-century work on formal systems, languages and metalanguages, etc., and then notice how those particular sandcastles got kicked over by the incompleteness theorems. By the way, personally I tend to look at type systems in terms of the tradeoffs they make. It certainly seems to me like the diminishing-returns point -- where writing verifiable code within a "more expressive" type system becomes more work than writing unverifiable code in a "less expressive" system and dealing with any bugs after the fact -- has already been passed by some of the popular FP languages.
vilhelm_s 12y ago
Certainly very sensible points. But I take some issue with the bits towards the end: > Fetishising Curry-Howard Hey, I happen to find Curry-Howard sexy, you have no right to shame me! > To specify and check liveness or reachability, we need to represent programs as some kind of flow graph, where flows are very likely to span multiple functions and multiple modules. But no, this is exactly what basing systems on Curry-Howard (with terminating functions) buys you. If I give a HTTP response handler in Coq the type HttpRequest -> HttpResponse I know it is live, because the function is total. And similarly, dead code paths can be gotten rid of by eliminating a proof of False. So this lets you state liveness and unreachability. Of course, the proofs of those statements is very different from program-analysis-style systems. In a whole-program analysis, the analyser goes over the entire program, and at the end it says "well, I could not find anything calling this function, so I guess it's dead". In a Curry-Howard-style system, you need to look at the function and figure out when it should be called and what preconditions need to be true for it to work properly. But this is exactly why people like type systems, you can think about programs modularly rather than all at once.
- skybrian 12y ago
  I suppose, but outside certain mathematical systems that are designed that way, assuming that all functions are total is unrealistic. The languages we use every day are Turing-complete languages and infinite loops can happen.
  - vilhelm_s 12y ago
    You don't have to assume everything is total, you just need to track in the type system which things are and which aren't. E.g. you could also give it the type HttpRequest -> IO HttpResponse where IO is some type allowing nontermination (e.g. defined coinductively along the lines of http://www.cs.swan.ac.uk/~csetzer/slides/goeteborg2009AgdaIntensiveMeeting.pdf http://www.cs.swan.ac.uk/~csetzer/slides/goeteborg2009AgdaIn...). Having a type for total functions gives you the option to state and prove totality properties, even if you maybe don't want to go through the effort of doing that for every function you write.
porker 12y ago
I posted this 4 hours before jashkenas (https://news.ycombinator.com/item?id=8420560 https://news.ycombinator.com/item?id=8420560) - why the duplicate?
- jashkenas 12y ago
  Because the /newest page is fortune's fickle wheel, where worthy essays like this one are lost, more frequently than not, in the flood of spammy chaff. I thought it was worthwhile, so I submitted it again. We got lucky this time ;)
- deleted 12y ago
  [deleted]
tikhonj 12y ago
This whole article is a reflection of a belief that I really don't like but is all too common these days. It's the idea that nothing is better than anything else, everything is a trade-off and strong positive are inherently wrong. I don't buy it. It's a tacit assumption that, somehow, everything is on the Pareto frontier. Profoundly implausible. In the background, it's basically a hybrid appeal to moderation (all extreme positions are wrong) and popularity (if so many people are doing something, it can't be wrong). Never mind the fact that popularity is almost meaningless, driven by fashion more than anything, and that what's "extreme" is arbitrary and largely driven by popularity itself... This is how we get "worse is better"; this is how we get standards that are compromises ideal for nobody but still widely adopted because they're standard or because that seems like the thing to do or because that's what everyone else is doing or because " engineering". The worst part is that this all goes unsaid, assumed correct by default. Just the fact that we're having the discussion the article wants, and not this meta-discussion, implicitly elevates its premise! Some things are better than others. A strong debate between strong positions is healthier than an artificial social force reverting everyone back to mean. Now, all this is not to say the usual message about types is perfect. It could definitely be improved in many different ways. But not by muzzling, weakening or qualifying: not by most of the argument's suggestions. Especially ironic is the rhetorical techniques the author uses to argue against rhetoric. The one I personally find the most grating—beyond the ambient implication that everything is equal that I've just written about—is establishing cheap credibility by aligning himself with the camp he's arguing against. "I like X, but..." Or, in this case, "I use OCaml, but..." Then again, my pointing this out is probably ironic in the same way. Or is it?
- skybrian 12y ago
  It seems more unrealistic to assume everyone agrees on the same cost-benefit function. We are different people and value different things. So in any attempt at a proof involving what should be valued more, you have to state your assumptions and they're generally debatable.
  - cantankerous 12y ago
    There's also the bit of refusing to agree to the same cost benefit function because it commits you to a standard that you can't back away from. I mean look at the global warming debate, for example.
ericssmith 12y ago
Sinner here. But I could only identify with four of the seven. Mostly because I couldn't make sense of his rhetoric for the other three. > I imagine that my passions are still rather thinly veiled in places You got that right. But I don't deny you your right to be as passionate about it as you like. It's a debate after all.
chrismorgan 12y ago
In my defence, on the question of header typing, I did mention that these were not things that couldn’t be done in dynamically typed languages, but rather that they were more dangerous in such languages, that it was the assurance of correctness that languages like Rust get you. A strongly typed header scheme is absolutely possible in Python, but the risks are considerably higher. I certainly agree that there were a few points that I didn’t substantiate or provide sufficient evidence for—I was deliberately intending to be broad and wanting people to think about these things, rather than going down rabbit holes. I’m afraid that half an hour really isn’t long to talk about such things in detail.
mercurial 12y ago
I take objection with the article regarding "Pretending that syntactic overhead is the issue". Or rather, I would say it's an incomplete way of looking at it. Non-statically typed languages (I'm thinking reasonably full-featured languages like Perl, Python or Ruby, not Bash) are, IMHO, go-to languages for certain tasks because they allow you to get results quickly. How? * Less typing (there is freedom in being able to cobble together a reasonably complex program in a single file of a few hundred lines in an editor, vs a number of files and thousands of lines in a IDE). * Advanced features! It is only now that closures, first-class functions, etc, start to trickle down to mainstream, statically typed languages. And they do make for shorter programs (see, eg, the post on expired links on HN). Of course, it's not to say that non-statically typed programs don't suffer from a number of drawbacks, but dismissing conciseness as something trivial does not, I think, accurately reflect reasons for why people use this kind of language.
cbd1984 12y ago
For reference, here's the difference: Strong typing ensures all results are well-defined, as the result of a specification, and it uses type information to do that. Weak typing throws away type information, so it can no longer uphold such specifications. Note that auto-conversion and error on mismatch are both evidence of strong typing in action, because both behaviors rely on type information in order to occur.

152 points by jashkenas 12y ago

Oh good, a discussion on typed vs untyped. I expect this will be a solid exchange of ideas, with each side trying to learn something from the other side.

untothebreach 12y ago
Did you read the article? It is actually quite refreshing in it's tone: Patronising those outside the faith If somebody stays away from typed languages, it doesn't mean they're stupid, or lack education, or are afraid of maths. There are entirely valid practical reasons for staying away. Please drop the condescending tone.
- egonschiele 12y ago
  Regarding that particular section, I agree with this comment: http://www.reddit.com/r/haskell/comments/2ijwwz/seven_deadly_sins_of_talking_about_types_cross/cl2u82b http://www.reddit.com/r/haskell/comments/2ijwwz/seven_deadly... And overall I agree with this: http://www.reddit.com/r/programming/comments/2ijt11/seven_deadly_sins_of_talking_about_types/cl2slxn http://www.reddit.com/r/programming/comments/2ijt11/seven_de... > People who I enjoy discussing issues with bow out of the discussion the same way they do when people bring up emacs vs. vim. They know they aren't going to hear anything new, so why bother? That's how I felt after reading this: "why did I bother?"

deleted 12y ago

[deleted]

emotionalcode 12y ago

> Now that I've ranted my heart out, here's a coda that attempts to be constructive. As I mentioned, part of the problem is that we equivocate when talking about “types”. Instead of saying “type” or “type system”, I encourage anyone to check whether anything from the following alternative vocabulary will communicate the intended meaning. Deciding which term is appropriate is a good mental exercise for figuring out what meaning is actually intended. > * data abstraction > * data type > * predicate, proposition > * proof, proof system > * interface specification [language] > * [compile-time] checker > * specification, verification > * invariant (the thing that “types” are usually specifying!) I add precondition, postcondition, state. As well, I think the space in between has importance: map, transformer, relation, command. Formalization is tricky, from my understanding.

jashkenas 12y ago

This is a bit of a nit to pick, but once again, I'm mystified as to why the HN front page mods changed the title of this submission. I had it as: "The Seven Deadly Sins of Talking About Types", which also happens to be the title of the blog post itself, give or take a definite article. What gives?

GeneralMayhem 12y ago
My guess would be it's an application of: >If the original title begins with a number or number + gratuitous adjective, we'd appreciate it if you'd crop it. E.g. translate "10 Ways To Do X" to "How To Do X," and "14 Amazing Ys" to "Ys." Exception: when the number is meaningful, e.g. "The 5 Platonic Solids." https://news.ycombinator.com/newsguidelines.html https://news.ycombinator.com/newsguidelines.html
- titanomachy 12y ago
  These guidelines are really strict, but I have to say I like the results in general. I can usually tell by the title if something is likely to contain information that's interesting to me, unlike with many news sites.
- jashkenas 12y ago
  > Exception: when the number is meaningful As it is in this case: http://en.wikipedia.org/wiki/Seven_deadly_sins http://en.wikipedia.org/wiki/Seven_deadly_sins If a (some might say, literary) allusion has no place on Hacker News, just because it happens to have a number in it, then the small-minded literalists have really taken over this joint.
  - forthefuture 12y ago
    You don't need to know the seven deadly sins to know anything about types. They could have had 5 or 8 sins having to do with types and the content wouldn't have changed. That's pretty much the definition of unnecessary.

z3t4 12y ago

Doesn't all modern programming languages has Loose typing? It allows more abstraction. Like for example in JavaScript where a object can be anything!

AnimalMuppet 12y ago
No. Some (more or less) modern languages have loose typing. Some modern languages have quite strict typing (Haskell for instance, but there are others).
steveklabnik 12y ago
'loose' typing isn't a word normally used when talking about type systems. Most people work with a two-axes "strong" vs "weak" and "dynamic" vs "static" system. But very, very few languages are 'weakly' typed, to the point of it almost being a silly way to talk about them. Ruby, for example, is Dynamic and Strong. Then there's the 'types' vs 'tags' issue...
- kyllo 12y ago
  But very, very few languages are 'weakly' typed, to the point of it almost being a silly way to talk about them. Like Perl and PHP? Perhaps few (in number) languages are weakly typed, but they're also a few of the most commonly used languages in existence.
  - chrisseaton 12y ago
    There's no good accepted definition of weak vs strong typing in the literature, but I don't think many people would agree that PHP or Perl are weakly typed. I would say they are both strongly, and dynamically, typed. Can you argue otherwise?
    - kyllo 12y ago
      Here's a trivial example of what I mean by strong vs. weak typing in dynamic languages: Python (strongly typed): >>>1 + "1" Traceback (most recent call last): File "<stdin>", line 1, in <module> TypeError: unsupported operand type(s) for +: 'int' and 'str' Ruby (also strongly typed): irb(main):001:0> 1 + "1" TypeError: String can't be coerced into Fixnum from (irb):1:in `+' from (irb):1 from C:/Ruby193/bin/irb:12:in `<main>' PHP (weakly typed): echo 1 + "1"; 2 Perl (also weakly typed): print 1 + "1"; 2

StefanKarpinski 12y ago

Bravo. This is the best thing I've read anywhere about the general issue of types, both static and dynamic. It is even-handed, acknowledging the benefits and limitations of both static and dynamic languages, and incredibly well-informed. I now have something to send to the next person that threatens to send me a copy of PFPL.

tome 12y ago
But unfortunately it doesn't say anything concrete about what the benefits and limitations of static and dynamic languages are.
- brandonbloom 12y ago
  s/But unfortunately/One of the best things about this article is that/
- yogthos 12y ago
  That's because we don't actually have any concrete evidence one way or the other. This is the biggest problem with the whole static/dynamic debate. Until there are studies that clearly demonstrate that projects written in statically typed languages have statistically less defects, are developed faster, or are easier to maintain, it's all anecdotal evidence. There are tons of large real world projects developed in both static and dynamic languages, there's very little indication that projects developed in dynamic languages have significantly more defects or that they're more difficult to maintain. In fact, some of the largest and most robust applications are written in Erlang. See the paper from Joe Armstrong as an example (https://www.sics.se/~joe/thesis/armstrong_thesis_2003.pdf https://www.sics.se/~joe/thesis/armstrong_thesis_2003.pdf).
  - mpweiher 12y ago
    > That's because we don't actually have any concrete evidence one way or the other. We do have some evidence that if there are differences in safety, they appear to be less than overwhelming, see http://blog.metaobject.com/2014/06/the-safyness-of-static-typing.html http://blog.metaobject.com/2014/06/the-safyness-of-static-ty... One can debate how viable the evidence is, but at least it is some evidence. However, there does appear to be some evidence that static typing helps with program comprehension/navigation, for example: http://dl.acm.org/citation.cfm?id=2568299 http://dl.acm.org/citation.cfm?id=2568299 Again, not overwhelming, but some evidence.

kazinator 12y ago

> If somebody stays away from typed languages, ... These people who stay away from typed languages, who are they and what are they using? Shell? Awk? Assembler? When is a language untyped: is it when you can misuse an operand by applying the wrong operation, with no diagnosis and strange, non-portable consequences? Or is when the character string "1.3" can be used as an arithmetic operand, automatically becoming a floating-point approximation of "1.3"? (If that is "untyped", how is it that "1.3" is identified as a character string, and how is the context identified as requiring an arithmetic operand?) Or is it untyped when wrong type operands do something unpredictable, but dumb? Bash: $ string=abcd echo $(( string + 3 )) 3 $ number=4 $ echo $(( number + 3 )) 7 That must be untyped. No?

freyrs3 12y ago
> When is a language untyped There's the formal definition of type and there's the colloquial definition of type. A type in the context of the article means a formal type, it is an syntactic classifier that is part of the static semantics of the language. The properties you describe ( string/number exceptions ) are part of the dynamics of the language, which is a separate concept. Dynamically typed languages quite often use boxed values with an attached runtime tags which are colloquially referred to as "types" even though they have nothing to do with static types. If you read the article in the context of "type" meaning "static type" it will make more sense.
- kazinator 12y ago
  Does that mean I can search and replace every occurrence of "type" in the article with "static type"? Are you sure dynamic types have nothing to do with static types? What about compilers for dynamic languages which reason about type, like that if the program calls (symbol-name x), it is inferred that x must hold a string, so that a subsequent (cos x) is inconsistent? Is such a compiler is reasoning about something which has nothing to do with static type?
  - kd0amg 12y ago
    Are you sure dynamic types have nothing to do with static types? "Static type" does not really mean "class of values." That is a common use of static types, but they can also be used for things like tracking what resources are available/released or describing what exceptions a function might raise.

mej10 12y ago

"Rich Hickey's transducers talk gave a nice example of how patterns of polymorphism which humans find comprehensible can easily become extremely hard to capture precisely in a logic." I haven't watched his talk, but Rich Hickey also commented on /r/Haskell with the types. It doesn't seem like it was that difficult to capture. There are also other comments that approach the types from different angles and achieve some success. Maybe this isn't a good example for this thesis? http://www.reddit.com/r/haskell/comments/2cv6l4/clojures_transducers_are_perverse_lenses/cjjyay7 http://www.reddit.com/r/haskell/comments/2cv6l4/clojures_tra...

swannodette 12y ago
I don't think anything in that Reddit thread was conclusive, nor did they capture all of their properties (early termination, cleanup step).
- deleted 12y ago
  [deleted]
- bkirwi 12y ago
  Yep, that's right. There seem to be a few factors involved: - Most of that discussion happened before a full description of transducers was up anywhere, so a lot of these details are just completely missing. - Haskell's type system is not expressive enough to capture certain interesting properties, like linearity. (To be clear, it's quite possible to translate any arbitrary transducer into Haskell -- but the type system will not prevent all the mistakes it is possible to make.) - There are different classes of transducers that Haskell people actively would not want to have identical types. (ie. stateful vs. stateless, early-terminating vs. unbounded) Many of the discussions revolve only one or a few of these classes -- typically the stateless unbounded version, which turns out to have a particularly simple encoding, but it definitely varies.
- tel 12y ago
  Those, I believe, are fairly easy to capture in the `Moore b r -> Moore a r` formulation. It also captures linearity. That said, I think the more general formulation is something like Fold or Traversal in Lens which operates polymorphically over the whole thing with a type that a refinement of Profunctor p => p a b -> p s t where such a type generalizes all of the concrete Haskell formulations.

colanderman 12y ago

This article says many things that need to be said, but I take issue with this: > No sane person can argue that we want to bifurcate a programming language into distinct base-level and type-level fragments. Well, I must be insane then. I much prefer writing type expressions in a language free from, say, mutation and iteration. Restricting languages aids not only computers which analyze programs, but also humans which create programs. It's much easier to remember, say, "I'm not allowed to mutate anything, there's no syntax for it", than, "I can use mutation, but if I use it in such-and-such a way, then compiler won't be able to statically determine the type, unless I have version 4.2.3 or later".

imanaccount247 12y ago
I think most of the article is as bad as the part you are criticizing. The part you refer to is just particularly bad in it's presentation. Making unsupported claims while declaring oneself correct and anyone who disagrees is not sane is not helpful or productive.
- ubernostrum 12y ago
  There is precedent that these types of splits don't make things as safe as advocates believe. Amusingly, the precedent is part of the foundational bits of modern theoretical CS :)
  - colanderman 12y ago
    Care to explain? Keep in mind I'm not talking about safety; I'm talking about usability.
    - ubernostrum 12y ago
      The short version is to look at the early twentieth-century work on formal systems, languages and metalanguages, etc., and then notice how those particular sandcastles got kicked over by the incompleteness theorems. By the way, personally I tend to look at type systems in terms of the tradeoffs they make. It certainly seems to me like the diminishing-returns point -- where writing verifiable code within a "more expressive" type system becomes more work than writing unverifiable code in a "less expressive" system and dealing with any bugs after the fact -- has already been passed by some of the popular FP languages.

vilhelm_s 12y ago

Certainly very sensible points. But I take some issue with the bits towards the end: > Fetishising Curry-Howard Hey, I happen to find Curry-Howard sexy, you have no right to shame me! > To specify and check liveness or reachability, we need to represent programs as some kind of flow graph, where flows are very likely to span multiple functions and multiple modules. But no, this is exactly what basing systems on Curry-Howard (with terminating functions) buys you. If I give a HTTP response handler in Coq the type HttpRequest -> HttpResponse I know it is live, because the function is total. And similarly, dead code paths can be gotten rid of by eliminating a proof of False. So this lets you state liveness and unreachability. Of course, the proofs of those statements is very different from program-analysis-style systems. In a whole-program analysis, the analyser goes over the entire program, and at the end it says "well, I could not find anything calling this function, so I guess it's dead". In a Curry-Howard-style system, you need to look at the function and figure out when it should be called and what preconditions need to be true for it to work properly. But this is exactly why people like type systems, you can think about programs modularly rather than all at once.

skybrian 12y ago
I suppose, but outside certain mathematical systems that are designed that way, assuming that all functions are total is unrealistic. The languages we use every day are Turing-complete languages and infinite loops can happen.
- vilhelm_s 12y ago
  You don't have to assume everything is total, you just need to track in the type system which things are and which aren't. E.g. you could also give it the type HttpRequest -> IO HttpResponse where IO is some type allowing nontermination (e.g. defined coinductively along the lines of http://www.cs.swan.ac.uk/~csetzer/slides/goeteborg2009AgdaIntensiveMeeting.pdf http://www.cs.swan.ac.uk/~csetzer/slides/goeteborg2009AgdaIn...). Having a type for total functions gives you the option to state and prove totality properties, even if you maybe don't want to go through the effort of doing that for every function you write.

porker 12y ago

I posted this 4 hours before jashkenas (https://news.ycombinator.com/item?id=8420560 https://news.ycombinator.com/item?id=8420560) - why the duplicate?

jashkenas 12y ago
Because the /newest page is fortune's fickle wheel, where worthy essays like this one are lost, more frequently than not, in the flood of spammy chaff. I thought it was worthwhile, so I submitted it again. We got lucky this time ;)
deleted 12y ago
[deleted]

tikhonj 12y ago

This whole article is a reflection of a belief that I really don't like but is all too common these days. It's the idea that nothing is better than anything else, everything is a trade-off and strong positive are inherently wrong. I don't buy it. It's a tacit assumption that, somehow, everything is on the Pareto frontier. Profoundly implausible. In the background, it's basically a hybrid appeal to moderation (all extreme positions are wrong) and popularity (if so many people are doing something, it can't be wrong). Never mind the fact that popularity is almost meaningless, driven by fashion more than anything, and that what's "extreme" is arbitrary and largely driven by popularity itself... This is how we get "worse is better"; this is how we get standards that are compromises ideal for nobody but still widely adopted because they're standard or because that seems like the thing to do or because that's what everyone else is doing or because " engineering". The worst part is that this all goes unsaid, assumed correct by default. Just the fact that we're having the discussion the article wants, and not this meta-discussion, implicitly elevates its premise! Some things are better than others. A strong debate between strong positions is healthier than an artificial social force reverting everyone back to mean. Now, all this is not to say the usual message about types is perfect. It could definitely be improved in many different ways. But not by muzzling, weakening or qualifying: not by most of the argument's suggestions. Especially ironic is the rhetorical techniques the author uses to argue against rhetoric. The one I personally find the most grating—beyond the ambient implication that everything is equal that I've just written about—is establishing cheap credibility by aligning himself with the camp he's arguing against. "I like X, but..." Or, in this case, "I use OCaml, but..." Then again, my pointing this out is probably ironic in the same way. Or is it?

skybrian 12y ago
It seems more unrealistic to assume everyone agrees on the same cost-benefit function. We are different people and value different things. So in any attempt at a proof involving what should be valued more, you have to state your assumptions and they're generally debatable.
- cantankerous 12y ago
  There's also the bit of refusing to agree to the same cost benefit function because it commits you to a standard that you can't back away from. I mean look at the global warming debate, for example.

ericssmith 12y ago

Sinner here. But I could only identify with four of the seven. Mostly because I couldn't make sense of his rhetoric for the other three. > I imagine that my passions are still rather thinly veiled in places You got that right. But I don't deny you your right to be as passionate about it as you like. It's a debate after all.

chrismorgan 12y ago

In my defence, on the question of header typing, I did mention that these were not things that couldn’t be done in dynamically typed languages, but rather that they were more dangerous in such languages, that it was the assurance of correctness that languages like Rust get you. A strongly typed header scheme is absolutely possible in Python, but the risks are considerably higher. I certainly agree that there were a few points that I didn’t substantiate or provide sufficient evidence for—I was deliberately intending to be broad and wanting people to think about these things, rather than going down rabbit holes. I’m afraid that half an hour really isn’t long to talk about such things in detail.

mercurial 12y ago

I take objection with the article regarding "Pretending that syntactic overhead is the issue". Or rather, I would say it's an incomplete way of looking at it. Non-statically typed languages (I'm thinking reasonably full-featured languages like Perl, Python or Ruby, not Bash) are, IMHO, go-to languages for certain tasks because they allow you to get results quickly. How? * Less typing (there is freedom in being able to cobble together a reasonably complex program in a single file of a few hundred lines in an editor, vs a number of files and thousands of lines in a IDE). * Advanced features! It is only now that closures, first-class functions, etc, start to trickle down to mainstream, statically typed languages. And they do make for shorter programs (see, eg, the post on expired links on HN). Of course, it's not to say that non-statically typed programs don't suffer from a number of drawbacks, but dismissing conciseness as something trivial does not, I think, accurately reflect reasons for why people use this kind of language.

cbd1984 12y ago

For reference, here's the difference: Strong typing ensures all results are well-defined, as the result of a specification, and it uses type information to do that. Weak typing throws away type information, so it can no longer uphold such specifications. Note that auto-conversion and error on mismatch are both evidence of strong typing in action, because both behaviors rely on type information in order to occur.