Comment by throwaway894345 | Hacker News Reader

Comment by throwaway894345 | Hacker News Reader

Parent Full thread

throwaway894345

I don’t see how JS or Python (not so sure about Julia) meaningfully have “dynamic checking for types”. If I have a function ‘def foo(a): return a.startswith(“foo”)’ and I pass an int in, Python doesn’t insert something like ‘if not isinstance(a, str): raise TypeError(“...”)’, partly because Python doesn’t even know that a str is expected; only that the param has a method called startswith(). And fair enough, maybe the type isn’t str in a statically typed language, but a Go-like structurally typed interface with a startswith() method; however, the function also isn’t inserting any meaningful check until the last possible moment when there is nothing left to do but blow up anyway, so I don’t see how this can meaningfully be called “dynamic type checking” when the types are all implicit and maximally abstract and the “check” is only dynamic dispatch. Pretty sure this all applies equally to JS except that a failed dynamic dispatch doesn’t raise an AttributeError but “undefined is not a function” IIRC. Not sure about Julia behavior, but I would guess that it also isn’t going to be sprinkling dynamic checks all over given its aspirations toward performance.

> I don’t see how JS or Python (not so sure about Julia) meaningfully have “dynamic checking for types”.

What would you describe as dynamic typechecking then? Would Scheme be a language that would fall under your definition, since it has much less dynamic dispatch?

> isn’t inserting any meaningful check until the last possible moment when there is nothing left to do but blow up anyway

I mean, inserting it earlier would require static knowledge of types, no?

> Not sure about Julia behavior, but I would guess that it also isn’t going to be sprinkling dynamic checks all over given its aspirations toward performance.

Haven't used it since I took a linalg class in undergrad, but my understanding was that Julia does similar dynamic dispatch, but it's using a JIT, and does type propagation. As a result, once operand types are known, the compiler is free to monomorphize and inline.

A coworker wrote a thing to do this for Common Lisp, too (for some numerical code); if you're willing to give up a bit of dynamism, you can get quite a bit of performance out of this.

> What would you describe as dynamic typechecking then? Would Scheme be a language that would fall under your definition, since it has much less dynamic dispatch?

I’m not sure about Scheme because I’m not very familiar, but one possibility is simply that “dynamic type checking” is meaningless. In other words, one could argue that anything that blows up at runtime is “runtime type checked” but that doesn’t seem meaningful. The only meaningful definition of “runtime type checking” that I can think of is explicit comparisons between a type annotation and a value’s runtime type information, for example, given this Python:

    def foo(a: str) -> bool:
        return a.startswith(“foo”)

I would argue that this would be “type-checked at runtime” if the interpreter implicitly added this snippet at the start of the function:

    if not isinstance(a, str):
        raise TypeError(“‘a’ is not a str”)

There are other possible notions, including a program which type checks each of its functions as their definitions are evaluated by the interpreter—I would call this “just-in-time type checking” and consider it a type of runtime type checking.

But these are different IMO than just blowing up at the last possible moment because there is no reasonable way to continue the program.

> I mean, inserting it earlier would require static knowledge of types, no?

First of all, even if it did require knowledge of static types, it could still be checked at runtime and thus runtime type checked. Secondly, many types aren’t known statically—consider types that are programmatically generated, such as are common when using SQLAlchemy, boto, etc. The interpreter could still type check these at runtime via either the JIT type-checking method described above or the flat-footed insertion of an isinstance() check at the start of the function (but I would argue that the later the type checking happens the less useful and meaningful it becomes).

> Haven't used it since I took a linalg class in undergrad, but my understanding was that Julia does similar dynamic dispatch, but it's using a JIT, and does type propagation. As a result, once operand types are known, the compiler is free to monomorphize and inline.

This sounds like the JIT type checking method that I described above, which is a concrete example of a meaningful runtime type checking example (as opposed to the notion that Python/JS does type checking at runtime which is either meaningless or incorrect IMO).

I agree with everything you say, except I have a lower bar of "meaningful".

> one possibility is simply that “dynamic type checking” is meaningless.

If I take your quotation out of context, this was the assumption of some people who separated languages into simply "strongly" vs "weakly" typed, by which they meant "checked by compiler" vs "not checked". It's incorrect though, and is the reason for separate "static" vs "dynamic" distinction.

C is a famous example of static (checked at compile time) but weak (≈ unsound) typing — compiler will happily accept programs that corrupt memory in all kinds of ways. mutating "const" variable, freeing used memory, crashing, remote code execution, and more... I don't think there are any invariants that a C compiler can enforce.

Scheme, Python, Lua, Javascript etc. OTOH, have no static (= compile-time) type checking, yet they maintain some invariants! An object that has pointers to it will not be freed; An object's type is known, and will not change (well, some class transmutation is allowed but some not, an int will not turn into an array); Some types are immutable; You can never divide a string / string! etc...

Moreover, by maintaining run-time metadata about object's types, they can tell you specifically that an operation raised a TypeError. Thus these languages are strongly typed at run time.

IOW, I'm arguing that anything that blows up at run time is checked IFF it tells you it was a type error. This is meaningful compared to C segfaults that tell you nothing :-)

---

The Java paper https://dl.acm.org/doi/pdf/10.1145/2983990.2984004 shows an interesting subtlety. "Fortunately, parametric polymorphism was not integrated into the Java Virtual Machine (JVM), so these examples do not demonstrate any unsoundness of the JVM" — yet they present unsound programs that "type-checks according to the Java Language Specification and is compiled by javac, version 1.8.0_25".

What gives? If a bad program compiles, how come JVM is still sound? See, Java has two type systems!

- JVM is the runtime, intended to be capable of loading even untrusted bytecode yet still maintain some type invariants. It manages memory and type metadata, and for this bad program will correctly identify type violation at run-time: "When executed, a ClassCastExceptionis thrown inside the main method with the message “java.lang.Integer cannot be cast to java.lang.String”"

- The compilers uses a distinct more complex static type system. The question of soundness is: can any program that passed the compiler cause JVM run-time type errors?

  + Java language allows you to write type casts.  These are deliberate "trust me" holes in the *static* type system, whose specified semantics is: JVM will check type at run time and raise exception if not as programmer promised.
    As https://typing-is-hard.ch/#what-about-unsafe-casts says, since these are deliberate, and fall back to meaningful run-time type checking(!), let's ignore them — redefine "soundness" as: can a program with no exclicit casts cause a run-time type error?

  + Generics only exist in static type system!
    They are invisible to JVM (aka "type erasure"), they compile into dynamically checked casts.  
    Their soundness goal was that the compiler can prove these implicit casts will never fail — e.g. you can only put candies into ArrayList<Candy>, so arr.get(0).eat() is guaranteed to give you a candy you can eat.
    That paper demonstrates a simple 17-line program with no explicit casts that compiles yet causes run time type error.

---

If you think what type soundness means, ALL statically typed languages have 2 type systems! There are execution semantics — what it means to, say, compute number + number. And there is a static language of talking about types that aims to predict / prove the types that will be involved at run time. Static checking fails if they don't match. Dynamic checking largely fails when you don't do it :-) But also when you erased info you needed to do it.

Reply on news.ycombinator.com