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

                        1. 2

                          Resurrecting a 2013 angular, nodejs, mongo, elasticsearch side project. Skipping forward so many versions has been messy. I’m now starting to move it to elixir, cockroach, elasticsearch, not sure about the client side as I haven’t touched any since that angular.

                          1. 1

                            Any thoughts on the effects of auto-complete on the developer? Eg faster typing, but less familiarity with the language because of reduced memory effort.

                            1. 4

                              In my experience it mostly saves the time that I’d usually spend going to the documentation website, finding the type that I need and scrolling through the methods to find the one that I want – I usually remember the “it’s in there somewhere” part but not the name. Autocompletion is a huge timesaver. I don’t feel like it’s a different learning experience, the end result is pretty much the same.

                              1. 3

                                For me, ide features are not about time, they are about flow. In an IDE, I am writing a depth first search, in a bare text editor, I am fixing the text of my code to conform to the actual syntax of the language.

                              1. 3

                                Letsencrypt were recently bitten by range - repeatedly processing the first item, not moving to the next. That’s not an obscure quirk, it’s pretty much Go 101, and yet it still happens.

                                1. 2

                                  Why not just go back to all logic in database Stored Procedures? Have we as software developers learned nothing?

                                  1. 1

                                    Yes, I’m not sure there’s much new here. Maybe if coming from a less capable db?

                                  1. 4

                                    And instead of Go try Nim.

                                    1. 6

                                      Aside: I will never get used to the “POS” initialism meaning anything other than “piece of shit”.

                                      1. 2

                                        I also have the problem with piece of crap.

                                        1. 2

                                          You bet retail workers say it all the time, too. Probably slip out in front of bosses or customers on occasion.

                                        1. 1

                                          I keep looking at these. They’re only sold online for Londoners so I haven’t been able to try one. If anyone could describe the feel of the keyboard, compared to an Xps13 or Macbook 2014 I’d be really grateful!

                                          1. 2

                                            OCaml could do with a CI site. Circle and travis can do it but it requires a hell of a lot more effort than explicitly supported languages. Inria has a CI site, iirc https://ci.inria.fr/ but when last I looked was for Inria people only.

                                            1. 3

                                              For upstream repositories, people normally seem to use Travis or AppVeyor (for Windows), using the scripts at https://github.com/ocaml/ocaml-ci-scripts.

                                              Another option is to provide a Dockerfile and then configure Travis to build that (e.g. https://github.com/mirage/capnp-rpc/blob/master/.travis.yml). That also means you can test the build locally easily and get the same result as the CI.

                                              For opam-repository, there are various CIs, e.g. http://check.ocamllabs.io/ shows the status of every version of every package in the repository against each version of the compiler.

                                            1. 5

                                              Org mode is amazing and is the one thing I really miss about emacs. I love emacs but don’t particularly have a knack for coding in Lisp so it’s not my mainstay but Org mode is superlative.

                                              It’s easily one of the best and most extensible outliners I’ve ever encountered on any platform. I keep hoping someone will build Org mode like extensions into VSCode or something, or maybe Neovim :)

                                              1. 3

                                                It’s the opposite with me. I never found that Org mode helped me that much - I prefer writing outlines on real paper in real notebooks. It’s the lisp power which drew me to, and keeps me coming back to, emacs :)

                                                1. 5

                                                  Nice. Being partially blind with fine & gross motor impairment, handwriting is a bit of a novelty. I can do it, but in order for it to actually be readable later it’s a tremendous outlay of time and effort.

                                                  1. 3

                                                    Ah, well I guess that org mode is significantly better option then.

                                                2. 2

                                                  I haven’t used org mode, but was a big vimotl user. When I switched primarily to vscode, I found the Todo+ plugin which had most of what I liked from vimotl.

                                                  1. 2

                                                    I’ll check them both out, thanks!

                                                    Most of what I liked about Org mode was not to use it as a task tracker but as an outliner in the old fashioned sense of the word - a way to crystallize thought by writing outlines for things and being able to have the bullets be super malleable and re-arrangable without having to retype. org mode is fantastic at this.

                                                  2. 1

                                                    I kinda like vimwiki these days, plus calendar-vim and I get a decent journaling + personal wiki.

                                                    I’m using task warrior for todo lists, another fine text-based tool but I’m a little bit annoyed by the fragmentation when Org mode could do it all…

                                                    1. 1

                                                      I will check vimwiki, but does it offer outlining support with re-arrangable bullets? That’s what I value most in org mode.

                                                      1. 1

                                                        I use the same - vimwiki and task warrior. I used to use Org mode but felt there was insufficient return on using another tool, found vimwiki. I started using task warrior because todo lists in my vimwiki seem to both grow endlessly and breed. I’ve concluded I’m a bit of a mess and no tool will cope with me. Optimistically, I’m having a tentative poke at tiddlywiki, but don’t yet see the point over vimwiki.

                                                    1. 7

                                                      Not sure this is really “intermediate” as it still seems beginnerish, but still important things for any Vim user to get used to. I think intermediate Vim would be more about how to improve usage of makeprg, quickfix, jumplist, netrw, etc.

                                                      1. 2

                                                        I have been using vim for a while, and have no idea about the things in your list. I guess I have some reading to do

                                                        1. 2

                                                          I have to agree. I’d consider these bare minimum, without knowing which I don’t know how or why you’d be using vim. I’d forgotten about quickfix!

                                                        1. 5

                                                          I’m going to try some writing: yesterday afternoon I managed to rewrite the entire interpreter for my toy language in about 150 lines of Scheme, so I think I’ll try to turn it into some kind of walkthrough article as an exercise.

                                                          The current interpreter is around 5K-8K lines of Rust written over several months, not counting the half-decade of previous failed attempts. Ah well.

                                                          1. 3

                                                            not counting the half-decade of previous failed attempts – I can’t tell tell you how comforting this is as I try to squeeze writing a language into my lunch breaks, and it feels like it’s been going on for a long, long time.