1. 47
  1. 15

    There are often these articles that attempt to create a mystique for Lisp. They should be take in context. 25 years ago Lisp was filled with ideas that didn’t exist in a lot of other languages. Perl and Python borrowed ideas from it which lead to many people being exposed to dynamically typed languages where you can do functional style programming.

    The only point in this article that is unique to Lisp is s-expressions.

    The section “Dynamically Typed” is not well informed. It gives a flavor of the time where type systems didn’t deliver much on their promises and the feelings of distrust that inspired.

    If you use Python and work with generators, functools, itertools, async, decorators, duck typing, PEP 484 types, contextlib, werkzeug debugger and I guess lists, dicts and objects, you have seen a lot of the parts of Lisp that got people excited 25 years ago. None of the long time Lispers are going gaga over these features but you don’t need to feel like you are missing out on the mystique of Lisp.

    A Lisp is a valid choice if you want to broaden your exposure to different ideas but it’s 2021 and there are a lot of interesting things going on.

    1. 7

      The best any static type checking will let you do is array[float]

      Can’t Idiris at least do the “Monotonically Increasing Float” part?

      1. 9

        It can do the whole thing, because the dependent type system is capable of end-to-end formal verification. Any FM coding language can verify properties statically, even if it’s not in the type system, so you can do this in HOL4, SPARK, Dafny, etc. It’s just balls-hard (because formal verification is balls-hard in principle).

        1. 12

          It can do the whole thing, because the dependent type system is capable of end-to-end formal verification.

          This effectively moves the complexity of expressing your invariants from one place (like tests) to another (a type system extensible by arbitrary code).

          Type systems only feel magical as long as they stay simple and declarative. Which necessarily keeps them limited.

          1. 3

            Type systems only feel magical as long as they stay simple and declarative.

            I wholeheartedly agree with this statement, but I doubt you’ll find any pair of programmers that agree on what’s simple and declarative. I bet if you asked around, you’d find that any point in the entire spectrum will be picked by someone as the sweet spot.

          2. 2

            Last I checked most of these end-to-end FV attempts require a lot of human intervention (i.e. a human has to prove the properties and encode it in the coding language). Has that changed?

            1. 10

              Nope, still sucks and I still hate it

              (It’s gotten better in the past 6 years as people got better at SMTing all the things, but you still need a lot of human intervention to get anything interesting verified)

              1. 1

                Lean has some cool machine-assisted tactics like suggest and library_search that will offer help to find a theorem or proposition that will complete a proof, but these are pretty brute and still often require a lot of work. They’re hit-or-miss but when they hit it’s like magic.

          3. 9

            Every half-serious statically typed language can create new types kilometers and miles from float. Then you won’t confuse array[kilometers] and array[miles] and possibly prevent $330 million dollars from being almost totally wasted (https://en.wikipedia.org/wiki/Mars_Climate_Orbiter).

            That’s quite a bit better than array[float]. And you don’t need to use a research language to do it, either.

            1. 3

              Mars climate orbiter is a good example of why the phrase ’‘should be caught in testing” is not sufficient justification for not using additional checks and fail-safes. I assume NASA LM’s testing regimes are fairly rigorous (correct me if there is evidence to the contrary) but in some applications you need another layer of checking. Having said that I also assume that the software in question did have a type system, and it simply wasn’t used in the way you describe.

              1. 14

                The type system couldn’t help in this case: the data in US units (pound-seconds) which should have been in metric units (Newton-seconds) was read from a file on disk. The software reading the data from that file thought it was metric, but it wasn’t. Perhaps the file format should have included the units? But the file format as specified was only ever supposed to contain Newton-seconds, so why would they include the units?

                Anyway, it was an interface problem, rather than a type system problem. See Mars Climate Orbiter Mishap Investigation Board Phase I Report

                1. 3

                  In a way, the interface problem was a type system problem, but perhaps one we aren’t well equipped to solve across systems.

                  One could imagine attaching typed schemas to certain files, and writing language bindings that enforced that stored values must be strongly typed, with explicit units.

                  1. 3

                    Seems like modern type systems don’t solve this problem as c– mentioned. It is certainly true that no error checking method is 100% foolproof. My main point above was merely that testing isn’t either, and having multiple independent error checking systems is a good idea. Type systems are useful but should not be relied upon.

                    1. 1

                      Absolutely. It even goes beyond merely having multiple independent error checking systems: you have to have the processes, or organizational culture, in place to act accordingly. It’s interesting that the Mars Climate Orbiter problem was actually detected multiple times before the disaster occurred, but no-one quite took it seriously enough.

            2. 3

              This misses the payoff of things like type-classes, where you can get the language to provide implementations of all sorts of things. A simple example is deriving lexicographic ordering for tuples if the type of each member is ordered. As much as I enjoy editing in a sexp-aware editor, the idea that static types only constrain you is very outdated thinking.

              1. 2

                Even dispensing with sophisticated types, having a smart constructor that might fail at runtime but on success returns a wrapper type which guarantees it’s an “array of numbers with a mean value of such and such and a standard deviation of such and such” can help avoid many mistakes.

              2. 8

                Refreshing to read some one challenging the value of type systems. But he is right. They are way overrated. A nicety certainly won’t determine the quality outcome of a product written in a given language.


                What improves (and guarantees) software quality is rigorous testing. To deliver high-quality software, there is no other solution.

                This could be equally challengee and the author even hints before that the fundamental quality of a program is not tied to such gimmicks.

                What determines the quality of a program is the engineering skill of the programmer. Throwing testst at it is no guarantee for anything. Plenty of hopeless codebases have thousands of tests.

                1. 1

                  What determines the quality of a program is the engineering skill of the programmer. Throwing testst at it is no guarantee for anything.

                  Hang on; please expand on this. I’m not seeing how a test that has assert(exactly_this) does not give you strong confidence that exactly_this is true (for the setup/context in the test code).

                  1. 1

                    I didn’t negate that. You obviously can’t create asserts that will give you confidence on all cases because at then point you could replace your code by a giant map.

                    Furthermore exactly_this is a value or a condition. It doesn’t asset anything at all about how the code is engineered. You can have an horribly written program and an code marvel passing the very same battery of tests.

                2. 4

                  There was an attempt.

                  But after this:

                  This is where I call bullsh*t. I have never had a static type checker (regardless of how sophisticated it is) help me prevent anything more than an obvious error (which should be caught in testing anyway). What static type checkers do, however, is get in my way. Always. Without fail.

                  Discourage himself.

                  And all this brag, what s-expressions is only trees. What about: [ ] ‘ # : ?

                  1. 9

                    Honestly, if a type checker gets in your way either the type checker is too simple or you have an attitude problem. Sometimes both

                    1. 4

                      Or you are doing something really, really weird.

                      1. 2

                        I have a question for you or anyone else interested. I’m not a type-system skeptic… I cut my teeth on Ocaml and Haskell as a language hobbyist. Lately I’ve been using more Python and I’ve been wondering how to get a specific function to compile. In dynamically typed languages it’s actually very common to come across a very generic “find” function over lists which takes an object to look for, the list, and optionally takes a key function (which produces the comparison object from each item in the list) and a test function (which defaults to the equality operator). This is really handy because the less names I have to learn (i.e. both find and findBy), the better. Naturally I wanted to see if I could do this in a statically typed language (without dependent types… those are hard for me. I know you’re the formal methods guy around here but forgive me for being recalcitrant about learning new tools).

                        I like OCaml, so I took a crack at it in OCaml but can’t get it to be as polymorphic as I want it to be. Here’s a simple version.

                        let rec find (o : 'b) (xs : 'a list) (key : ('a -> 'b) option) (test : ('a -> 'a -> 'bool) option) =
                          match xs with
                          | [] -> None
                          | x :: rest ->
                            match key, test with
                            | Some(k), Some(t) ->
                                if (t o (k x)) then (Some x)
                                else find o rest (Some k) (Some t)
                            | Some(k), None ->
                                if (o = (k x)) then (Some x)
                                else find o rest (Some k) None
                            | None, Some(t) ->
                                if (t o x) then (Some x)
                                else find o rest None (Some t)
                            | None, None ->
                                if (o = x) then (Some x)
                                else find o rest None None

                        I’d like to be able to call this like find 2 ["my"; "name"; "is"; "kris"] (Some String.length) (Some (=)). Unfortunately Ocaml gives me back val find : 'a -> 'a list -> ('a -> 'a) option -> ('a -> 'a -> bool) option -> 'a option = <fun> It’s been a while since I worked through a Hindley-Milner example but I think this is the correct refinement because: what if the needle and the haystack items are differently typed, but there’s no key or test function? The default is structural equality, which is 'a -> 'a -> bool, so it follows that the needle must always have type 'a. I tried a few different things, like breaking the match arms into different functions, but I’m not sure what to do. One thing I haven’t tried yet is trying this in Rust and using the Any trait. Specifically, how can I, or what is the closest I can get to, have one function I can call to do all the different kinds of list searching that I want to do?

                        I don’t think this is “weird”. In general there are a lot of examples that make command line interfaces, dynamic languages, etc. feel so ergonomic, and it’s also why I feel like the answer might lie in dependent types: there are a lot of times where a function or verb is parameterized by the types of the arguments or the way that you call it. I suspect a hypothetical language that supports overloading by keyword argument would suffice for this example but there are other examples I have where there’s a similar tradeoff between completeness and ergonomics. But furthermore, this isn’t really an ad-hoc polymorphism example, because I can write a single definition in dynamic languages. Something like

                        find (o, xs, key=None, test=None):
                            if len(xs) == 0: return None
                                x = xs[0]
                                if key: x = key(x)
                                t = default_equality
                                if (test): t = test
                                if test(o, x): return x
                                else: return find(o, x[1:], key, test)
                        1. 4

                          Specifically, how can I, or what is the closest I can get to, have one function I can call to do all the different kinds of list searching that I want to do?

                          Have a find function that takes a predicate for an item, and call it with different predicates. This is how List.find already works in Base: depending on how you call it, you can search for a needle in a haystack:

                          List.find haystack ~f:(My_type.(=) needle)

                          You can search for some nested key, of a different type:

                          List.find haystack ~f:(fun x -> Other_type.(=) x.key needle)

                          You can find something using something other than equality:

                          List.find haystack ~f:(fun x -> Shape.fits_inside x.hole shape)

                          I get what you’re asking, though. I don’t mean this to be snarky or annoying, just to say that this isn’t… the thing that works well in Python doesn’t really work well here.

                          I think one difficulty is that you’re using the polymorphic equality function, which is… basically shouldn’t really exist. It has surprising (illogical) behavior in the face of any nontrivial abstract type; it will throw exceptions if you pass it certain types of objects; it just shouldn’t exist.

                          So let’s pretend that we have no polymorphic equality. Then how do you write that function?

                          Well, now you need to pass an explicit comparator. Basically, make test a required argument. Okay; no problem. You wind up with a signature like this:

                          let find (needle : 'a) (haystack : 'a list) ?(key : ('a -> 'b)) (test : ('b -> 'b -> 'bool)) = ...

                          I’m making key a named optional argument instead of an explicit positional option because that’s more stylistically natural, but it’s equivalent here.

                          But what’s the default value of key? Easy: the identity function. We want it to default to Fn.id if it’s not provided explicitly.

                          Except… that doesn’t typecheck. That doesn’t actually make sense. Fn.id isn’t 'a -> 'b; it’s 'a -> 'a. This makes sense if my test predicate expects an 'a, but the type signature says right there that it accepts a 'b. What if I call it with a differently typed test, but don’t provide a key argument?

                          You kind of want to say “you can’t do that.” In other words, make key required when test has a different type, and allow it to be optional when test doesn’t. But you can’t express that – you can’t decide that an argument is optional or not, based on the type of the function passed to test.

                          And you know all this, which is why you’re bringing up dependent types. Can they let you determine, at runtime, whether this argument is optional or not?

                          Well, not in OCaml. But in some other type system? Sure! Dependent types wouldn’t even be necessary: just moving the type-checking of the defaulted arguments to each callsite would get you the behavior you want (you’d have to use actual optional arguments, instead of defaulting them in a match statement in the function body, but whatever).

                          You can express the behavior you want in OCaml; you can construct predicates like this dynamically at runtime – but just not using optional arguments and a single function call. There are other ways to do it; heck, as soon as you make key a required argument, you have done it – callsites can typecheck whether Fn.id is valid for each individual invocation of your function. But that’s not the API you want.

                          I think this is an interesting illustration of a point the original author of this post was trying to make: why is the type system getting in my way like this? After all, Python lets you have the API you want. Why doesn’t OCaml?

                          Well, this example makes just as little sense in Python as it does in OCaml. Python just allows programs that use the “wrong” types. Want to compare a string and an int? Go ahead. False, I guess? Hope that was what you wanted; hope you meant to compare a string and an int. The Python function works if you use it right – if o is the same type that test expects, etc. But OCaml wants to ensure that all possible uses of the function are valid. It doesn’t want you to say “there is a right way to call this function,” it wants to say “all ways you can call this function are valid.”

                          These are very different goals! There are some contexts where you want that extra assurance, and some where you don’t. Depends on what you’re doing. (Er, sorry – what I meant to say was “static typing is pointless.”)

                          I have run into this probably before (specifically the “I want an optional argument to transform this value that defaults to the identity function”), and it’s annoying. I wish I could express that; I wish I could hold the compiler and soothe it and explain to it that it’s going to be okay. But instead I just make it a required argument and move on.

                          But in this case, you don’t even need to do that. The canonical OCaml way to do this is simpler and more flexible than the function you’re trying to write. You say you don’t think your function is “weird,” but it does look weird to me: why write this very specifically-shaped find function instead of the far more general one that lets you pass any predicate you want?

                          List.find haystack ~f:(My_type.(=) needle)

                          The key example you want where the needle is the same type as elements in the list and you still want to compare it can be accomplished with the not-very-well-named Comparable.lift:

                          List.find haystack ~f:(Comparable.lift Identifier.(=) ~f:(fun x -> x.id) needle)

                          It’s verbose and kinda ugly, but OCaml is a verbose and kinda ugly language :)

                          Last thing: you say you want a single function to do everything so you don’t have to remember which function to use. But why is find special? What if you want to, say, filter a list next? Do you have a filter function that takes these same optional arguments?

                          By breaking out the functions that construct these predicates from the functions that use the predicates, you end up with a (subjectively!) simpler program with less to think about. Find takes a predicate. Filter takes a predicate. Partially applying a comparator will get you a predicate. Comparable.lift is one way to compose comparators. String these together, and now any function that takes a predicate gets this compare-on-a-key function; you don’t need to go in and add these optional arguments to every function you want to call.

                          Okay I’m just rambling now and I have an undefined-is-not-a-function exception to track down so I’ll go now.

                          1. 2

                            I’m not an OCaml expert but I probably wouldn’t introduce option types into this signature. Your key and test parameters have reasonable “default” implementation that are as convenient as typing None or Some:

                            let rec find (o : 'b) (xs : 'a list) (k : ('a -> 'b)) (t : ('b -> 'b -> 'bool)) =
                              match xs with
                              | [] -> None
                              | x :: rest ->
                              if (t o (k x)) then (Some x)
                              else find o rest k t
                            let itself x = x ;;
                            let always x _ _ = x ;;
                            find 2 ["my"; "name"; "is"; "kris"] String.length (=);;
                            find "my" ["my"; "name"; "is"; "kris"] itself (always true);;
                            1. 1

                              I presented a simplified problem. The arguments are optional because I wanted to use optional arguments in OCaml so that I didn’t have to always provide a key or test function (the typical case). Furthermore the find function might take an arbitrarily large number of options, like fromEnd, so even though two optional arguments are simple enough to write explicitly, it would get unwieldy for more. Obviously the more power you give a function the less likely it is to be able to find a single signature for it. You can easily take this too far to the point of making a function with uselessly large surface area but I think there’s a grey area where a function is conceptually small enough to be useful and ergonomic for a lot of people but way too large to be statically typed.

                              1. 3

                                Well, you asked “Specifically, how can I [do the above]” and both I and ianthehenry gave pretty specific examples :)

                                I do agree with ianthehenry that it sounds like you want OCaml to be more like Python but there are some fundamental language design choices which mean that Python can do some “unsound” things that OCaml just won’t allow.

                                I think I get what you mean referring to large number of optional parameters. This seems to be a common pattern in Python, especially in the popular scientific and ML library APIs. sklearn.svm.SVR as an example has 11 options, and that’s not even a lot in comparison to other sklearn functions!

                                That sklearn API has more design issues than just having “too many” parameters. Two of those options are only valid when combined with certain choices for another option. Although this is documented, the language does nothing to help prevent usage mistakes here. Some of the options specify that they must be positive real numbers, which is a case where a stronger, dependent type system might come in handy.

                                Human errors in setting up complex options like this are common, and stupid mistakes like that are easy to make. This sort of bug is often much more subtle and pernicious than an error in logic. How will I know what will happen if I try to fit an SVR while invalidating some of those documented constraints? At a quick glance in the Python code, there’s no obvious runtime checking either, so who knows! How could unit testing solve this problem? Furthermore, why should the burden of testing be passed off to us end users, when we didn’t design this API?

                                But in a typed language this API would probably should be designed differently from the start. I would imagine some sort of Builder pattern might be appropriate, as it is well known as an alternative to having lots of constructor parameters. (Again, I’m not an OCaml expert so I don’t know the idiomatic forms.)

                                The typed language design tenets say to “make illegal program states unrepresentable.” That does mean that typed API design requires some more effort, to carefully model parameter variants rather than dumping a bunch of defaults into the function signature. In exchange for the cost of design, you get to make certain guarantees to your clients. This is what the typing proponents mean when they say typing “eliminates a whole class of bugs.”

                          2. 1

                            Thing is that I’m always doing something really really weird when I’m between states of working code, i.e. when I’m doing anything that I cannot instantly get right. I find that being in that dark zone is usually more fun and efficient with a less restricting language. A less restricting language kinda tries to work with me during the journey, but a stricter language just goes “dude, where the fuck are you even going?”

                            1. 1

                              I’d love to see an example of a language working with you here. I’ll admit my primary dynamic typing experience is Ruby where doing something invalid immediately results in an exception and (usually) a crash.

                              1. 1

                                Perhaps I’m thinking via negative examples when working with languages like Rust or Haskell. If I do something weird there, I just get an entirely unhelpful type error.

                          3. 4

                            Having worked in Haskell and Rust, I’ve definitely had the type checker get in the way. I mean pages of Haskell community questions are filled with people asking how to chain operations through lenses or questions about how to lift one monad into another. When you work enough in Haskell, it comes naturally as you’re holding the types (e.g. monad transformer stacks, or free monads) in your head, but let’s not forget that if you were coding in a language that doesn’t require this type-level specificity, that you wouldn’t need to do any of this.

                            I presume (though the author does little more than rant about this so I’m being charitable here lol) that the author’s position is that the contortions necessary to satisfy the type checker in cases where behavior is well understood is too high, and that guards/assertions/contracts around tricky parts of your code offer much of the same benefits as types without forcing the contortions around all of your code. I’m not sure how to test the veracity of either side of this claim, but I do think it has merit, having had to spend more time than I’d like building up State monads and lifting results out.

                            FWIW I still largely think this is a neurotype thing. I suspect folks who find abstractions easy/empowering will have little trouble juggling abstractions in their head and will prefer to use that rather than think about weird/silly edge cases. I suspect other folks prefer focusing on a more concrete approach in their code, and these folks will lean on things like contracts, property testing, and regular old unit testing for assurance. sqlite certainly offers us a window into what the latter approach could look like. I don’t really have the data to back up my thoughts on the matter though so I’m idly speculating as much as everyone else 🤷.

                            1. 3

                              Monad transformer stacks (besides being an advanced feature most code doesn’t need) aren’t a type system thing, if you want the same behaviour in a unityped language you’d need very similar machinery. Free monads are a cool technique, but same thing. I don’t use lenses often (and avoid lens especially) but maybe they are poorly enough set up that the type system fights you, I couldn’t say.

                              In general I find that if the compiler says I’m wrong, it is I who is wrong. The idea that “oh, this code would work but the dang type system won’t take it” is the thing I just can’t see. Sure, if you’re using advancing tools you need to understand the tools, but if you took away the type system all the compile errors would become equivalent runtime crashes. You’re not fighting the types usually, at most fighting yourself / your understanding of the tool. I definitely wouldn’t suggest most new Haskellers use monad transformer stacks (and only occasionally transformers at all… maybe ExceptT) or lenses, just as I wouldn’t suggest a new Rubyist reach straight for refinements or metaprogramming or a new rust programmer use Rc or RefCell

                              1. 3


                                This continues to be one of the most smug and contemptuous ways people refer to dynamic typing. Not as bad as “unethical” but up there

                                1. 2

                                  How is it smug or contemptuous? I’m a Rubyist and have nothing against dynamic typing or anything like that.

                                2. 1

                                  Monad transformer stacks (besides being an advanced feature most code doesn’t need) aren’t a type system thing, if you want the same behaviour in a unityped language you’d need very similar machinery. Free monads are a cool technique, but same thing.

                                  Hm. I feel that there aren’t many benefits to using an ML type system if I can’t layer guarantees with a monad transformer stack or a free monad approach. Without those, I feel like I’m just working with any other somewhat strong type system. I may be throwing out the baby for the bathwater here since I haven’t used more “relaxed” languages like Ocaml or SML, mostly spending time in Haskell.

                                  In general I find that if the compiler says I’m wrong, it is I who is wrong.

                                  Sure and I don’t think that’s what TFA is talking about. I think TFA is saying that, the cost the author pays for using an ML-style type system is too high in instances of simple and clear logic to justify the benefits that it offers when the compiler tells you you’re wrong. This is a more complicated value tradeoff and I think it largely depends on the person. Knuth is famous for advocating to write prose to accompany logic in order, so the reader of code follows along as one does a math textbook and I presume this allows Knuth to keep the bugs in his code very low.

                                  1. 2

                                    I may be throwing out the baby for the bathwater here since I haven’t used more “relaxed” languages like Ocaml or SML, mostly spending time in Haskell.

                                    Me too. I’ve played with SML and done some rust and swift, but mostly I use Haskell.

                                    the cost the author pays for using an ML-style type system is too high in instances of simple and clear logic

                                    Right, whereas I find for those cases (in Haskell anyway) I don’t need to even write any types at all. I just write the code as I would in Ruby (in ref to types, obviously syntax and approach will differ a bit) and that’s it. Types get inferred and if I make a typo or logic error I get a message when I run it with runhaskell just like I would when running the equivalent ruby script with ruby.

                                    Anyway, I think maybe the issue is that it’s hard to discuss this in the abstract. Might be more constructive in the context of a particular fight someone is having, which is really a topic for pairing and not a forum, unfortunately.