1. 54
  1.  

  2. 7

    … let’s go shopping!

    1. 2

      Ironically Go looks like one of the few languages on this list that succeed.

      1. 4

        Go does have an easier time because of it’s lack of generics and limited inference, which makes type checking (and inference) pretty simple.

        Of course this may change completely with the Go Generics design draft. From their descriptions it seems to be similar to the simplicity of the old inference algorithm, only inferring function types when all type variables occur in the function argument.

        1. 3

          I really want to know how this will be impacted by Go generics!

          1. 2

            Me too! I haven’t found any information on the (planned) implementation of Go’s generics though (it vaguely alluded to HM’s algorithm W), so we will have to see how it plays out.

            Edit: It looks like the current draft has plans of keeping it simple with a 2-pass unification algorithm in restricted contexts.

          2. 3

            What do you mean by “succeed?” The piece doesn’t talk about success or failure in any meaningful sense as far as I can tell.

        2. 5

          I learned a tremendous amount from reading the concise definitions on this page.

          1. 0

            I’d argue that types are a terrible solution to the actual problem.

            I’d argue the actual problem is, we need to check variables in our languages, for instance for someone’s age, we almost certainly don’t want -32768 as a possible age, as that makes zero sense. Also an age of 32768 is also probably equally stupid.

            we want age to be an integer between 0 and 120 or so. Certainly < 200. That’s what we actually want.

            We can argue about the upper and lower bounds of the age variable, depending on the program being written(i.e. an age of 120 for a program about the romans would be laughable, since they never lived remotely that long). But I hope we can all agree there should be upper and lower bounds for our variables.

            Types, basically don’t do that, and practically every language ever written skips over any sane way to have limits on our variables besides basically int8, int16 and string.

            There are some attempts, Liquid Haskell has a way. Postgres does this pretty well with the check constraint(though it’s not a programming language, obviously). Nim recently got ‘DrNim’ that attempts the same thing. Most other languages fail.

            1. 8

              Types do that. Commonly the pattern looks like having a constructor function that validates the machine type, like smart constructors in Haskell. (Though, as cgenschwap already noted, dependent types can do this in a quite different way.)

              1. 2

                I think you meant types might be able to do that. so I agree, in theory, types can grow to specify constraints, but other than Haskell(with multiple competing solutions apparently) and now Ada(thanks @weinholt), nobody’s type system has this ability that I’m aware of(I’m sure there are some weird esoteric languages out there that do..).

                But no commonly available/used language has anything resembling a way to sanely do constraints. The best you can do is writing a check function and calling it all over the place, hoping you don’t miss a place and your constraint fails to hold, with no warnings if you miss a spot. Languages aren’t immune to the problem, even most databases, except some SQL ones(like PG’s check) pretty much punt on constraints, so it’s a very wide problem.

                Even web frameworks, mostly fail at checking constraints, and it’s rare to see web code in the wild do much beyond the occasional JavaScript-based client-side validation of inputs. Otherwise the most you will see is ‘yes input validation is important’, but almost nobody is doing it. It’s hard, it’s not taught in programming classes or books or documentation(for the most part) and languages by and large punt on the issue.

                I’ve read a few haskell learning sites, and a book, though I’ve never programmed anything useful in Haskell, and I’d never heard of smart constructors before, so even when it’s available, nobody apparently uses it.

                Anyways, the goal here, from my perspective, is we desperately need to validate inputs, and store data with known constraints, and with rare exception, no code does this, and no commonly used languages make this remotely easy. so I think my point stands, constraint checking is still very much not done in the wild.

                Thanks for teaching me about Smart Constructors! :) I <3 learning new things!

                1. 8

                  Pascal also supports it:

                  type
                    Age = 0..200;
                  
                  1. 4

                    Smart constructors are definitely not in the “nobody uses it” category. They are one of the most pervasive patterns in strongly typed languages (especially ML descendants like Haskell or Scala).

                    1. 2

                      Smart constructors are just functions that build values of the required type, but perform some extra checks when the value is constructed…

                      It seems like you could employ the same smart constructor pattern in many languages. For the age example, you’d create a type for the valid age range and use this type elsewhere in your code:

                      class Age {
                          final int value;
                          Age(int value) {
                              if (value < 0 || value > 120) {
                                  ...raise exception
                              }
                              this.value = value;
                          }
                      }
                      

                      This is along the lines of cgenschwap’s recommendation of preferring parsing over verifying.

                      1. 1

                        You’d have to make sure the setters and getters did the checking as well along with making sure there was never any access to the internal value other than by the setters and getters. Which is a lot more faff than having it supported natively.

                  2. 7

                    Aren’t you just talking about dependent types? I don’t think this is a situation where languages “fail” per se, but more that it is a technically difficult thing to do (while also having a language that is easy to use for regular programmers/programs).

                    Dependent types are just an extension of types – so they are certainly a good solution to the actual problem!

                    1. 1

                      Dependent types is one way to do this, though so far I’ve never seen that built into a language and usually a very complicated way.

                      But who uses dependent types? no languages really have them built-in, certainly no commonly available/used languages. Haskell, has Liquid Haskell and per pushcx smart constructors also does this, apparently. Are Smart Constructors built-in? It seems like they are, but my Haskell on this machine won’t compile it, but it’s also a really old Haskell, so that could be why.

                      I agree bolting constraints onto our existing type system(s) is very complicated and messy.

                      I’ve never seen any code out in the wild that does anything like this.

                      We all know we can’t trust whatever the user gives us, and the giant list of security vulns just enforce the point, and yet basically no language in common use has any nice sane way to handle these sorts of issues.

                      1. 3

                        If dependent types interest you, the answer to “who uses dependent types” is idris

                        1. 2

                          It is unfortunate that few languages have dependent types – I completely agree with you here. However, putting constraints on user input isn’t really an issue in my opinion. You should always parse the info from the user rather than verify it.[1]

                          Raw user input is stored in a Raw{var} type (which can’t be trusted) and is parsed (with constraints) into a {var} which can be used without fear. Of course, this doesnt guarantee the data is valid – your code might still screw it up – but this concept can just be used every time the data is mutated.

                          Dependent types are fantastic because they turn this into a compile-time guarantee. Otherwise I don’t really see the benefit of having a language feature like this at runtime, it is very easy to do yourself.

                          [1] https://lexi-lambda.github.io/blog/2019/11/05/parse-don-t-validate/

                          1. 1

                            I think you and I are in complete agreement here about the end goal. I’ve read that post before, and while what they write is possible in Haskell, basically never used(from my very limited Haskell experience), in other languages it’s a giant PITA.

                            No popular JSON parser will let you add constraints to your parsing of JSON(that I’m aware of).. The most they will do is sort of let you say this must be an int64, or this must be a string. Obviously JSON is just one example here. I’m sure there is one or two very generic parsers that allow for constraints at parsing time, but I’m not aware of any in popular languages that make adding actual constraints easy, or even possible.

                            1. 1

                              Certainly with strong, static typing this is easier to enforce (functions only take the parsed version of input). However every language can do this, it just becomes a matter of code hygeine. If JSON parsers dont let you add constraints then you just add another parsing step which can apply constraints.

                              Sure this adds boilerplate and complexity, but I would argue that this is fairly easy to do.

                      2. 6

                        I’d argue that types are a terrible solution to the actual problem.

                        I’d argue the actual problem is, we need to check variables in our languages…

                        …we want age to be an integer between 0 and 120 or so. Certainly < 200. That’s what we actually want.

                        Let me make sure that I understand what you’re asserting here: you believe that there’s only value in type systems insofar as they can allow for constraining numeric types to a bounded range? And, all languages with static type systems which fail to do this are fundamentally failures?

                        1. 0

                          No, Types are awesome for compilers, to make things go fast and optimize their implementation. There is a reason types got invented in the first place. It’s hugely easier for a compiler to optimize number math if they don’t have to concern themselves with if it might also be a string “happy”.

                          I argue though that they are pretty terrible for end programmers, because they lack constraints. There is a reason Python and friends, who mostly ignore types are hugely popular.

                          I only picked age as a very easy, hard to dispute example, but I believe constraints should apply to all data types, not just numeric types. pay period date constraints on a timesheet would be another easy use-case that doesn’t use numbers, but dates.

                          PostgreSQL’s check syntax is what I’m after here, before anything can get stored in the table, it has to be verified for sanity. but PostgreSQL is the wrong place to do this, it needs to happen way out near the user, so it’s way, way easier to say “hey user, “first” is not a valid number in the range 0-100, since this is an input for age.” So when we go to store the variable in our program, we need to be able to parse it and constrain it and verify it’s sane before anything else can happen. We as an industry completely fail at this, for the most part.

                          1. 3

                            Yes and no. There is a lot of benefits to types, they help when writing code by pointing out bugs before the code is running (contrary to Python for example). Depending on the type model you even get theorems for free, i.e. you can prove theorems about functions just from it’s type signature! That’s pretty neat.

                            Another problem is the overly structured data you’re proposing: What if I’m 106 and want to register for your service? What if I don’t have a first name? What if I don’t have a street address and live “2 mi N then 3 mi W of Jennings, OK 74038”? What if, in a family tree program, a person wants to input a child which he had with his daughter?

                            I’m not saying no constraints is a better approach, but there are a lot of edge cases to be thought of, even for something as simple as an age or a name, which maybe shouldn’t be restricted at all.

                            1. 2

                              There are new things being added to types to make it better, I agree, dependent types one of them. Like the OP post says, many type systems are hard to reason about.

                              I agree gross errors are caught trying to shove a string into an int8 variable. But academic papers disagree over how useful types are in practice, it’s mostly just yelling opinions across the internet these days, as far as I can tell. Perhaps over time, academic papers will have better science involved and eventually figure it out, but I think we can all agree the answer , scientifically speaking, is murky at best[0]. That said proving theorems sounds pretty neat!

                              Of course there are lots of edge cases with data validation/parsing, the known issues here, are multitude. I don’t have a street address most of the time. That doesn’t mean we should punt and give up on the problem, and let everything be free-form text fields. :) It’s very, very hard to reason about free-form text fields.

                              Every application will likely need unique constraints around particular data, depending on the context, but I think sane defaults can be found for many use cases. In my OP I covered this already. We can argue where the limits need to be, but for most applications I think we can agree negative ages, and ages over 150[1] are probably sane defaults.

                              If you buy into the parse vs. validate debate[2], we can’t even currently parse with any sanity. OpenBSD mostly punts on sane parsers and just assumes they are totally broken by sandboxing the parsers from the rest of the application(sshd, tcpdump as examples). I also mentioned in a different comment about JSON parsers as an example.

                              0: http://danluu.com/empirical-pl/

                              1: https://en.wikipedia.org/wiki/Oldest_people

                              2: https://lexi-lambda.github.io/blog/2019/11/05/parse-don-t-validate

                        2. 5

                          Types, basically don’t do that, and practically every language ever written skips over any sane way to have limits on our variables besides basically int8, int16 and string.

                          I believe that Ada handles this in a good way. You can declare an age type that has a valid range of 0 .. 120. I don’t have direct knowledge of this, but AFAIK it uses a combination of static and dynamic checking. Those cases which are impossible to verify with a static checker are verified at runtime.

                          1. 3

                            Pascal and Common Lisp are two other languages with this feature, just for completeness. They’re called “subrange types” in Pascal.

                            1. 2

                              Yep, Ada can do this. You can also use a regular integer type with contracts and use Spark (the Ada subset) to prove that the integer is in the range you expect it to be, thus guaranteeing that your program is free from runtime exceptions.

                              Ada has some pretty cool features, it’s sad that nobody knows about them.

                            2. 4

                              You might find Racket’s contract system interesting. Also this talk if you have ~40 minutes (assuming 1.5x speed).

                              1. 1

                                Neat! So I agree in non-popular languages, this is sort of only recently being addressed, to some degree or other, with varying degrees of implementation. Most documentation ignores the problem. I’ve never used Racket, but Haskell is the other commonly known language that has this ability to some degree, yet I’ve never seen any Haskell code in production that uses any of the features available. Is using the contract system actively used in Racket?

                                I went looking through github, seems Pollen is popular for something written in racket, and it uses ‘provide’! [0]

                                It seems however, it’s limited to modules only.

                                0: https://github.com/mbutterick/pollen/search?q=provide&unscoped_q=provide&type=Code

                                1. 3

                                  Yes, the majority of Racket code uses contracts extensively and they are also used in documentation. Some examples:

                                  provide is just Racket’s way of exposing bindings from one module so that they can be required by another. The contract library provides the contract-out provide transformer that attaches contracts to bindings when they are provided. You’re right that when someone uses contract-out, then that contract will only be enforced at module boundaries. However, that’s not the only way to attach a contract to a value. The same library also provides define/contract among other things so you can do stuff like this within a single module:

                                  #lang racket
                                  
                                  (define smallint/c (integer-in 0 255))
                                  
                                  (define/contract (f x)
                                    (-> smallint/c smallint/c)
                                    x)
                                  
                                  (f 42)
                                  (f 1024)
                                  

                                  Running the above yields:

                                  42
                                  f: contract violation
                                    expected: (integer-in 0 255)
                                    given: 1024
                                    in: the 1st argument of
                                        (-> (integer-in 0 255) (integer-in 0 255))
                                    contract from: (function f)
                                    ...
                                  

                                  Or even stuff like:

                                  #lang racket
                                  
                                  (define smallint/c (integer-in 0 255))
                                  
                                  (define/contract (f x)
                                    (->i ([in smallint/c])
                                         [out (in) (=/c (add1 in))])
                                    x)
                                  
                                  (f 42)
                                  

                                  That yields:

                                  f: broke its own contract
                                    promised: (=/c 43)
                                    produced: 42
                                    in: the out result of
                                        (->i
                                         ((in (integer-in 0 255)))
                                         (out (in) (=/c (add1 in))))
                                    contract from: (function f)
                                    blaming: (function f)
                                     (assuming the contract is correct)
                                  

                                  It’s been a while since I’ve done any Haskell, but I don’t think there’s anything quite like this in the language. I definitely recommend watching the talk I linked to because it explains some of these ideas in a visual way and much better than I could do here.

                                  I believe Clojure is also adopting some of these ideas now via spec, but I haven’t looked into it.

                                  1. 1

                                    <3 Thanks!! This looks very awesome! Go Racket!

                                    1. 1

                                      <3 Thanks!! This looks very awesome! Go Racket!

                                2. 2

                                  I believe you’re looking for dependent types as in eg Idris: https://en.wikipedia.org/wiki/Dependent_type