1. 95
  1.  

  2. 41

    The claim is simple: in a static type system, you must declare the shape of data ahead of time, but in a dynamic type system, the type can be, well, dynamic! It sounds self-evident, so much so that Rich Hickey has practically built a speaking career upon its emotional appeal. The only problem is it isn’t true.

    Immediate standing ovation from me.

    I can only assume that oft-made claim is perpetuated from a position of ignorance. Have those people actually tried doing the thing in a statically typed language that they claim a statically typed language cannot do? Here’s an approach that appears all over my Haskell projects:

      req <- requireCheckJsonBody :: Handler Value
      let chargeId = req ^. key "data" . key "object" . key "id" . _String
    

    I don’t know (or care) what the exact structure of the JSON coming over the network will look like. I just know it will contain this one field that I care about, and here I pull it out and read it as a string.

    Do I need the entire JSON string to conform to some specific protocol (more specific than JSON itself)? No. I am just parsing it as some JSON (which is represented with the Value type).

    Do I need to parse it into some complex data type? No. I’m just building a string. I am doing — in Haskell — exactly the kind of thing that Clojurists do, but without being smug about it.


    If we keep the datatype’s constructor private (that is, we don’t export it from the module that defines this type), then the only way to produce a UserId will be to go through its FromJSON parser.

    I’m glad I read this article even for this design tip alone. I had never thought to do it this way; I thought a “smart constructor” was always necessary, even when that seemed like overkill.

    1. 5
        let chargeId = req ^. key "data" . key "object" . key "id" . _String
      

      So what does this piece of code actually do? Get the value under data->object->id as a String? _String is there to prevent name clashes with actual String? Is the magic here that the JSON payload isn’t parsed any more than it needs to be?

      Stylistically, do you know why Haskell people often seem to decide to use weird operators? Are all alternatives somehow worse?

      1. 8

        So what does this piece of code actually do? Get the value under data->object->id as a String?

        Yeah, exactly. This is how the Stripe API structures their responses. I could have picked a simpler hypothetical example, but I think even this real-world case is simple enough.

        _String is there to prevent name clashes with actual String?

        I believe so, yes. This is just a thing in the lens library.

        Is the magic here that the JSON payload isn’t parsed any more than it needs to be?

        I believe it is parsed only as much as necessary, yes. I’m not sure there’s any magic happening.

        Stylistically, do you know why Haskell people often seem to decide to use weird operators? Are all alternatives somehow worse?

        There are plenty of alternative syntaxes and approaches you could opt for. I happen to find this easy enough to read (and I think you do too, since you worked out exactly what it does), but that is of course subjective.

        1. 3

          the syntactic weirdness is mostly due to the fact that the base grammar is very simple, so you end up basically relying on making infix operators to build symbol-ful DSLs.

          This is very powerful for making certain kinds of libraries, but means that lots of Haskell looks a bit “out there” if you haven’t looked at code using a specific library before. This tends to be at its worst when doing stuff like JSON parsing (where you have very variably-shaped data)

          1. 6

            Although conversely, I think more typical parsing with Aeson (especially the monadic form) is usually very tidy, and easy to read even by people not familiar with Haskell. It’s much less noisy than my lens example.

            Here’s an example: https://artyom.me/aeson#recordwildcards

            I think you probably know this, but I am posting here mostly so that other curious onlookers don’t get the wrong idea and think that Haskell is super weird and difficult.

        2. -5

          Lol what - you’re defining a benefit of dynamically typed language with your example. The json in your case IS a dynamic object.

          1. 7

            I think you are quite confused about what we’re discussing.

            The discussion is around type systems in programming languages. JSON is just a protocol. The JSON that my example parses is not a “dynamic object”. There is no such thing as a JSON object. JSON is only ever a string. Some data structure can be serialised as a JSON string. A JSON string can potentially be parsed by a programming language into some data structure.

            The JSON protocol can be parsed by programming languages with dynamic type systems, e.g., Clojure, and the protocol can also be parsed by programming languages with static type systems, e.g., Haskell.

            My example is taken verbatim from some Haskell systems I’ve written, so it is not “defining a benefit of dynamically typed language”.

            You’re going to have to go and do a bit more reading, but luckily there is plenty of material online that explains these things. I think your comment is a good example of the kind of confusion the article’s author is trying to address.

            1. 2

              I read the article, and I agree somewhat with the parent commenter. It really seems that the author – and perhaps you as well – was comfortable with the idea of potentially declaring parts of the program as just handling lots of values all of a single generic/opaque/relatively-underspecified type, rather than of a variety of richer/more-specified types.

              That position is not all that far from being comfortable with all values being of a single generic/opqaue/relatively-underspecified type. Which is, generally, the most charitable description the really hardcore static-typing folks are willing to give to dynamically-typed languages (i.e., “in Python, all values are of type object”, and that’s only if someone is willing to step up their politeness level a bit from the usual descriptions given).

              In other words, a cynical reading would be that this feels less like a triumphant declaration of “see, static types can do this!” and more an admission of “yeah, we can do it but only by making parts of our programs effectively dynamically typed”.

              1. 3

                I don’t know how you’ve come to this conclusion. Moreover, I don’t understand how your conclusion is related to the argument in the article.

                In other words, a cynical reading would be that this feels less like a triumphant declaration of “see, static types can do this!” and more an admission of “yeah, we can do it but only by making parts of our programs effectively dynamically typed”.

                What does this even mean? How did you come up with this idea? When you want to parse some arbitrary JSON into a more concrete type, you can just do that. How does parsing make a program no longer statically typed?

                1. 2

                  What is the difference between:

                  1. “Everything in this part of the program is of type JSON. We don’t know what the detailed structure of a value of that type is; it might contain a huge variety of things, or not, and we have no way of being sure in advance what they will be”.
                  2. “Everything in this part of the program is of type object. We don’t know what the detailed structure of a value of that type is; it might contain a huge variety of things, or not, and we have no way of being sure in advance what they will be”.

                  The first is what the article did. The second is, well, dynamic typing.

                  I mean, sure, you can argue that you could parse a JSON into some type of equally-generic data structure – a hash table, say – but to usefully work with that you’d want to know things like what keys it’s likely to have, what types the values of those keys will have, and so on, and from the type declaration of JSON you receive absolutely none of that information.

                  In much the same way you can reflect on an object to produce some type of equally-generic data structure – a hash table, say – but to usefully work with that you’d want to know things like… hey, this is sounding familiar!

                  Now do you see what I mean? That’s why I said the cynical view here is the author has just introduced a dynamically-typed section into the program.

                  1. 3

                    Any program which reads some JSON and parses it will be making some assumptions about its structure.

                    This is true of a program written in a dynamically-typed language.

                    This is true of a program written in a statically-typed language.

                    Usually, you will want to parse a string of JSON into some detailed structure, and then use that throughout your system instead of some generic Value type. But you don’t necessarily need to do that. Nothing about writing in a statically-typed programming language forces you to do that. And no, Haskell programmers don’t generally intentionally try to make their programs worse by passing Value types, or generic Map types, or just anything encoded as a String, throughout their program. That would be stupid.

                    1. 3

                      OK, I’ll do the long explanation.

                      Many programmers whose primary or sole familiarity is with statically-typed languages assume that in dynamically-typed languages all code must be littered with runtime type checks and assertions. For example, I’ve run into many people who seem to think that all Python code is, or should be, full of:

                      if isinstance(thing, some_type) ...
                      elif isinstance(thing, some_other_type) ...
                      

                      checks in order to avoid ever accidentally performing an operation on a value of the wrong type.

                      While it is true that you can parse a JSON into a data structure you can then pass around and work with, the only way to meaningfully do so is using your language’s equivalent idiom of

                      if has_key(parsed_json, some_key) and isinstance(parsed_json.get(some_key), some_type)) ...
                      elif has_key(parsed_json, some_other_key) and isinstance(parsed_json.get(some_other_key), some_other_type) ...
                      

                      since you do not know from the original type declaration whether any particular key will be present nor, if it is present, what type the value of that key will have (other than some sort of suitably-generic JSONMember or equivalent).

                      Which is to say: the only way to effectively work with a value of type JSON is to check it, at runtime, in the same way the stereotypical static-typing advocate thinks all dynamically-typed programmers write all their code. Thus, there is no observable difference, for such a person, between working with a value of type JSON and writing dynamically-typed code.

                      Now, sure, there are languages which have idioms that make the obsessive checking for members/types etc. shorter and less tedious to write, but the programmer will still be required, at some point, either to write such code or to use a library which provides such code.

                      Thus, the use of JSON as a catch-all “I don’t know what might be in there” type is not distinguishable from dynamically-typed code, and is effectively introducing a section of dynamically-typed code into the program.

                      1. 3

                        I still don’t get what point you’re trying to make. Sorry.

                        Thus, the use of JSON as a catch-all “I don’t know what might be in there” type is not distinguishable from dynamically-typed code, and is effectively introducing a section of dynamically-typed code into the program.

                        This now sounds like you’re making an argument between parsing and validation, and misrepresenting it at static vs dynamic.

                        1. 2

                          This now sounds like you’re making an argument between parsing and validation, and misrepresenting it at static vs dynamic.

                          For an alternative formulation, consider that people often claim, or want to claim, that in a statically-type language most of the information about the program’s behavior is encoded in the types. Some people clearly would like a future where all such information is encoded in the types (so that, for example, an add function would not merely have a signature of add(int, int) -> int, but a signature of add(int, int) -> sum of arguments which could be statically verified).

                          I have complicated thoughts on that – the short hot-take version is those people should read up on what happened to logical positivism – but the point here is a reminder that this article, which was meant to show a way to have nice statically-typed handling of unknown data structures, was able to do so only by dramatically reducing the information being encoded in the types.

                          1. 3

                            the point here is a reminder that this article, which was meant to show a way to have nice statically-typed handling of unknown data structures, was able to do so only by dramatically reducing the information being encoded in the types.

                            …How else would a program know what type the program’s author intends for the arbitrary data to be parsed into? Telepathy?

                            1. 1

                              I think at this point it’s pretty clear that there’s nothing I can say or do that will get you to understand the point I’m trying to make, so I’m going to bow out.

                    2. 3

                      What is the difference between:

                      1. “Everything in this part of the program is of type JSON. We don’t know what the detailed structure of a value of that type is; it might contain a huge variety of things, or not, and we have no way of being sure in advance what they will
                      2. “Everything in this part of the program is of type object. We don’t know what the detailed structure of a value of that type is; it might contain a huge variety of things, or not, and we have no way of being sure in advance what they will be”.

                      The first is what the article did. The second is, well, dynamic typing.

                      The difference is that in a statically-typed language, you can have other parts of the program where proposition 1. is not the case, but in a dynamically-typed language proposition 2. is true all the time and you can’t do anything about it. No matter what style of typing your language uses, you do have to inspect the parsed JSON at runtime to see if it has the values you expect. But in a statically-typed language, you can do this once, then transform that parsed JSON into another type that you can be sure about the contents of; and then you don’t have to care that this type originally came from JSON in any other part of your program that uses it.

                      Whereas in a dynamically-typed language you have to remember at all times that one value of type Object happens to represent generic JSON and another value of type Object happens to represent a more specific piece of structured data parsed from that JSON, and if you ever forget which is which the program will just blow up at runtime because you called a function that made incorrect assumptions about the interface its arguments conformed to.

                      Anyway even introducing a “generic JSON” type is already encoding more useful information than a dyanmically-typed language lets you. If you have a JSON type you might expect to have some methods like isArray or isObject that you can call on it, you know that you can’t call methods that pertain to completely different types like getCenterPoint or getBankAccountRecordsFromBankAccountId. Being able to say that a value is definitely JSON, even if you don’t know anything about that JSON, at least tells you that it’s not a BankAccount or GLSLShaderHandle or any other thing in the vast universe of computing that isnt JSON.

                      1. 2

                        Whereas in a dynamically-typed language you have to remember at all times that one value of type Object happens to represent generic JSON and another value of type Object happens to represent a more specific piece of structured data parsed from that JSON, and if you ever forget which is which the program will just blow up at runtime because you called a function that made incorrect assumptions about the interface its arguments conformed to.

                        This is where the discussion often veers off into strawman territory, though. Because I’ve written code in both dynamically and statically typed languages (and hybrid-ish stuff like dynamically-typed languages with optional type hints), and all the things people say about inevitable imminent doom from someone passing the wrong types of things into functions are, in my experience, just things people say. They don’t correspond to what I’ve actually seen in real programming.

                        That’s why in one of my comments further down I pointed out that the generic JSON approach used in the article forces the programmer to do what people seem to think all dynamically-typed language programmers do on a daily basis: write incredibly defensive and careful code with tons of runtime checks. My experience is that people who prefer and mostly only know statically-typed languages often write code this way when they’re forced to use a dynamically-typed language or sections of code that are effectively dynamically-typed due to using only very very generic types, but nobody who’s actually comfortable in dynamic typing does that.

                        And the best literature review I know of on the topic struggled to find any meaningful results for impact of static versus dynamic typing on defect rates. So the horror stories of how things will blow up from someone forgetting what they were supposed to pass into a function are just that: stories, not data, let alone useful data.

                        Anyway, cards on the table time here.

                        My personal stance is that I prefer to write code in dynamically-typed languages, and add type hints later on as a belt-and-suspenders approach to go with meaningful tests (though I have a lot of criticism for how Python’s type-hinting and checking tools have evolved, so I don’t use them as much as I otherwise might). I’ve seen too much statically-typed code fall over and burn the instant someone pointed a fuzzer at it to have much faith in the “if it passes type checks, it’s correct” mantra. And while I do enjoy writing the occasional small thing in an ML-ish language and find some of the idioms and patterns of that language family pleasingly elegant, mostly I personally see static typing as a diminishing-returns technique, where beyond a very basic up-front pass or two, the problems that can be prevented by static typing quickly become significantly smaller and/or less likely as the effort required to use the type system to prevent them increases seemingly without bound.

                        1. 3

                          This is where the discussion often veers off into strawman territory, though. Because I’ve written code in both dynamically and statically typed languages (and hybrid-ish stuff like dynamically-typed languages with optional type hints), and all the things people say about inevitable imminent doom from someone passing the wrong types of things into functions are, in my experience, just things people say. They don’t correspond to what I’ve actually seen in real programming.

                          I disagree - passing the wrong types of things into functions is definitely a phenomenon I’ve personally seen (and debugged) in production Ruby, JavaScript, and Python systems I’ve personally worked on.

                          For instance, I’ve worked on rich frontend JavaScript systems where I was tasked with figuring out why a line of code a.b.c was throwing TypeError but only sometimes. After spending a bunch of time checking back to see where a ultimately came from, I might find that there was some function many frames away from the error in the call stack that sets a from the result of an xhr that isn’t actually guaranteed to always set a key b on a, and that code was not conceptually related to the code where the error happened, so no one thought it was unusual that a.b wasn’t guaranteed, which is how the bug happened.

                          In a statically typed language, I could convert the JSON that will eventually become a into a specifically-typed value, then pass that down through 10 function calls to where it’s needed, without worrying that I’ll find 10 frames deep that SpecificType randomly doesn’t have a necessary field, because the conversion from the generic to the specific would’ve failed at the conversion site.

                          I am a fan of statically typed languages, and a huge reason for this is because I’ve debugged large codebases in dynamically-typed languages where I didn’t write the original code and had to figure it out by inspection. Static typing definitely makes my experience as a debugger better.

                          1. 1

                            definitely a phenomenon I’ve personally seen (and debugged)

                            Notice I didn’t say “your stories are false”.

                            Nor did you refute my claims that I’ve seen statically-typed code which passed static type checks fall over and crash when fuzzed.

                            We each can point to instances where our particular bogeyman has in fact happened. Can either of us generalize usefully from that, though? Could I just use my story to dismiss all static typing approaches as meaningless, because obviously they’re not catching all these huge numbers of bugs that must, by my generalization, be present in absolutely every program every person has ever written in any statically-typed language?

                            The answer, of course, is no. And so, although, you did write a lot of words there, you didn’t write anything that was a useful rebuttal to what I actually said.

                2. 0

                  I appreciate your condencending tone but really you should work on your ability to argument. The original post claims that this statement is not true:

                  in a static type system, you must declare the shape of data ahead of time, but in a dynamic type system, the type can be, well, dynamic!

                  You argue however that this is indeed not true because you can have “dynamic” data and “static” types when that’s just a silly loophole. Surely you want data as an object right? A string of characters without the meta structure are completely useless in the context of programming.

                  Just because you can have a static type that doesn’t have strict, full protocol implementation doesn’t mean that you don’t need to declare it before hand which renders the original statement absolutely correct - you must declare static shape of data that matches what your type expects. The claim that types can be “lose” doesn’t invalidate this statement.

                  1. 4

                    I appreciate your condencending tone but really you should work on your ability to argument.

                    I’m sorry you feel that way. I genuinely did my best to be kind, and to present some absolute truths to you that I had hoped would clear up your confusion. Unfortunately, it looks like you’ve decided to dig your heels in.

                    You argue however that this is indeed not true because you can have “dynamic” data and “static” types when that’s just a silly loophole.

                    I don’t know what you are talking about. Dynamic data? What does this mean? And what silly loophole?

                    In the context of this argument: the JSON being parsed is a string. It’s not static. It’s not dynamic. It’s a string.

                    which renders the original statement absolutely correct - you must declare static shape of data that matches what your type expects.

                    No, you don’t. Again, you have misunderstood me, you have misunderstood the article, and you have misunderstood some pretty basic concepts that are fundamental to constructing a cohesive argument in this debate.

                    The argument is whether or not — in a statically-typed programming language — the JSON string you are parsing needs to conform 1:1 to the structure of some data type you are trying to parse it into.

                    The answer is: No. Both statically-typed and dynamically-typed programming languages can parse arbitrary data.

                    1. 0

                      The answer is: No. Both statically-typed and dynamically-typed programming languages can parse arbitrary data.

                      That was never the topic; you can parse arbitrary data with a pen and a piece of toilet paper…

                      1. 2

                        That was never the topic

                        Yes it was. Perhaps you should have actually read the article.

                        you can parse arbitrary data with a pen and a piece of toilet paper…

                        At this point, it is clear you are not even trying to add anything constructive. I suggest we leave this discussion here.

                        1. 0

                          Oof, I guess there had to be first failed discussion experience here on lobsters. I’m sorry but you are absolutely inept at discussing this. Maybe it’s better if we don’t continue this. Cheers.

                3. 2

                  The grandparent’s code example uses way more than one type.

              2. 9

                Seems to me there are at least three topics that get conflated into one discussion here.

                1. What is the world like? That is, can I faithfully represent the world inside a static type system? I think the answer is no, corbin seems to make a good case. (But I’m weak on CT)

                2. What should my code be like? That is, what types of code do I want to create and look at while I’m programming? This is what most of the discussion on larger forums like HN is about.

                3. What is the frickin’ actual problem I’m trying to solve? This is what jgt is getting to. I don’t care about anything else in the universe aside from “what is this thing here and what do I have to do to it?” The static-vs-dynamic type discussion seems to be around what sorts of superstructures you want around executing this solution. Many times we lose track of just actually solving the problem by getting caught up in #1 or #2

                We need incremental strong typing. That is, we need enough type control over our data in order to do one small thing and only that. Once we start modeling the universe or debating what makes good code we lose track of that.

                1. 4

                  The key point is mentioned in the final sentence: “solving a slightly more restricted version of the problem”.

                  1. 4

                    This is a case of improper data modeling, but the static type system is not at fault—it has simply been misused.

                    The static type system is never at fault, it behaves just like the programmer tells it to. But this is kind of handwaving over the very point this article attempts to address. This particular case of “improper data modeling” would never be a problem on dynamically-typed systems.

                    Bad analogy time: it is pretty much like advocating the use of anabolic steroids, because they make you so much stronger, but when the undesired side effects kick in, you blame the hormonal system for not keeping things in balance.

                    1. 9

                      Bad analogy time: it is pretty much like advocating the use of anabolic steroids, because they make you so much stronger, but when the undesired side effects kick in, you blame the hormonal system for not keeping things in balance.

                      To me it feels like that’s exactly what proponents of dynamic typing often do “I can write all code super fast” and then when people say there’s issues when it is accidentally misused (by another programmer or the same programmer, in the future) it is always “you should’ve used more hammock time to think about your problem real hard” or “you should’ve written more tests to make sure it properly handles invalid inputs”.

                      1. 5

                        You are not wrong and this is just a proof that the debate around type systems is still too immature. There is certainly a component of dynamism in every computer system that programmers crave, and it usually lives out of bounds of the language environment, on the operating system level. Dynamically typed languages claim to offer that dynamism inside their own environment, but most of the programs don’t take advantage of that.

                        There is no known definitive argument on either side that would definitively bury its respective contender. Programmers sometimes seem too afraid of some kind of Tower of Babel effect that would ruin the progress of Computer Science and I believe that the whole debate around static and dynamic type systems is just a reflex of that.

                      2. 2

                        This particular case of “improper data modeling” would never be a problem on dynamically-typed systems.

                        I think this is addressed in the appendix about structural vs nominal typing. In particular, very dynamic languages like Python and Smalltalk still allow us to do such “improper data modelling”, e.g. by defining/using a bunch of classes which are inappropriate for the data. Even if we stick to dumb maps/arrays, we can still hit essentially the same issues once we get a few functions deep (e.g. if we’ve extracted something from our data into a list, and it turns out we need a map, which brings up questions about whether there’ll be duplicates and how to handle them).

                        Alternatively, given the examples referenced by the author (in the linked “parse, don’t validate” post) it’s reasonable to consider all data modelling in dynamically-typed systems to be improper. This sounds a bit inflammatory, but it’s based on a core principle of the way dynamically-typed languages frame things: they avoid type errors in principle by forcing all code to “work” for all values, and shoehorning most of those branches into a sub-set of “error” or “exceptional” values. In practice this doesn’t prevent developers having to handle type errors; they just get handled with branching like any other value (with no compiler to guide us!). Likewise all dynamic code can model all data “properly”, but lots of code will model lots of data by producing error/exceptional values; that’s arguably “proper” since, after all, everything in a dynamic system might be an error/exception at any time.

                        Side note: when comparing static and dynamic languages, it’s important to remember that using “exceptions” for errors is purely a convention; from a language/technology standpoint, they’re just normal values like anything else. We can assign exceptions to variables, make lists of exceptions, return exceptions from functions, etc. it’s just quite uncommon to see. Likewise “throwing” and “catching” is just a control-flow mechanism for passing around values; it doesn’t have anything to do with exception values or error handling, except by convention. I notice that running raise 42 in Python gives me TypeError: exceptions must derive from BaseException, which doesn’t seem very dynamic/Pythonic/duck-typical; yet even this “error” is just another value I can assign to a variable and carry on computing with!

                        1. 1

                          The point I was trying to make is that, in the example mentioned in the article, the reason why the type description was inaccurate at first has only to do with the fact that the programmer must provide the checker information about UserId‘s subtype. On a dynamically-typed system, as long as the JSON type supports Eq, FromJSON and ToJSON, you are fine, and having to accurately determine UserId‘s subtype would never be a problem.

                          So I do understand the appeal of static typing in building units, but not systems, especially distributed ones, and this is why I believe the article is myopic, but dynamic language advocates do a terrible job in defending themselves. Having to process JSON payloads is the least of the problems if you are dealing with distributed systems; how would you accurately type check across independent snippets of code in a geographically-distributed network over which you have no control is a much more interesting problem.

                          1. 1

                            On a dynamically-typed system, as long as the JSON type supports Eq, FromJSON and ToJSON, you are fine, and having to accurately determine UserId‘s subtype would never be a problem.

                            That’s not true. At some point your dynamically typed system will make an assumption about the type of value (the UserId in this case) that you’re applying some function to.

                            1. 1

                              For practical purposes, it is true. The system internals indeed need to resolve the dependency on that interface, indeed, either with fancy resolution mechanisms or attempting to call the function in a shoot-from-the-hip fashion. But it is not common between dynamic language implementations that the programmer needs to specify the type, so it is not a problem.

                      3. 2

                        Great article - And I am a strong lover of Dynamic typing languages. But I don’t believe they have any sort of fundamental superiority, and this article debunks it well.

                        My preference for Dynamic typing comes entirely from a personal preference, I prefer the simplicity they give over the boilerplate of static types. But I do work with both and I can see the value static types can bring.

                        On one defense of dynamic languages though, this part:

                        We know, for example, that this application doesn’t care about the timestamp field, since it never appears in any of the payload types. In the dynamically-typed program, we’d have to audit every code path to see whether or not it inspects that field, which would be a lot of error-prone work!

                        You can argue that it’s also an unfair thing to say about dynamic languages, because it is bad modelling, the same thing the author has criticized on people talking about static types.

                        It’s not because a language has dynamic types that it should be typeless, a good developer will also use predefined types and have classes/enums/structs of some kind and some sort of structure, that would allow you to know the timestamp field is not used.

                        To be fair, it’s also possible to do bad modelling on a static language, and force someone to have to go over every code path to know if timestamp is used or not! I’ve seen enough bad use of generic types in static languages that forced me to look at every code path to know which field of an XML is used.

                        If we’re to argue on both cases on good discipline and well defined domains, the code should be as readable in both cases, but the static type will have a richer compiler error system, code editor, need less tests, but the domain can be typed and well written in any typing systems.

                        1. 2

                          No value judgments here, please. But it just crossed my mind that apologies to static typing pretty much assume some level of historical materialism, in which they advocate that adaptations to the code, and hence its evolution over a timeline, are at least partially tied to the data structures one must process.

                          [sarcasm] Software history repeats itself first as remote exploits, then as fuzz testing. [/sarcasm]

                          1. 1

                            I think the Lexi Lambda post is a good one, although I found its argument kind of obvious–maybe because I lean toward static typing myself. The other post that was merged in, though, I don’t fully understand. It says:

                            “So, give me an example of a thing dynamically-typed languages can do that statically-typed languages can’t?”

                            and then gives the example of sayHello = putStrLn messageToBeDefined at a fresh REPL. Since messageToBeDefined is an undefined symbol, this is going to fail in almost all languages. In Python:

                            >>> print(messageToBeDefined)
                            Traceback (most recent call last):
                              File "<stdin>", line 1, in <module>
                            NameError: name 'messageToBeDefined' is not defined
                            

                            or in Scheme:

                            > (print messageToBeDefined)
                            . . messageToBeDefined: undefined;
                             cannot reference an identifier before its definition
                            

                            What is this supposed to be demonstrating?

                            1. 2

                              It was supposed to be demonstrating this:

                              Python 3.7.4 (tags/v3.7.4:e09359112e, Jul  8 2019, 20:34:20) [MSC v.1916 64 bit (AMD64)] on win32
                              Type "help", "copyright", "credits" or "license()" for more information.
                              >>> def sayHello():
                              	print(messageToBeDefined)
                              
                              	
                              >>> messageToBeDefined = 'hello, world'
                              >>> sayHello()
                              hello, world
                              >>> messageToBeDefined = 'hi, everyone'
                              >>> sayHello()
                              hi, everyone
                              

                              In contrast to

                              GHCi, version 8.4.4: http://www.haskell.org/ghc/  :? for help
                              Prelude> messageToBeDefined = "hello, world"
                              Prelude> sayHello = putStrLn messageToBeDefined
                              Prelude> :t sayHello
                              sayHello :: IO ()
                              Prelude> sayHello
                              hello, world
                              Prelude> messageToBeDefined = "hi, everyone"
                              Prelude> sayHello
                              hello, world
                              
                              1. 1

                                Ah, I see. It’s true that Haskell doesn’t allow this (without using a global State monad or something to simulate it), but other statically typed languages like C++ do. (Even Rust would, although you have to use something like an Arc.)

                                1. 2

                                  Actually the argument was less about feasibility, but how does the community deal with these discussions. Coming from a Unix/C background myself, I don’t have a horse in this race, though.

                                2. 1

                                  That’s a property of Haskell (specifically GHCi in this case I think), not static typing, right? I think you can get both behaviors in e.g. Scheme with (untested)

                                  (define message "hello, world")
                                  (define (say-hello) (display message))
                                  ; Python mode:
                                  (set! message "hello, Brent")
                                  ; Haskell mode:
                                  (define message "hello, Greg")
                                  

                                  edit: i.e. it’s just the distinction between introducing a new variable binding and modifying an existing one.

                                  1. 1

                                    That’s a property of Haskell (specifically GHCi in this case I think), not static typing, right?

                                    This is a property of sound strong static type systems, which, in that case, is represented with Haskell code. But the real difference there is the “static” part.

                                    I think you can get both behaviors in e.g. Scheme with (untested)

                                    Truth is, you could either implement interpreters of statically-typed environments in a dynamically-typed language, or dynamically-typed environments with a statically-typed language. So that comes to me as no surprise. But thanks for mentioning that. My impression, though, is that getting a dynamically-typed environment to behave statically requires so much more boilerplate than its counterpart.

                                    1. 3

                                      Oh, my mistake, I missed the missing initial definition of messageToBeDefined in the Python snippet.

                                      Hmm, I never thought about that relationship, but I don’t know if sound static typing completely precludes dynamic variable binding (assuming that’s what this is about and I’m not completely missing the point). I just tried this in Typed Racket, which is statically typed (and I believe sound):

                                      > (define (say) (display msg))
                                      ; readline-input:1:23: Type Checker: missing type for top-level identifier;
                                      ;  either undefined or missing a type annotation
                                      ;   identifier: msg
                                      ;   in: msg
                                      ; [,bt for context]
                                      > (: msg String)
                                      > (define (say) (display msg))
                                      > (say)
                                      ; msg: undefined;
                                      ;  cannot reference an identifier before its definition
                                      ;   in module: top-level
                                      ; [,bt for context]
                                      > (define msg 6)
                                      ; readline-input:5:12: Type Checker: type mismatch
                                      ;   expected: String
                                      ;   given: Positive-Byte
                                      ;   in: 6
                                      ; [,bt for context]
                                      > (define msg "hello")
                                      > (say)
                                      hello
                                      > (define msg "hello again")
                                      > (say)
                                      hello again
                                      > 
                                      

                                      (Aside: the GHCi feature I was thinking of was -fdefer-out-of-scope-variables but that still errors when actually running it.)

                                      1. 3

                                        This is where things get tricky. People (e.g. me) usually conflate static/dynamic typing with early/late binding, either due to ignorance or laziness. It is very common that you find early binding on statically-typed systems and late binding on dynamically-typed systems. But binding strategies are not a binary choice: they sit in a spectrum. It is expected that static typing systems introduce the necessity for earlier binding to some degree, because type checks, at least, should be provided ahead of time.

                                        Typed Racket is usually classified as a gradually-typed language. I won’t risk an explanation of that, but suffice to say that you get type checks before execution without usually introducing any restrictions on runtime.

                              2. -3

                                This article is obviously wrong in its conclusion. To see how, first recall that while Haskell’s types don’t form a category, we can imagine a “platonic” Hask whose objects are types, whose arrows are functions, and where undefined and friends have been removed.

                                Now, consider that platonic Hask is but one object of Cat. From size issues, it is immediate that Cat cannot be a subcategory of Hask; that is, that Hask cannot describe all of Cat’s objects. It follows that Haskell typeclasses like Functor are not arrows in Cat, but endofunctors on Hask, and that Control.Category does not capture objects in Cat, but the internal category objects in Hask.

                                Finally, pick just about any 2-category, indeed say Cat, and then ask whether Hask can represent it faithfully: The answer is a clear, resounding, and obvious “no”. Going further, pick any ∞-category, say Tomb, and then ask whether Hask can even represent a portion of any object; an ∞-object is like a row of objects, one per level, but Haskell’s type system could only see one single level of types at a time. (This is not just theoretical; I have tried to embed Tomb into Haskell, Idris, and Coq, and each time I am limited by the relatively weak type system’s upper limits.)

                                I wonder why the author believes otherwise.

                                1. 16

                                  This article is obviously wrong in its conclusion.

                                  I think the word “obviously” is relative to the reader’s familiarity with category theory.

                                  For the purposes of the misconception she is addressing, the author’s conclusion — to me — is obviously correct.

                                  You appear to be refuting her argument in some different context. I’m interested to hear your argument (although it would probably be a long time before I learn the CT necessary to properly understand your argument), but switching out the context the argument was made in to refute the entire original argument makes your own argument (to me, at least) appear as an attack against a straw-man.

                                  1. -1

                                    My argument ought to follow readily for any ML, and we can see the scars it causes in the design of many MLs. Idris, for example, uses a hierarchy of universes to avoid universe-inconsistency paradoxes as it climbs this tower that I’m talking about. Haskell and Elm don’t bother trying to climb the tower at all. SML and OCaml have exactly one tier, adding on the module system, and strict rules governing the maps between modules and values.

                                    I’m not removing the word “obviously”. Cat obviously contains Hask, Set, and many other common type systems as objects; the size issues around Cat are usually one of the first things mentioned about it. (Third paragraph in WP and nCat, for example.) And Cat is one of the first categories taught to neophytes, too; for example, in the recent series of programmer-oriented lectures on category theory, Programming with Categories, Cat is the second category defined, after Set.

                                    My refutation is of the article’s title: Yes indeed, dynamic type systems are more open, simply because there are certain sorts of infinite objects that, when we represent them symbolically, still have infinite components. Haskell can represent any finite row of components with multi-parameter typeclasses but that is not sufficient for an ∞-category. By contrast, when we use dynamic type systems, especially object-based systems, our main concern is not about the representation of data, since that is pretty easy, but the representation of structures. For categories, for example, there are many different ways to give the data of a category, depending on what the category should do; we can emphasize the graph-theoretic parts, or the set-theoretic parts, or even transform the category into something like a Chu space.

                                    Finally, if static type systems are so great, why isn’t your metatheory, the one you use for metaphysics and navigating the world, a static type system? Probably because you have some sort of open-world assumption built into the logic that you use for day-to-day reasoning, I imagine. This assumption is the “open” that we are talking about when we talk about how “open” a type system is! Just like how we want a metatheory in our daily lives that is open, we all too often want to represent this same sort of open reasoning in our programming languages, and in order to do that, we have to have ways to either subvert and ignore, or entirely remove, limited static types.

                                    1. 5

                                      My argument ought to follow readily for any ML, and we can see the scars it causes in the design of many MLs. Idris, for example, uses a hierarchy of universes to avoid universe-inconsistency paradoxes as it climbs this tower that I’m talking about.

                                      Could you give examples of useful programs that are inexpressible in a typed way without a hierarchy of universes? Even when doing pure mathematics (which demands much stronger logical foundations than programming), most of the time I can fix a single universe and work with (a tiny part of) what lives in it.

                                      When programming in ML, the feature that I want the most badly is the ability to “carve out” subsets of existing types (e.g., to specify that a list must contain a given element). This would be actually useful for specifying preconditions and postconditions of algorithms (which is ultimately the point to programming, i.e., implementing algorithms). But it does not require hierarchical type universes.

                                      Yes indeed, dynamic type systems are more open, simply because there are certain sorts of infinite objects that, when we represent them symbolically, still have infinite components.

                                      You seem to be confusing symbols with their denotation. Symbols are finite out of necessity, but you can use them to denote infinite objects just fine, whether you use a type system or not.

                                      Haskell can represent any finite row of components with multi-parameter typeclasses but that is not sufficient for an ∞-category.

                                      The arity of a multiparameter type class has absolutely nothing to do with n-categories. But, in any case, why is Haskell supposed to do represent ∞-categories in its type system? It is a general-purpose programming language, not a foundation of mathematics.

                                      Finally, if static type systems are so great, why isn’t your metatheory, the one you use for metaphysics and navigating the world, a static type system? Probably because you have some sort of open-world assumption built into the logic that you use for day-to-day reasoning, I imagine.

                                      Every nominal type definition literally brings a new type of thing into existence. What exactly is this, if not dealing with an open world?

                                      And, by the way, my metatheory is ML.

                                      1. 3

                                        Can any programming language usefully represent these infinite objects? Is that ever useful?

                                        Surely you can just build something with opaque objects within Haskell if the type system is too restrictive?

                                    2. 9

                                      I wonder why the author believes otherwise.

                                      Probably because the author isn’t comparing Hask to all of category theory. They’re comparing it to the unitype, which cannot faithfully represent anything at all.

                                      1. -5

                                        As long as we are using “probably” to speak for the author, I think that they probably are not familiar enough with type theory to understand that there are size issues inherent to formalizing type systems.

                                        Please reread the original article; they do not talk about “unityping” or Bob Harper’s view on type theory of languages which don’t know the types of every value.

                                        1. 26

                                          The author is Alexis King, who is a PLT researcher, an expert in both Haskell and Racket and has discussed category theory in depth on Twitter. I’d be shocked if she didn’t understand the ramifications here and was intentionally simplifying things for her target audience.

                                          1. -1

                                            Sure, and I am just a musician. Obviously, therefore, the author is right.

                                            Anyway, they didn’t talk about size issues, nor did they talk about “unitype” ideas, in the article. I am not really fond of guessing what people are talking about. I am happy to throw my entire “probably” paragraph into the trash, as I do not particularly value it.

                                      2. 4

                                        I don’t know enough category theory to follow your argument precisely, but I’d argue that the category theoretic perspective isn’t relevant in this discussion. How much of category theory you can model using Haskell’s type system is totally unrelated to how much you can model with a program written in Haskell. I guess I don’t even need to make this argument, but still, whatever code you were planning to write with Javascript, can be mechanically translated by a Haskell beginner line-by-line to a Haskell program that simply uses JSON.Value everywhere.

                                        I believe the parts of category theory you can’t model in Haskell’s types corresponds to the kinds of relationships you can’t get the type checker to enforce for you. And you go into the language knowing you can’t model everything in types, so that’s no news. What’s relevant is how much you can model, and whether that stuff helps you write code that doesn’t ruin people’s lives and put bread on the table. As a full time Haskeller for a long time, my opinion is that the answer is “yes”.

                                        I think the friction comes from the desire to view the language as some sort of deity that you can describe your most intricate thoughts and it will start telling you the meaning of life. For me, once I stopped treating GHC (Haskell’s flagship compiler) as such and started viewing it as a toolbox for writing ad-hoc support structures to strengthen my architecture here and there it all fell into place.

                                        1. 2

                                          I’m going to quote some folks anonymously from IRC, as I think that they are more eloquent than I am about this. I will say, in my own words, that your post could have “Haskell” replaced with basically any other language with a type system, and the same argument would go through. This suggests that the discussion is not at all about Haskell in particular, but about any language with a type system. I would encourage you to reconsider my argument with that framing.

                                          (All quoted are experts in both Python and Haskell. Lightly edited for readability.)

                                          Maybe another way of making the point is to say that the job of a type system is to reduce the number of programs you can write, and proponents of a type system will argue that enough of the reduction comes from losing stupid/useless/broken programs that it’s worth it.

                                          The problem with this argument and the statement [IRC user] just made is the same, I think. It depends. Specifically, it depends on whether one is trying to use the type system as a mathematical object, or as a practical programming tool. And further, on how good your particular group of programmers is with their practical programming tools on the particular day they write your particular program. With a mathematical system, you can produce something correct and prove it; with a practical programming tool, you can produce something correct and run it.