1. 31
  1.  

  2. 41

    Not for proving theories about […]

    Come now. Types establish facts and enforce useful equalities that help in writing and maintaining software. It makes the code more amenable to human comprehension and along the way it gives you mechanical assistance, which is huge. They’re also essentially “free” proofs as the only proof required is the code-that-does-the-thing-you-want-to-do. The only time this isn’t the case is if you’re using a DTPL and need to establish something not eminently obvious from a straight-forward implementation. With type inference you also don’t have to state your expectations. You can write the code that you think should work and see what type you get. In Haskell you can then flip that around, declare some types, set their implementations to undefined, and then play with the types to see if you’re headed where you want to get. Particularly useful for library integrations. Like a “bidirectional conversation” with the compiler about what’s going on.

    I, for one, embrace having become a cyborg.

    I don’t really want to get sucked into this debate, but I’ll note that I don’t often see Haskellers seeking this debate out like they used to. Myself included. It seems to mostly be users of untyped languages feeling insecure/defensive about it. You can do what you want, but don’t get upset when it instigates rebuttals. I think some of the communication difficulties here are related to how I didn’t really appreciate types until I grokked a language with nice types. Then I saw how there was no “trade-off”, all stages of a project or idea could become faster and easier, from ideation to EOL maintenance.

    I used to use Clojure and Datomic in production and let me say that the proof is not in the pudding for what Rich is saying. Datomic was a spectacularly poorly managed product. Getting irritated with unnecessarily difficult-to-debug runtime errors in a few hundred lines of Clojure is what drove me to finally learn Haskell, so I guess I should thank Rich for that.

    There’s a great thread started by Chris Done here.

    Other good replies

    1. 16

      It makes the code more amenable to human comprehension

      No, not for everyone. I find thinking in types way more constraining than thinking in values at runtime. Apparently, there are many people like me.

      and along the way it gives you mechanical assistance, which is huge.

      No, it’s not huge. There’s no conclusive study showing that type checking improves quality. It usually boils down, again, to personal preference of particular people doing the coding.

      I’m not against type checking in general (heck, Rust is one of my favorite languages, as is Python). But the outright arrogance of quite a few people considering type checking to be a clearly superior paradigm, here on Lobste.rs and elsewhere, starts getting on my nerves, sorry.

      It seems to mostly be users of untyped languages feeling insecure/defensive about it.

      That sounds like confirmation bias and doesn’t advance the discussion. Look at how every pro-dynamic typing article is upvoted (this one and one of Bob Martin’s recently) and gets shredded in the comments, with gusto.

      1. 8

        No, not for everyone. I find thinking in types way more constraining than thinking in values at runtime. Apparently, there are many people like me.

        Can you describe what you mean by that? Are you saying the runtime values do not correspond to any static type? When I write in a dynamic language, I still think about things in terms of what type they correspond to. Do you not do this?

        1. 3

          Right… Since I keep failing to write a good blog post about it, let me use this opportunity to try and articulate this here.

          Yes, runtime values do have types, but that alone is both too much and too little:

          • too much in a sense that I usually don’t care about the majority of the allowed operations on this type at a particular place in my code
          • too little in a sense that a type does not convey semantics (okay, it’s a string, but what it represents?)

          Consider an example in (hopefully) self-descriptive Python:

          def read_safe(filename):
              if os.path.exists(filename):
                  return open(filename).read()
              return 'default_value'
          

          I don’t care here if I can, say, upcase the filename, or if it’s representable as a valid utf-8, or of any other string properties. The only thing that this code actually cares about is that this value can be checked against if a certain file exists and can be opened by this name.

          Conversely, the name that I chose for this value — “filename” — already tells a programmer much more than the knowledge that it might be a string. We all know what a “filename” is. (Hickey talks about this too in that video.)

          And in fact, depending on the version of Python this value can be of many different types: an array of bytes, an array of 16- or 32 bit unicode codepoints, and in later Pythons — an instance of pathlib.Path. And this particular function doesn’t care in the slightest, it works without changes. This is why I don’t like the excitement in the Python community about type annotations: as soon as this value with is annotated with any concrete type it’s coupled with irrelevant details and becomes a maintenance burden.

          In a typed language we could invent an interface/trait/protocol for such a value. But then we will have to invent and maintain very granular definitions of such contracts for every possible use case, whereas in a dynamic language the value contract is defined by the way the value is actually used.

          1. 4

            too little in a sense that a type does not convey semantics (okay, it’s a string, but what it represents?)

            It’s pretty common in languages with good type systems that using strings for things that are more semantically rich falls away. I generally have some abstract type that can be converted to and from a string but in the business layer it remains this abstract type. So a social security number would not be a String but SSN type where its underlying representation is hidden.

            How would you communicate to users of the function what filename can be, though? Somewhere, someone has to state what the things open can validly take, right? This informalism seems convenient for you, you’re just writing a function that passes its input to another function and, hey, if they give you something that open doesn’t take, that’s not your problem, amirite? But what if you need to do any bit of manipulation of filename before opening it? For example, the _safe part means that it won’t read from /etc/ so you need to check if it starts with that. Isn’t the flexibility a hindrance now? This code suddenly balloons because it has to handle all these possible representations of a filename.

            Conversely, the name that I chose for this value — “filename” — already tells a programmer much more than the knowledge that it might be a string.

            But what if we made an abstract type called Path and the only way to construct a Path was in such a way that obeyed the operating system’s definition of what a path is?

            Maybe I’m getting side tracked though, I was trying to understand how you think about things in terms of runtime values, but it still feels to me like you think in terms of types, you’re just letting something else deal with it. But maybe I just don’t get it.

            1. 1

              How would you communicate to users of the function what filename can be, though?

              A docstring! I actually often call Python a docstring-typed language :-) The good part of this is that it’s not formal, so you can convey meaning in whatever way you feel best. This is, of course, the worst part as well because you can mislead or completely ignore the fact that your users need to know what the hell f or items mean in your argument list. So, to be clear, I’m not saying there’s an iron-clad solution to bad APIs, I’m saying that adequate means are available.

              Also, given the introspective nature of dynamic languages it’s usually fairly easy to drop down a level and just read the source code and see how those parameters are used. For example in the ipython shell it just requires adding a second ? to an object (func? would show the docstring, func?? — the source).

              if they give you something that open doesn’t take, that’s not your problem, amirite?

              Yes. I’m not sure how problematic you see it, though. It surely happens from time to time, but a single traceback is usually enough to see at which level of the stack something expected a different value.

              But what if we made an abstract type called Path and the only way to construct a Path was in such a way that obeyed the operating system’s definition of what a path is?

              That would’ve been awesome! But we didn’t. You can’t anticipate all the usage patterns and invent ideal data types for everything from the get go.

              That’s a little beside the point though (unless I misunderstand something). Assumption change, and code has to be refactored.

              I was trying to understand how you think about things in terms of runtime values, but it still feels to me like you think in terms of types, you’re just letting something else deal with it.

              The difference is that instead of specifying a concrete type as part of the function contract I’m specifying this contract in a different way that allows a user choose whatever type they happen to have around. And yes, they’re responsible for seeing if it actually works.

              The main idea of this dichotomy is not that “values don’t have types”. Of course they do. It’s just that a notion of type may not be the best (and certainly not the only) way to establish an API contract. It disallows using other un-anticipated types, and it doesn’t convey the particulars of using a value in this particular function (even if I say “this is a Path”, it fails to say that it should be openable).

              Let’s push this a little further… Values have many properties by which they can be grouped with other values. Size, memory layout, origin, security context, mutability, lifetime — you name it. A “type” is usually a combination of a few of those, but ultimately it doesn’t tell you everything about the value. Only the value itself can tell you everything about itself. “Thinking in values” as opposed to “thinking in types” is the proposition to accept this fact. And yes, the flexibility of being more expressive does have downsides. Like not being able to rely on fixed memory layout to compile into an efficient machine code.

              1. 2

                It disallows using other un-anticipated types, and it doesn’t convey the particulars of using a value in this particular function (even if I say “this is a Path”, it fails to say that it should be openable).

                I’m not really grokking this “un-anticipated types” part of your argument, though. At some point, someone has to implement how to handle string, Path and all the encodings. In the case of your example, that is whoever implemented open. So there are no un-anticipated types, we can’t pass an int in there and expect open to magically figure out what to do with it.

                And so, if someone needed to figure out what the type was at some point, then that means that, at the very least, we could infer the type of filename based on its usage in open. So I’m not really understanding what is being saved or won in the example you’re using.

                1. 1

                  In this example, what’s being saved is the need to update type annotations on arguments of read_safe that sits in the middle. While the user upstream and open downstream care about it, read_safe doesn’t have to. In a typed language, it does.

                  It’s not the only advantage though… Consider a different example:

                  def process_json(f):
                      data = json.load(f)
                      return process(data)
                  

                  Here, the only contract on f is that it should have the .read() method returning some json. It can be of any type having many more methods. And even json.load doesn’t have to care about everything else those concrete types can do, it only cares about the subset.

                  This is exactly what interfaces/traits/protocols are about with added flexibility of not having to define a new one for every particular use case.

                  So, there’s really nothing more to it than saying “don’t tell what type it is, tell me what it should do”.

                  1. 2

                    In this example, what’s being saved is the need to update type annotations on arguments of read_safe that sits in the middle.

                    But either the type inference engine can figure that out on its own, or in the case of read_safe, I could just say that filename has the same type as the input to open, that way if open changes, read_safe gets it for free.

                    Here, the only contract on f is that it should have the .read() method returning some json

                    Don’t you mean .read() method returning a string?

                    So, there’s really nothing more to it than saying “don’t tell what type it is, tell me what it should do”.

                    This is exactly what structural typing will do, which is what Ocaml’s object system is based on. It can infer the type of input based on what methods you call or you can specify the type based on what things it can do.

                    1. 1

                      Yeah, language that require type annotations can be a pain. Whole-program inference is a must-have feature, IMHO.

          2. 17

            No, not for everyone. I find thinking in types way more constraining than thinking in values at runtime. Apparently, there are many people like me.

            That’s familiarity, not a difference in how your brain works.

            No, it’s not huge. There’s no conclusive study showing that type checking improves quality. It usually boils down, again, to personal preference of particular people doing the coding.

            We don’t have sound experimental protocols for this. Reading tea leaves on GitHub is not science.

            I’m not against type checking in general (heck, Rust is one of my favorite languages, as is Python). But the outright arrogance of quite a few people considering type checking to be a clearly superior paradigm, here on Lobste.rs and elsewhere, starts getting on my nerves, sorry.

            I don’t care what you believe or use. If nobody lies about the tools or practices then I won’t have to rebut anything.

            That sounds like confirmation bias and doesn’t advance the discussion. Look at how every pro-dynamic typing article is upvoted (this one and one of Bob Martin’s recently) and gets shredded in the comments, with gusto.

            Bob Martin’s post was even more ignorant than this talk, it deserved to get shredded if only for making preferential users of dynamic typing look dumb.

            Reiterating what I said in my first post, I don’t reaaaallyyyyy want to debate this because people tend to get upset and I don’t think arguing with programmers is a good use of my time or this space. You’re going to believe what you believe until you get shocked out of it. That’s just how this thing tends to go, nobody’s actually open-minded in these threads. So why not spare ourselves the grief and get back to work?

            1. 5

              It’s got nothing to do with familiarity. Types force you to express yourself in a way that can be verified statically by the type checker. A set of provable statements is necessarily a subset of all valid statements. Static typing restricts how you can express yourself, and that’s the biggest drawback of this approach.

              At the end of the day, a human has to be able to read the code and understand its intent. Anything that distracts from that is a net negative in my experience. For example, you could write a 300 line sort in Idris https://github.com/davidfstr/idris-insertion-sort/blob/master/InsertionSort.idr that verifies all kinds of things statically. Understanding that it’s semantically correct is much harder than it would be for a 5 line version without types.

              1. 12

                A set of provable statements is necessarily a subset of all valid statements.

                You don’t typically run into incompleteness when you’re only using lightweight types like with run-of-the-mill Haskell. If your program is ill-typed in Haskell, the overwhelmingly likely scenario is that your program is just wrong or unsafe, not that it’s correct but can’t be typed.

                1. 3

                  That depends what you’re doing and what you consider “Hakell”. It’s not too hard to run into a need for RankNTypes in some cases (though you can usually write the code in a different way to avoid that need).

                  1. 0

                    Sure, but at that point you’ve already accepted that there is value in avoiding formalism. At that point it’s just a matter of degrees of comfort. My view is that code should be written for human readability first and foremost, because only a human reader can decide whether it’s semantically correct or not.

                    1. 10

                      There’s a minimum amount of formalism, but there isn’t a maximum amount of formalism. It’s necessarily a matter of degree. The argument is that most people pick way too low.

                      I find Haskell code more readable than the vast majority of languages, at a given level of program complexity. You seem to be assuming that Haskell is hard to read, which I don’t think is a reasonable assumption at all.

                      1. 1

                        I find a lot of people also conflate typing with type signatures. What makes Haskell great is you can get many of the type system benefits without ever writing a type signature at all!

                      2. 8

                        Sure, but at that point you’ve already accepted that there is value in avoiding formalism.

                        There is value in not being tied to a specific formalism. But there is little value in avoiding all formalisms altogether, unless you count the possibility of being wrong as “value”.

                        only a human reader can decide whether it’s semantically correct or not.

                        Only if the human reader can reliably prove things about programs.

                        1. 2

                          This is something that static typing proponents have to demonstrate empirically. So far there’s no compelling evidence to suggest that projects are delivered faster with statically typed languages, have less defects, or improved ease of maintenance. Considering how long both type disciplines have been around, that’s quite the elephant in the room. I’ve heard the sentiment that it’s just too hard to test for this, but that just rings hollow to me. If something is clearly more effective that would be possible to demonstrate.

                          It’s a false dichotomy to claim that you either use static typing or nothing at all. The reality is the formalism of using the type system is only one approach, and other approaches appear to be equally as effective in practice. You have testing, static analsysis tools like Erlang dialyzer http://erlang.org/doc/man/dialyzer.html runtime specification tools like Clojure Spec https://clojure.org/about/spec

                            1. 2

                              This is something that static typing proponents have to demonstrate empirically.

                              No—You have to be more careful about how you’ve selected the “burden of proof”.

                              You’ve placed it on requiring proof that static types provide X benefit.

                              One can just as well turn this around and require poof that eschewing static types provide X benefit.

                              We cannot a-priori place such demands in either direction.

                              Finally, Requiring statistically significant studies pretty much guarantees no provable claims can be made for any side; since that amounts to a social science laden with shaky assumptions and ambiguous modeling. ‘reading the tea leaves on github is not science’

                              (~crossposted from hn thread)

                              1. 2

                                Requiring statistically significant studies pretty much guarantees no provable claims can be made for any side; since that amounts to a social science laden with shaky assumptions and ambiguous modeling.

                                It’s not a guarantee. We have the techniques and skill required to do a rigorous study, it’s just that such a study is really expensive and nobody wants to invest the money. “It’s hard” is not a reason to give up on something.

                                1. 3

                                  Very well; I eagerly await the studies then.

                                  In the meantime, then, be skeptical about claims that attempt to discredit practices such as static typing due to an undue burden of proof requirement.

                                  1. 2

                                    Sure. But also be skeptical about claims that types reduce bugs. Everybody’s arguing from anecdata and everybody’s both biased and fallible.

                                2. 1

                                  You’ve placed it on requiring proof that static types provide X benefit.

                                  That’s actually a correct burden of proof. We usually put it on the person claiming something brings benefits or should be a standard practice. So, if static typing has benefits, it’s up to us who believe that to demonstrate that using logical arguments and/or evidence in the field. There’s people in the discussion doing that. So, we don’t have to worry about burden of proof since we’re doing our part. ;)

                                  1. 1

                                    Claiming the same point more strongly doesn’t provide new information or absolve you from the contradiction I’ve identified

                                    1. 3

                                      Yogthos correctly noted that the burden of proof is on anyone challenging the status quo. The status quo is that there’s no consensus in this forum or in programming community at large whether static typing improves software over dynamic with their style of quality assurance. Yogthos wanted anyone pushing static types as the new, status quo that we should all adopt for the claimed benefits to provide evidence of those benefits. This is the standard method of discussion. When you countered that, I reminded you of that and that’s all my comment was about.

                                      Now you’re talking about a contradiction I have to absolve. Whatever it is will be a separate point to discuss. Burden of proof remains on anyone advocating adoption of a method with claimed benefits. They prove it. Then people should check it. Otherwise, we’d have to accept an Internet’s worth of false claims wasting time proving each one wrong. That would be a waste of time. Hence, the established direction for burden of proof.

                                3. 2

                                  This is something that static typing proponents have to demonstrate empirically. So far there’s no compelling evidence to suggest that projects are delivered faster with statically typed languages, have less defects, or improved ease of maintenance.

                                  As I said elsewhere in the discussion, I’m not advocating static type systems in this discussion. Formalisms other than types do exist! However, if you want your programs to be free of defects, you have to prove them correct. Types sometimes make a very small contribution towards that goal. Tests don’t help one iota.

                                  1. 0

                                    I disagree with that. If you want your programs to be correct, you have to ensure they work as specified for the use cases you have. You can try to do that using static types, or you can use test,s or a runtime contract. All these approaches are effective in practice.

                                    1. 2

                                      If you want your programs to be correct, you have to ensure they work as specified for the use cases you have.

                                      No disagreement here. However, the claim that a program works as specified requires proof.

                                      You can try to do that using static types, or you can use tests or a runtime contract.

                                      Most type systems only allow you to prove very trivial things about your programs. Tests are only a feasible strategy if the space of legitimate inputs is small enough to be exhaustively searched. “Runtime contracts” are a misnomer, but assuming you meant “runtime contract checks”, well, those don’t prove your program correct.

                                      1. 1

                                        Proof is a formal term and typically implies correctness for all possible cases. A program has to only demonstrate correctness for possible inputs.

                                        Ultimately, your program has to have some sort of specification. My experience is that these specifications will not be formal in practice. You have to code your program to whatever requirements you have as best understood.

                                        A runtime contract like Clojure Spec https://clojure.org/about/spec will allow you to encode a specification and do generative testing against it. This is a sufficient level of proof that the software works as expected for vast majority of situations.

                                        1. 3

                                          Proof is a formal term and typically implies correctness for all possible cases. A program has to only demonstrate correctness for possible inputs.

                                          What distinction are you making between “all possible cases” and “all possible inputs”?

                                          Ultimately, your program has to have some sort of specification. My experience is that these specifications will not be formal in practice. You have to code your program to whatever requirements you have as best understood.

                                          Of course, you can’t expect a business analyst or what-have-you to hand you a formal specification. You have to generate it yourself from the information you have been given.

                                          A runtime contract like Clojure Spec https://clojure.org/about/spec will allow you to encode a specification

                                          This would actually be a formal specification, assuming you have a formal semantics for Clojure! The proof that your program meets the specification is still missing, though.

                                          and do generative testing against it.

                                          Generative testing is a little bit smarter than unit testing, but it’s no replacement for a proof.

                                          1. 2

                                            Generative testing is a little bit smarter than unit testing, but it’s no replacement for a proof.

                                            It’s worth noting that the first property-based testing library was QuickCheck for Haskell, so proof is no replacement for generative testing, either :P

                                            1. 1

                                              It’s worth noting that the first property-based testing library was QuickCheck for Haskell, so proof is no replacement for generative testing, either.

                                              Let’s set aside for a while the matter of whether your conclusion is true or false. I fail to see how exactly your premise entails your conclusion. Are you implicitly assuming that Haskell’s type system can verify every property you could possibly care about, and even then it still wasn’t enough?

                                              1. 2

                                                I’m saying that enough Haskell people felt that their particular type system wasn’t enough such that they created (an incredibly innovative!) testing library. Defense in depth, yo.

                                                1. 1

                                                  Almost every other comment I said in this thread explicitly says (paraphrased) “types do little for you” and “you have to prove yourself that your programs are correct”.

                                                  1. 3

                                                    I think there’s a miscommunication happening here. I love formal methods to the point I spent months writing a manual on TLA+. I just don’t think it’s enough. It’s not enough to prove your program is correct: you have to obsessively test it too.

                                                    1. 4

                                                      I think your original statement felt a bit out of place since I don’t know any Haskeller that thinks their type system is powerful enough to generate a proof of the correctness of the program.

                                            2. 1

                                              Let’s say I have inputs a and b, and a result c. If I know my input range is from 0-100, I can test that a^n + b^n = c^n for all possible inputs. However, it’s much more difficult to prove this to be the case for any input in general.

                                              This would actually be a formal specification, assuming you have a formal semantics for Clojure! The proof that your program meets the specification is still missing, though.

                                              I would argue that it’s not required. If I have a specification, I can do generative testing to exercise the code, and I can validate that the data coming into the system is within the accepted range.

                                              My argument is that the effort required to provide an exhaustive proof is not justified in vast majority of situations. The business requirement is typically to produce software that works well enough that the users are happy. A proof is not a business requirement.

                                    2. 2

                                      This is something that static typing proponents have to demonstrate empirically.

                                      What is? I don’t see that @pyon made any contentious claims in that comment.

                                      1. 0

                                        The claim that static typing is the most effective formalism. This is a false dichotomy:

                                        There is value in not being tied to a specific formalism. But there is little value in avoiding all formalisms altogether, unless you count the possibility of being wrong as “value”.

                                        1. 1

                                          What I actually claimed is that types help very little. How exactly does that agree with “types are the most effective formalism”?

                                          1. 1

                                            Appears I misread your comment. That said, I do think there is value in possibility of being wrong, if that means you can express yourself in a less constrained fashion. Ultimately, your formal specification can be wrong as well, so it’s really a question of where you’re going to be looking for errors.

                                            1. 2

                                              Appears I misread your comment.

                                              I didn’t even bring types into the discussion until you did.

                                              That said, I do think there is value in possibility of being wrong, if that means you can express yourself in a less constrained fashion.

                                              The only freedom that you get is the freedom to say nonsense. That’s not terribly useful.

                                              Ultimately, your formal specification can be wrong as well

                                              So you test it, more or less the same way scientists test scientific theories:

                                              • Make predictions (i.e., logical inferences from the specification) about what the user meant in distinct cases.
                                              • Ask the user if these predictions agree with what they expected.
                                              1. 1

                                                The only freedom that you get is the freedom to say nonsense. That’s not terribly useful.

                                                That’s absurd. You can state many things without being able to prove them. As long as you can demonstrate that the statement works within the context you’re using it, you get value out of it.

                                                So you test it, more or less the same way scientists test scientific theories:

                                                Which is exactly what you’d do with tests or runtime specifications.

                                                Ultimately, we’re discussing cost benefit here. My claim is that you can deliver working software faster without using formal proofs. That’s what the business cares about at the end of the day. A company that delivers a working product that people use will outcompete the company working on a perfect product.

                                                1. 1

                                                  As long as you can demonstrate that the statement holds (FTFY) within the context you’re using it, you get value out of it.

                                                  You’re just adding one more premise (the “context” you talk about) to the implication you have to prove.

                                                  1. 1

                                                    While we don’t have a proof, we certainly have a lot of evidence accumulated over the years. If formal proofs were indeed a requirement for developing usable software, then we’d all be using them by now. It’s really that simple.

                                                    Businesses using languages like Haskell and OCaml would outcompete those using Python, Ruby, or JavaScript. This is not what we see happening in practice though. Despite these languages having been around for many decades, they remain niche.

                                                    Now, it’s perfectly possible that once somebody is trained up sufficiently they could be just as productive. However, that seems to be a challenge as well.

                                                    At the end of the day we need languages that can be learned relatively easily by an average developer to become productive with. The more formal the language the less accessible it becomes. So economics aren’t in favor of formal methods I’m afraid.

                                                    1. 2

                                                      If formal proofs were indeed a requirement for developing usable software, then we’d all be using them by now.

                                                      Sure, one can trivially argue they are not a requirement but we lack any reasonable amount of scientific study on if they help. I think they probably do (more understanding of / reasoning about code seems likely to help quality) but what I think is hardly science ;)

                                                      1. 1

                                                        Businesses using languages like Haskell and OCaml would outcompete those using Python, Ruby, or JavaScript.

                                                        I don’t see how you arrive to that conclusion. Neither Haskell nor OCaml is in short supply of features that make formal verification harder than necessary.

                                                        At the end of the day we need languages that can be learned relatively easily by an average developer to become productive with.

                                                        Maybe the notion of “average developer” is the problem in the first place?

                                                        1. 1

                                                          You still haven’t explained what sort of formal verification you advocate, or given an example of a language using it. Haskell and OCaml are the most popular formal languages I’m aware of. Are you talking about languages like Coq here?

                                                          From a business perspective, you need a tool that can be learned in a reasonable amount of time by a person you’re going to be able to hire from the pool of people available. That’s where your average developer comes from. Technology that can be used by a wider pool of people effectively will always dominate.

                                                          1. 1

                                                            Are you talking about languages like Coq here?

                                                            No. Plain paper and pen proofs.

                                4. 11

                                  For example, you could write a 300 line sort in Idris https://github.com/davidfstr/idris-insertion-sort/blob/master/InsertionSort.idr that verifies all kinds of things statically. Understanding that it’s semantically correct is much harder than it would be for a 5 line version without types.

                                  https://research.googleblog.com/2006/06/extra-extra-read-all-about-it-nearly.html

                                  1. 3

                                    Sure, and these are exactly the types of bugs you will see in the real world in dynamically typed languages. I’ll let you decide if that bug was a show stopper or not for production use. Also from the link:

                                    And now we know the binary search is bug-free, right? Well, we strongly suspect so, but we don’t know. It is not sufficient merely to prove a program correct; you have to test it too.

                                    1. 2

                                      But would the Idris proof actually have caught the bug? It’s an overflow error, while Haskells have infinite-precision numbers. Seems like sidestepping the problem to me.

                                      1. 7

                                        The actual error is conflating (physical or virtual) machine integers with the integers. It is totally fine to use machine integers for performance reasons, but it is not okay to pretend that results that were proven for the integers must also hold for machine integers.

                                    2. 7

                                      The Idris example is interesting but doesn’t say too much. There is lots of complicated ways things can be solved with or without types. I don’t know if the link you pasted is considered a good solution or not.

                                      That being said, one thing that the Idris solution will give you but a dynamically typed solution won’t without extensive tests is if I modify the code in such a way that it violates the invariants, the compiler will complain. This is a major benefit of a good type system, IME.

                                      1. 3

                                        However, you have to know that the invariants themselves are correct. A type specification is effectively a program that the type checker uses to analyze your original program. If a specification is as complex as the Idris example, it becomes difficult to tell whether it’s correct in any meaningful sense. So, now you just pushed the problem back, you just have a metaprogram that you have to reason about.

                                        1. 8

                                          The thing you are missing:

                                          In typed languages you often have to be wrong twice to introduce a bug: You have to get both the code and the types wrong. Getting only one of them wrong will be flagged and rejected by the compiler.

                                          In untyped languages you usually have to be right twice to avoid a bug: Yo have to get both the code and the tests right. Getting only one of them wrong is no reliable guarantee that your bug will be found before deployment.

                                          1. 2

                                            In typed languages you often have to be wrong twice to introduce a bug

                                            Yes, and moreover, both wrong in a compatible way!

                                            1. 1

                                              I’m not missing that at all. My point is that the formalism often requires you to express yourself in a specific way that can be verify. So, while you know something is self-consistent, you don’t know that it’s correct in a semantic sense.

                                              Dynamic languages let you write much more direct code that’s easier for a human to read. Meanwhile, you can also provide specifications in a dynamic language. Take a look at Racket Contracts or Clojure Spec as examples https://clojure.org/about/spec In fact, I’d argue this provides a more rich specification than types as it focuses on semantic correctness.

                                              1. 8

                                                Dynamic languages let you write much more direct code that’s easier for a human to read.

                                                No more than any other paradigm, though, right? I don’t find Ocaml code any less readable than Python code. In most cases, the types aren’t even explicitly written in Ocaml so there is line noise or anything getting in the way.

                                                I’ve actually been writing code in Python a bunch lately after spending a lot of time in Ocaml and I’ve noticed that I end up having to look at documentation fairly frequently, whereas in Ocaml I would generally just look at the type of a value instead. But the documentation is really hit or miss, so I’ve even found myself looking at the code for dependencies several times, I’ve only done that a few times in Ocaml.

                                                YMMV, but your blanket claim that dynamic languages let one write code easier to read than statically typed languages doesn’t match my experience.

                                                On top of that, ease of reading isn’t the metric I personally go by. It’s ease of refactoring. I’ve found that dynamic languages take a lot of effort to make refactoring safe, but in a language like Ocaml I have the compiler watching over my shoulder.

                                                1. 1

                                                  We clearly have very different experience here. I do find that Clojure code ends up being more direct than any static language I’ve used. I also find that it allows me to trivially express patterns that are challenging to encode using type systems. For example, something like Ring middleware https://github.com/ring-clojure/ring/wiki/Middleware-Patterns is difficult to do in a static context.

                                                  I do find readability is incredibly important when refactoring. I need to know what the code is doing and why to refactor it effectively.

                                                  1. 3

                                                    You can accomplish that pattern in a statically typed language. Ocaml has a few implementations of that, one is hmap: http://erratique.ch/software/hmap

                                                    The only thing that isn’t exactly what I think you want is your key encodes the type of the value so you have to know the type you want to get out of a particular key.

                                                    I do find readability is incredibly important when refactoring. I need to know what the code is doing and why to refactor it effectively.

                                                    But how does that square with your response to @pyon in another subthread:

                                                    With a dynamic language it’s sufficient to show that the program behaves as expected for the specific use cases that you have

                                                    How do you express how the program should behave for the cases you have? Is it tests? What happens if your break the code for a valid case but that you didn’t write a test for? The problem I find when refactoring code in a dynamically typed language generally revolves around how hard it is to know what the code should do and if I change the code in a certain way (for example, make something that was an integer now a string), have I broken something users of the codebase depend on. That sort of refactoring is trivial in a statically typed language, just make the change and let the compiler tell you every other place that needs to change. IME, those changes are very difficult in a dynamically typed language.

                                                2. 4

                                                  I’m not missing that at all. My point is that the formalism often requires you to express yourself in a specific way that can be verify.

                                                  That’s a bit like arguing that seat belts are bad, because they make it hard to drive while standing upright in your seat. Doh!

                                                  The point is that there are hundred of thousands of people still walking on this planet that wouldn’t be around without seat belts.

                                                  Dynamic languages let you write much more direct code that’s easier for a human to read.

                                                  Let’s just disagree on that.

                                                  Take a look at Racket Contracts or Clojure Spec as examples https://clojure.org/about/spec.

                                                  The whole problem with these things is that they are optional. You can decide to use them in your own code, but if libraries are not using them you are in an uphill battle.

                                                  We have seen this problem times and times again with newer languages trying to graft on nullability information on existing libraries and spectacularly failing, despite the much smaller scope of the issue.

                                                  The main benefit of types is that they force everyone to follow their rules.

                                                  I can look at a random library’s type signatures and immediately know which things cannot happen.

                                                  1. 3

                                                    If you use Design-by-Contract, you can do both. The Design-by-Contract preconditions, invariants, and postconditions are similar to static types where you’re bolting them on rather than being integrated in the language. Some languages, esp Eiffel and Ada/SPARK, integrate them. I doubt Python etc support it so you’d be using some language feature, maybe just the OOP stuff, to do it. The precondition checks especially would guarantee certain things about your program before you even run it with people using your library knowing more about it just looking at them. Invariant or postcondition checks can be combined with property-based or purely-random testing to catch a lot of errors in a way that highlights exactly what failed.

                                                    Now, people can get these properties wrong. However, the literature of academic and industrial deployments strongly argue that they’ll catch vastly more implementation errors in development and maintenance phases than review or testing alone.

                                                3. 7

                                                  However, you have to know that the invariants themselves are correct.

                                                  And in a dynamic language we don’t even know what any of the invariants are, so I don’t see this response as damning of types. In Ocaml, the sort function for lists has the type: cmp:('a -> 'a -> int) -> 'a list -> 'a list which is pretty lightweight, it’s not nearly as formal as the Idris one but it still tells me important things, like that the sort implementation cannot know anything about the contained type.

                                                  Essentially it feels like you’re saying there exists no invariants worth checking at compile time. Is this an accurate summary of your stance?

                                                  1. 5

                                                    However, you have to know that the invariants themselves are correct.

                                                    So long as an understandable logic, the experience of several decades in formal specification show people find errors in requirements, design, or implementation using them. Every case study has errors caught this way with most in industry who were just using their heads and tests before reporting a drop in defects after introducing formal specs. The specs themselves are about the what more than the how which focuses the mind for review or tooling for checks. The how is usually more complex with Idris especially being a heavyweight way to do things not representative of effort/reward ratio of typical usage of either static typing or formal specs.

                                                    Now, some of these specs can get pretty big. This varies from being limitations of the spec language to intrinsic complexity of the problem. The former is something they might also screw up on. The compiler might catch some but not all of those screwups. The latter represent the complex details the programmer must get right that are implicit in non-typed or non-specified programs. As in, such complexity is always there but just invisible to compilers, checkers, and maybe the programmer depending on skill. Then, making it explicit, it can be checked by any of those. The more you want to explicitly check, the more types/specs come with the given module. Again, there’s a spectrum of effort put in vs rewards gotten out that one can use depending on importance of module and their resource constraints.

                                                    1. 1

                                                      Agree completely.

                                                4. 5

                                                  In real life, programmers do not deliberately write unreadable code in either static or dynamic type systems, because that would be pointless. It is also possible to write dynamically-typed code that is unreadably dynamic if you aren’t immersed in the local idioms (I can point to a lot of mainstream Ruby examples!). So I’m not sure what point you’re trying to make. [edited due to premature post!]

                                                  1. 0

                                                    I completely agree that you can make a mess in any language. However, my point was that static typing necessarily restricts the number ways you can write code to those that are statically provable. A dynamic language allows you to write a statement that is not accompanied by an exhaustive proof, and proving something is often much more difficult than stating it.

                                                    For example, Fermat’s Last Theorem states that no three positive integers a, b, and c satisfy the equation a^n + b^n = c^n for any integer value of n greater than 2. That’s a really simple statement to make, and to understand. Proving that to be correct is a lot more difficult. Even when such a proof has been found, only a handful of people in the world can judge whether its correct or not.

                                                    1. 14

                                                      A dynamic language allows you to write a statement that is not accompanied by an exhaustive proof,

                                                      Yes, but that is overly categorical.

                                                      Most typed languages also do not require exhaustive proofs, in the form of the Idris example you posted. You seem to want to create a false dichotomy, between no types on one had, and a total formally verified technique on the other (which are cumbersome).

                                                      Most proponents of static typing here aren’t advocating for full dependent-typed/verified languages (most of which are still experimental!) capable of solving Fermat’s Last Theorem in the compiler.

                                                      1. 1

                                                        Idris example is an extreme case, but pretty much any statically typed languages make it difficult to work with heterogeneous data. Types are also make it difficult to pass data across boundaries. This is the same problem you have with OO class hierarchies.

                                                        1. 4

                                                          Is heterogeneous data something you find yourself commonly working with? Even in a language like Python it’s generally considered good practice that all entries in your containers have the same type unless there is some way to know before hand what they will be. But GADTs make that work in a statically typed language just fine.

                                                          1. 2

                                                            Yes absolutely. Most real world data tends to be heterogeneous in my experience. This is a perfect example https://github.com/ring-clojure/ring/wiki/Middleware-Patterns You can have middleware functions that update the request and response maps by adding keys relevant to that piece of middleware, or updating existing keys. This would be pretty much impossible to do using a static language, especially if you want to be able to write middleware libraries that aren’t aware of one another.

                                                            1. 3

                                                              Linking to my response about HMap here: https://lobste.rs/s/n6eix9/rich_hickey_delivers_rationale_for#c_keqhja

                                                              tl;dr - it isn’t pretty much impossible.

                                                              Most real world data tends to be heterogeneous in my experience.

                                                              I guess you mean heterogeneous and not known a-priori? For heterogeneous data we have things like records which let you store different kinds of data in the same thing, but you know what it is before hand.

                                                      2. 3

                                                        If you have to bring up Fermat’s Last Theorem that suggests your argument is on shaky ground.

                                                        1. 1

                                                          Please do elaborate.

                                                          1. 3

                                                            It’s a very hefty sledgehammer of an argument and it suggests that some subtledties may be escaping you.

                                                    2. 4

                                                      Static typing restricts how you can express yourself, and that’s the biggest drawback of this approach.

                                                      Do you have an example of a program that cannot be statically typed and still represents a program you would want to write?

                                                      1. 5

                                                        Clojure transducers https://clojure.org/reference/transducers are difficult to type for a general case since the result depends on the runtime type of the argument. These are a core mechanic in Clojure. Ring middleware https://github.com/ring-clojure/ring/wiki/Middleware-Patterns is another example of something that’s not really possible in a typed language.

                                                        1. 2

                                                          Thanks! I don’t know enough about either to comment more.

                                                          1. 1

                                                            Ring middleware is another example of something that’s not really possible in a typed language.

                                                            Unless I’m very much mistaken “ring middle way” is easily expressible in a typed language with polymorphic row types.

                                                            1. 1

                                                              Ring middleware functions can modify the map in any way. They can add keys, remove keys. or change types of existing keys. The functions are defined in separate libraries that aren’t aware of one another directly. I can add a dependency and chain the middleware libraries any way I see fit. How would you express this using row types?

                                                              1. 1

                                                                They can add keys, remove keys. or change types of existing keys. … How would you express this using row types?

                                                                That’s exactly the functionality that polymorphic row types give you.

                                                                Concretely, in some imaginary type system

                                                                -- Consumes any row type
                                                                addAKey :: { r } -> { newKey :: Foo, r }
                                                                
                                                                -- Consumes any row type with `oldKey` field
                                                                removeAKey :: { oldKey :: Foo, r } -> r
                                                                
                                                                -- Consumes any row type with `key` field
                                                                changeTypeOfAKey :: { key :: Foo, r } -> { key :: Bar, r }
                                                                
                                                                1. 1

                                                                  This is something you’d have to do on case by case basis though?

                                                                  1. 1

                                                                    I don’t understand what you mean.

                                                                    1. 1

                                                                      Linking to HMap comment, I think it does what the @Yogthos is referring to:

                                                                      https://lobste.rs/s/n6eix9/rich_hickey_delivers_rationale_for#c_keqhja

                                                        2. 2

                                                          A set of provable statements is necessarily a subset of all valid statements.

                                                          That runs counter to Gödel’s completeness theorem: a statement in a first-order theory is provable iff it’s true in all models. In programming language terms: a statement about a program is provable iff it holds in all conforming implementations of the language the program is written in.

                                                          Now, you might only care about one language implementation (presumably the one you’re using), but some of us care about portability and freedom from irrelevant implementation details…

                                                          1. 0

                                                            This is actually a direct result of Godel’s incompleteness theorem. It’s also known as the halting problem in CS. For example, Scala compiler has a bug where it stack overflows trying to resolve types https://github.com/scala/bug/issues/9142

                                                            You’re restricted to a set of statements that can be verified in a reasonable amount of time.

                                                            1. 3

                                                              Gödel’s first incompleteness theorem asserts every effectively axiomatized formal system sufficiently powerful to prove basic arithmetic facts contains statements that are neither provable nor disprovable. It says nothing about the “validity” of such statements, because GFIT is a theorem in proof theory, not model theory. In particular, by Gödel’s completness theorem, the Gödel statement, just like any other statement that is neither provable nor disprovable in a theory, is true in some models and false in others. Whether that is “valid” enough for you is up to you - I prefer to work with statements (programs) that are true (run correctly) in all models (conforming implementations) of a theory (programming language).

                                                              Also note that I’m not advocating types (in this discussion). But you have to prove your programs correct, whether you use types or something else altogether. “Using types is an inefficient way to prove most things I have to prove” is a legitimate objection - one that I agree with, even! “I want to get away with not proving what I have to prove” is not.

                                                              1. 1

                                                                No, you don’t have to prove your programs correct. That’s the key difference. With a dynamic language it’s sufficient to show that the program behaves as expected for the specific use cases that you have. With a static language you have to write it in a way that the type checker is able to prove to be exhaustively correct.

                                                                1. 4

                                                                  With a dynamic language it’s sufficient to show that the program behaves as expected for the specific use cases that you have.

                                                                  So you can exhaustively test the entire space of legitimate inputs? You must have a few dozens orders of magnitude more computing power available to you than I do.

                                                                  With a static language you have to write it in a way that the type checker is able to prove to be exhaustively correct.

                                                                  That’s not true. As a matter of fact, I don’t do that when I use statically typed languages. Types provide basic sanity checks (e.g., modules don’t peek into each other’s internal details), but the bulk of the program’s proof of correctness is written by me, using paper and pen.

                                                                  1. 0

                                                                    Of course I wouldn’t. I’d validate data at the edges using Spec https://clojure.org/guides/spec Types are not the only way to provide basic sanity checks.

                                                                    1. 5

                                                                      Judging from your replies, you seem to think I’m delusional about types, even though I have been very explicit about the limited extent to which types help me. I expected it to be patently clear from my previous statements that I’m not telling you to use types. You can, of course, use whatever you wish. What I’ve actually said is:

                                                                      • You have to prove your programs correct.
                                                                      • To prove your programs correct, you need to use some formal system.
                                                                      • Gödel’s incompleteness theorems isn’t an excuse for not proving your programs correct.
                                                                      • Types sometimes relieve you from a very tiny part of the effort of proving your program correct.
                                                                      • There exist formal systems other than types.

                                                                      Furthermore, I originally only intended to make the first two points.

                                                                      1. 0

                                                                        I disagree with the idea that you have to prove your programs correct in a general case. That can be desirable in some situations, but it’s simply not a business requirement.

                                                                        The result of Godel’s incompleteness theorems is that the type checker restricts the way you’re able to express yourself to a subset of expressions that can be proved in a reasonable amount of time by the type checker. My argument is that it can result in code that’s harder for a human to understand than code that can’t be machine verified.

                                                                        I think we agree on the value of types, but not on the value of formal proofs.

                                                                        1. 2

                                                                          The result of Godel’s incompleteness theorems is that the type checker restricts the way you’re able to express yourself to a subset of expressions that can be proved in a reasonable amount of time by the type checker.

                                                                          You keep bringing in type checkers. Didn’t you get the memo when I said “Formalisms other than types do exist!”?

                                                                          My argument is that it can result in code that’s harder for a human to understand than code that can’t be machine verified.

                                                                          My experience is exactly the opposite. Types don’t write much of your proof of correctness for you, but they make the parts you have to write yourself much easier to write.

                                                                          1. 0

                                                                            It certainly does sound like our experiences are very divergent here. You keep talking about other formalisms, but the point I make regarding the type checker apply to those just the same. Perhaps, you can elaborate on how you believe these other formalisms avoid the problem.

                                                                            1. 5

                                                                              Humans and computers have different strenghts:

                                                                              • Computers are faster and more reliable than humans at performing long calculations, especially case analyses.

                                                                              • Humans are better than computers at defining usable abstractions and jumping between them, which requires insight.

                                                                              Formal systems come in varying degrees of human- and computer-friendliness. At the two extremes, we have:

                                                                              • Cellular automata usually have simple and efficiently implementable definitions (computer-friendly). However, their evolution over time is very difficult to analyze and predict (human-hostile).

                                                                              • Higher-order programming languages (i.e., whose variables can be instantiated with abstractions) allow complex hierarchical structures to be directly expressed in them (human-friendly), but the fundamental operation in their semantics, namely variable substitution, is difficult to implement both correctly and efficiently (computer-hostile).

                                                                              Notably, the first-order predicate calculus lies at a sweet spot in the middle. It is simple enough to be used by humans directly, not just to define things, but also to perform actual computations (although this requires training). At the same time it is a powerful enough metalanguage for higher-order object languages (e.g., set theory).

                                                                              In my view (others might not agree), the key to making verification more tractable is to intelligently split the verification effort into parts that are relatively easy for a human to perform (defining hierarchical structures and abstraction boundaries, finding loop invariants and variants) and parts that are relatively easy for a computer to perform (performing mechanical consistency checks, exhaustive searches and case analyses). Different parts might have to be performed using different formal systems, designed to exploit the strengths of whoever has to use it directly.

                                                                  2. 3

                                                                    With a static language you have to write it in a way that the type checker is able to prove to be exhaustively correct.

                                                                    Here’s a well-typed program

                                                                    add3 x y z = x + y + z
                                                                    

                                                                    In what way have I (or the type checker) “proven it to be exhaustively correct”?

                                                                    1. 1

                                                                      It’s not well typed if x, y, and z are int32s.

                                                                      1. 2

                                                                        It is well typed. The operation just happens to be addition in Z/kZ for k = 2^32, instead of the usual integer addition.

                                                                        1. 1

                                                                          So it’s well-typed but potentially has a lot of behavioral bugs, because you can’t guarantee that x + y >= x.

                                                                          1. 3

                                                                            Z/kZ isn’t an ordered ring, hence you shouldn’t define an operation <= that works on int32 arguments.

                                                                      2. 0

                                                                        You’ve created some very basic constraints here such as x, y, and z having to support the + operation. This example is not very interesting for obvious reasons. :)

                                                                        1. 4

                                                                          The rest of strongly typed programming is very much of this flavour and indeed rules out (merely?) “not very interesting” bugs.

                                                        3. 2

                                                          Have some thoughts on this, but first of all:

                                                          I don’t really want to get sucked into this debate … users of untyped languages feeling insecure/defensive about it.

                                                          That’s very rude of you.

                                                          Okay, on to the meat of this. I think everybody has the same misconception about dynamic typing, including a lot of people who use dynamic typing: dynamic typing and static typing are not exclusive. All static typing means is that types exist at compile time. All dynamic typing means is that types exist at runtime. Languages can be both statically typed and dynamically typed (C#). Languages can be neither (bash). Each one has benefits and drawbacks, and it happens that each one’s drawbacks cancel out the other’s benefits, which is why a lot of languages are only one or the other. But since most dynamic languages aren’t also static (because drawbacks), people conflate it with untyped and end up arguing “static vs untyped”. It doesn’t help that a lot of languages don’t really explore the power dynamic typing gives you, precisely because they choose it to avoid the overhead of static typing.

                                                          Here are some dynamic language features that would be a lot to implement in non-dynamic languages:

                                                          • J’s array manipulations have very different type signatures depending on the dimensions of your arguments and the specified rank of the verb. That allows it to do extremely fast manipulations in extremely concise syntax: see here for examples.
                                                          • The two most popular data analysis languages, Python and R, both allow for interactive, partially executable REPLs. That makes them good for exploring data before committing to a transformation or full script.
                                                          • Python also uses prototype inheritance, letting you adjust all instances of an object at runtime (for example, to add logging or caching).
                                                          • Ruby has runtime metaprogramming, which is key for how the ActiveRecord ORM works.
                                                          • I get the impression SQL would be a lot trickier to statically type but that’s just a hunch.

                                                          Now, I’m not saying these are good or bad. In some contexts, these are good features to have. In other contexts, they’re less useful than static typechecking. But there is a tradeoff that happens and there’s never a free lunch.

                                                          1. 3

                                                            dynamic typing and static typing are not exclusive

                                                            Right, and that’s true in Haskell too. The former should be preferentially minimized.

                                                            All dynamic typing means is that types exist at runtime.

                                                            Those aren’t types, they are tags, sometimes called class tags. Types have no representation.

                                                            I get the impression SQL would be a lot trickier to statically type but that’s just a hunch.

                                                            I maintain a type-safe SQL DSL library for Haskell and it has single-handedly improved my work more than learning or using Clojure ever did.

                                                            Python also uses prototype inheritance, letting you adjust all instances of an object at runtime (for example, to add logging or caching).

                                                            I have never ever needed this and anytime I’ve run into someone that did it’s because the tooling was failing them in other places. There are far more robust and maintainable ways to solve the same problems.

                                                            I was primarily and preferentially a user of untyped programming languages until I finally got to grips with Haskell. I still use it despite being quite comfortable in and having used Python and Clojure in production because the advantages have been profound. I get you don’t share in that belief, IME, it’s usually unfamiliarity or discomfort. I didn’t like feeling stupid at first either. I tried and failed to learn Haskell many times, that’s partly why I started writing a book years ago. I gave a talk about having failed to learn Haskell over the course of several years too. I assure you it was worth it in the end.

                                                            I see you getting stuck into your idiosyncratic definition of what a type system is with soc so let me cite Robert Harper. I think the point is elaborated in PFPL as well but I don’t remember it being very accessible.

                                                            1. 3

                                                              It seems to mostly be users of untyped languages feeling insecure/defensive about it.

                                                              I get you don’t share in that belief … I didn’t like feeling stupid at first either.

                                                              I see you getting stuck into your idiosyncratic definition of what a type system is

                                                              Are you able to have a discussion with someone without making fun of them?

                                                              If I said I was comfortable programming in languages with good static type systems, would you accept that it’s possible for someone to have different preferences without being objectively wrong, or are you going to say that my experience doesn’t count?

                                                              1. 2

                                                                You can do better than preference, but this isn’t the time or place for that conversation. Hit me up another time.

                                                            2. 3

                                                              Technically (I know, I know) every language has a static type system.

                                                              In shell this system has only one type (string) and there is no need for a typechecker because and value can always be used anywhere a string can be used (since they are all strings). You have some arguments about shell functions (they’re not strings… but also aren’t values).

                                                              Bash has a bit more in it. Every value in bash has the type of anonymous union across string, list, etc. There’s still only one type in the static type system, so again, no typechecker.

                                                              In Ruby, there is still only one type, but now it has a name (RbValue) and it is a tagged union. (Again, reasonable people can have arguments about if it counts as a union since new tags can be introduced at runtime. Tagged union is the most obvious thing to call it, but you might want to call it Dynamic or some such, but this does not fundamentally change the description of the static type system).

                                                              1. 2

                                                                All dynamic typing means is that types exist at runtime.

                                                                I’m not sure how this can be true:

                                                                A type system is a tractable syntactic method for proving the absence of certain program behavior by classifying phrases according to the kinds of values they compute.

                                                                With other words, types are used to reject programs according to the rules specified by the type system at compile-time.

                                                                There might be artifacts of types encoded into the compiled program to facilitate the execution of that program, but these runtime tags are are values, not types.

                                                                1. 1

                                                                  You’re defining a “type system” as “a static type system”. That’s like me defining a “programming language” as “compiled”, and then saying that Python is clearly not a programming language.

                                                                  1. 2

                                                                    There is no “dynamic” type system. A type system is a “static” type system is a type system.

                                                                    1. 2

                                                                      If you’re unwilling to even acknowledge that your preferred definition is not universal, I don’t see how we can have any meaningful discussion.

                                                                      1. 2

                                                                        The definition is a literal quote from Pierce.

                                                                        Which definition would you propose instead, which doesn’t dilute the term “type system” to the point where any random bit pattern in memory can be construed as a type?

                                                                        1. 2

                                                                          One guy makes a claim about something that’s widely contested. It’s popular in a subset of academia. Now, it’s undeniable truth to be reinforced for all time. Am I following that argument about Pierce correctly?

                                                                          I’ve seen definitions like his or those we’re getting in this thread. I’ve also seen in formal methods community that some build things on a computational basis where some tech computes something that supports the logical system (eg type system). They use a mix of logic and computation to get things done with user defining the types as they go for their specific programs, proofs, and so on. That’s a lot more like developing with languages using dynamic, strong typing far as foundational concepts. Then, some say dynamic is a subset of static but they work so differently in how they’re used. Seem like independent lines of thought much like ALGOL68 vs LISP 1.5.

                                                                          I doubt the matter is settled because Pierce or any subset of CompSci says so. That experienced programmers are still arguing about it hints at this.

                                                                          1. 2

                                                                            I doubt the matter is settled because Pierce or any subset of CompSci says so. That experienced programmers are still arguing about it hints at this.

                                                                            That’s a bit like arguing that the shape of the earth is not settled, because there are camps advocating for a spherical model and camps arguing for a flat earth model.

                                                                            To cut it short, one is science, the other one is nonsense.

                                                            3. 7

                                                              I really wish if in defense of spec and dynamic types that rich hickey et al would use the same defense that aria haghighi used when he introduced schema: sure, you can verify these same kinds of things in a dependently typed language, but those are currently much harder to use and these dynamic checks get you most of the way there with less effort.

                                                              1. 7

                                                                One thing that is rarely mentioned in the static vs dynamic debate is whether the programming language compiler is actually the right place for static typing.

                                                                I have been doing a lot of work lately that makes me believe that schemas and types are much more useful in databases and wire formats than they are in programming languages themselves. Examples for me include data modeling in Elasticsearch (where types determine query and aggregation capabilities) and Parquet (where types determine storage costs and read/parse speeds). I would contrast these two with, say, MongoDB and JSON, where the lack of types and schemas in these layers leads to massive loss of “effectiveness”, to borrow Hickey’s term.

                                                                Meanwhile, in programming language compilers themselves, types are often a source of “wrestling with the compiler” for even the well-trained senior programmer and are rarely the source of order of magnitude performance gains, at least not at cluster scale and petabyte data scale. The loss of programmer time is also simply a bad opportunity cost bet. Even the single-core speedups come more from “low-level optimizations” than from type models, e.g. in Python they come from writing code in C and Cython to strip out interpreter overhead.

                                                                I realize here I am talking much more about speed than program correctness. But for me, correctness comes at such a higher level than the code itself. It comes from users.

                                                                1. 3

                                                                  Even the single-core speedups come more from “low-level optimizations” than from type models, e.g. in Python they come from writing code in C and Cython to strip out interpreter overhead.

                                                                  Non sequitur. Python is dynamically typed and the speedups come from implementing it in C … which is statically typed (to an extent, anyway).

                                                                  1. 5

                                                                    I’d say C is “machine typed”, rather than statically typed in the way Haskell programmers or Java/Scala programmers think about the world.

                                                                    1. 3

                                                                      It’s not machine typed and on purpose. BCPL was machine-typed:

                                                                      https://en.wikipedia.org/wiki/BCPL

                                                                      Thompson and Ritchie changed that. See this vid:

                                                                      https://vimeo.com/132192250

                                                                2. 3

                                                                  A transcript is now available.