Hacker News Reader

Exactly. Almost any error can be a type error with a sufficiently expressive type system, because a type system is just a way to mechanically prove things about your code. A more expressive type system lets you prove more useful things.

Of course, you can easily do things in a dynamic language that are observably correct, but which are very difficult to prove correct without advanced logic (i.e., an expressive type system). And more advanced type systems typically lose some nice ergonomic properties of simpler type systems, such as clear error messages, type inference, principal types, or decidability. So I can definitely see how someone moving for example from Java to Python would find the latter very liberating at first.

On the other hand, you can argue that people shouldn’t be writing code that’s so difficult to prove things about in the first place. :)

To my mind, the benefit of static types is that they allow proving properties of your code, but the cost is that they may force you to do so; the benefit of dynamic types is that they don’t force you, but the cost is that they don’t allow it.

On balance I think static types are therefore preferable, because you can always fall back to dynamic types (strings/hashes/variants/sums) in a static language, but you can’t “fall forward” to static types in a dynamic language.

With things like typescript or mypy in python you fall the other way around with types in dynamic languages. You can do it if you really want (optional but recommended for large projects). So Python and typescript have a nice sweet spot between static and dynamic if you want.

> ...the cost is that they don’t allow it.

Saying they don't allow it is too strong (they allow it, but it might be harder).

You can’t prove even very simple universal properties of dynamically typed code, such as “when given an integer, this function always returns an integer”, because its result type can depend on the value of the integer passed in at runtime. You can only prove existential properties (“there are integers for which this function returns an integer”) through testing.

That testing can be done before runtime in some languages, e.g., with Perl’s BEGIN/UNITCHECK/CHECK/INIT blocks. But it’s not really the same.

In a referentially transparent, statically typed language, if you give me a function of type ∀a. a → a, then I know for a fact that if this function halts, it must be the identity function. The only thing it can do is return its input.

The same function in a dynamically typed language could return any value of any type, because its result’s type can depend on both the type and the runtime value of its input, or not depend on its input at all, even if it’s referentially transparent.

Even if you supply that type annotation and check it at runtime (“this function returns a value of the same type as its input”), it would only be checking a single code path, and it could still give me any value. That is, a valid implementation would be “return 3”—I wouldn’t get a type error if I only ever called it on integers, but it would still be non-parametric.

"when given an integer, this function always returns an integer"

    (defun foo (x)
      (declare (integer x))
      (round (/ x)))

    (describe #'foo)

Derived type:

    (function (integer) (values integer rational &optional))

When given an integer, the function returns an integer, as well as an additional rational value. ROUND's specification says the type of the remainder is a REAL, but since I call it with integer, it is more precisely a RATIONAL (a subtype of REAL).

    (foo 0)
    => arithmetic error DIVISION-BY-ZERO signalled

Note, the meaning of the derived type is: if the code returns a value, then its type is .... The same applies in OCaml, where you can raise exceptions.

Let's restrict the input domain to non-zero integers:

    (defun foo (x)
      (declare (type (or (integer 1 *)
                         (integer * -1)) x))
      (round (/ x)))

    (describe #'foo)

    Derived type:

    (function ((or (integer 1) (integer * -1)))
              (values (integer -1 1) (rational -2 2) &optional))

The primary return value is an integer between -1 and 1; the remainder is a rational between -2 and 2 (ranges are inclusive).

Cool—Common Lisp? Isn’t that a promise to the compiler that you will obey the type, not a request to the compiler to enforce that you do? And can it correctly enforce something like the (∀a. a → a) that I described?

I consider gradual typing (e.g. Typed Racket, Hack) an interesting case of static typing where you’re trying to provide good interop with your dynamically typed surroundings, typically while migrating from dynamic to static types. Not all dynamically typed systems that allow type annotations have “gradual typing” in that sense, because many of them don’t give you enough power to get to “fully annotated” code (where the compiler is finally free to erase types completely).

Yes, SBCL, where declarations are treated as assertions (before you reach it, you must prove it or test it, after the declaration you can assume it).

No, (∀a. a → a) is not easily expressible (unless you write your own DSL).

That's right; those are promises to the compiler whose main use case is local "hotspot" optimizations. Those promises can be used as checking assertions in safe code; they become dangerous if code is optimized with safety 0.

You'd work around not being able to express (∀a. a → a) by focusing on the specific use scenario in the optimized code where that function is being called, and the concrete types that are involved. The identity function fits this type. If we know that x is fixnum, we can do this: (the fixnum (identity x)). Using the, we an assert types of individual forms.

Which is not to say that an implementation cannot do type inference for (identity x) and represent it type as (∀a. a → a) ; it's just that type inference is a separate thing from the ANSI CL declaration system.

Every time i hear some person complain about dynamic typing as if it was a world filled with pitfalls and dangers, I think in Common Lisp and how great is its dynamic type system.

Good example.

> You can’t prove even very simple universal properties of dynamically typed code, such as “when given an integer, this function always returns an integer”

Really?

Straight from my common lisp (SBCL) command line:

    CL-USER> (defun myfunction (x) (atanh x))
    MYFUNCTION
    
    CL-USER> (describe #'myfunction)
    
    #<FUNCTION MYFUNCTION>
      [compiled function]

    Lambda-list: (X)
    Derived type: (FUNCTION (T)
                   (VALUES
                    (OR (SINGLE-FLOAT -1.0 1.0) (DOUBLE-FLOAT -1.0d0 1.0d0)
                        (COMPLEX SINGLE-FLOAT) (COMPLEX DOUBLE-FLOAT))
                    &OPTIONAL))
    Source form:
      (SB-INT:NAMED-LAMBDA MYFUNCTION
          (X)
        (BLOCK MYFUNCTION (ATANH X)))
    ; No value
    
    CL-USER>

What happened here? I defined a function, i never declared which type does the function use, but the compiler can infer all the types.

If i supply a string to "myfunction", the compiler will complain. Typing is strong, but it's dynamic.

What will atanh return?

    CL-USER> (describe #'atanh)
    #<FUNCTION ATANH>
      [compiled function]

    Lambda-list: (NUMBER)
    Declared type: (FUNCTION (NUMBER)
                    (VALUES
                     (OR SINGLE-FLOAT DOUBLE-FLOAT (COMPLEX SINGLE-FLOAT)
                         (COMPLEX DOUBLE-FLOAT))
                     &OPTIONAL))
    Derived type: (FUNCTION (T) *)
    Documentation:
      Return the hyperbolic arc tangent of NUMBER.
    Known attributes: foldable, flushable, unsafely-flushable, movable, recursive
    Source file: SYS:SRC;CODE;IRRAT.LISP
    ; No value
    CL-USER>

The wonders of CL... not only i get all the possible input types, but also the return types. And the documentation, and the source code file(!)

Also: tests don't prove the absence of errors, only their presence.

Static types prove the absence of some errors.

Any type snob will tell you that even in supposedly good type systems, without dependent types, all lists are dynamic! Yet most of us that swear by static types don't use dependent types (much). There might be a limit where "more types" don't pay off their added cost relative to the thinking and typing needed and the security gained. Where that limit is depends on the application. Formally verified programs aren't used for many simple web backends - for good reason.

Also, type systems aren't equal. There are decent dynamic ones and terrible ones. Same goes for static type systems.

As for dependent types, it's probably just that the type systems for them are simply not yet mature enough to be practical for most tasks.

If you're using a dependently typed language, you have to write maths proofs to prove properties hold. It's incredibly challenging and not going to be automated any time soon.

I think that's going to change. It's my completely biased, uninformed opinion that dependently typed systems are much easier to reason about than their counterparts.

> In the end, dynamic typing is just a way to make runtimes slow and building correct programs slower, in exchange for some entirely subjective aesthetic or ergonomic quality.

To be honest, I really don't understand what the benefit of dynamic types are supposed to be. People say it's easier and less hassle to get something up and running because you don't need type annotations but this isn't an issue with decent type inference and all you're doing is replacing compile time checks with runtime crashes.

I still feel there's a correlation between Python coding bootcamp survivors and the new wave of people thinking static typing is hard. It makes it easier if you know what you're doing.

There are also people with 10+ years of using static typing languages like Java or C++, that then go to Python or Lisp or Racket and find out they are more productive with dynamic typing, while writing even more readable code than before.

Yes, everything can be a type error (security, memory management, concurrency (deadlocks), ...). You define properties about the code and you can check them either at runtime, or statically. If I choose to write in OCaml, the memory management is done with a GC, which relies on dynamically typed memory; but I write in Rust, there is no GC but a kind of static analysis for managing ownership; both approaches work.

Your fallacy is saying: there is a whole class of errors that can avoided if only we use a different type system, so there is no point in using that type system which defers (some or all) checks at runtime.

I can write code that manipulates values which represent types in the language, at runtime. If the types happen to be known or declared during compilation, fine enough, they can be optimized away. Otherwise, they will be checked later (which transparently invokes dynamic dispatch if needed), and I can even use them once they are known to compile the code myself, on a closure; there, along with other values which are then known, they can be taken into account to perform more aggressive optimizations. Why don't all language provide this?

As for bugs or errors, if you cannot lower risks (with static guarantees) then you have to improve on fault tolerance. You take other approaches to ensure the system behaves well, even if some parts can fail (e.g. Erlang).

> This is just rehashing the same tired and fallacious argument that most errors aren't type errors. And it is pure fallacy because different languages have different ideas as to what constitutes a type,

Ok, so you are writing an algorithm for a fast approximation of ATANH using IEEE floating point standard.

In type: IEEE floating point number Out type: the same.

Tell me how the magical type checking of the excellent programming language you propose will ensure that my calculations are correct.

Insightful +1. But by "types", they really mean the so-called practical languages' types, not the academic definition. Types allow you to prove something about your program - but it takes extra upfront effort to prove something. The trade-off between ease and proof-power has settled on what we have... IDK of course, but I don't think it will change much. And worse, the popularity of static typing is mainly due to performance, followed by documentation, and correctness of proof not really in it. But maybe this story's empirical github evidence on errors will shift it a little.

When you're re-coding all the time, the upfront cost isn't amortized over future runs as much as it used to be. Libraries are, but the massive real-world crowd-testing (i.e. usage) catches them...

BTW I really like units of measure types, you get dimensional analysis almost for free. You can do it in e.g. java but it's verbose (i.e. it's java). Classes, with arithmetic methods (add, sub, mult etc), You need an ezplicit class for each unit combination (though you can do a little better with generics). And get compile-time type errors when you assign, compare or operate incorrectly.

I don't claim to be very knowledgeable about this but it seems like you're bringing up a valid point. In the presenters analysis, he looks for very specific types of bugs when making the claim that static typing only addresses 1-5% of bugs. Your claim is, essentially, his type of analysis undercounts the number of bugs a non statically typed language by creating too heavy handed of filter.

Do you have any data to back this up or have links to papers that try and do a better job of counting issues that statically typed languages catch?