Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Typing Is Hard

typing-is-hard.ch

Post reply on HN
Print view View original

51–60 of 83 posts

Re: Typing Is Hard

#51

Post by remexre »

throwaway894345 wrote: post #49
remexre wrote: post #46

Earlier quoted context omitted.

Having no type system (e.g. Forth) is different from having dynamic checking for your types (e.g. JavaScript, Python, Julia iirc), though. Julia also has Common Lisp-like multimethods, which are pretty nice, especially for linear algebra sorts of stuff, where you might be multiplying a scalar by a tensor, or a tensor by a tensor, and don't want to have to specify different syntax for the two operations.

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 th…

> 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.

Re: Typing Is Hard

#52

Post by kjeetgill »

riwsky wrote: post #26
Lammy wrote: post #25

The headline made me hope for an article about ergonomics.

People keep arguing for array covariance as if soundness and developer ergonomics were in conflict, but upgrading your type system from a laptop keyboard to some infamously-sound Cherry MX blues shows you indeed can have both. With the amount of high-quality keyboard manufacturers these days, though, and the support for variance in preferred type parameters—do you need backlighting? Mac keys?—I do not blame people fo…

Ugh, I hate to do this, but GPT-3? Am I being paranoid?

Edit: Nevermind, I think I just missed the joke maybe

Re: Typing Is Hard

#53

Post by intortus »

jcelerier wrote: post #35
intortus wrote: post #28

Earlier quoted context omitted.

Sure, you don't have to go out of your way to challenge your type system, but it still means that you're a single typo away from sending your compiler and yourself on a wild goose chase.

> Sure, you don't have to go out of your way to challenge your type system, but it still means that you're a single typo away from sending your compiler and yourself on a wild goose chase. the alternative would be writing bash or python or ... scripts to generate the code, and for those : - you likely don't have any error message at all (ugh) - they won't have knowledge of the type system of the language you're opera…

There are mainstream languages with decidable static type systems. They compile quickly and give obvious short error messages.

Re: Typing Is Hard

#54

Post by Kutta »

johncolanduoni wrote: post #45
Kutta wrote: post #38

Earlier quoted context omitted.

Incorrect. Whether the language as a logic is capable of expressing undecidable statements, is orthogonal to whether type checking is decidable. Type checking is analogous to checking proof validity in logics. Commonly used proof systems for first-order or higher-orders logics admit decidable proof validity, and already many first-order theories allow expressing undecidable statements. ZFC is a rather obvious example…

This is not true, as MLTT-style type theories have a different syntactical notion of proof than first order logical theories like ZFC. Proof of termination of type checking for Idris is equivalent to proof that all terms can be reduced to a normal form: for any given term, you can construct another term which when type checked requires fully normalizing the first term. It is well known that proving that the normal fo…

I don't see that "normalization implies consistency", which I'm aware of, relates to my previous comment in any relevant way.

ZFC and MLTT do not differ in that decidability of proof validity is not related to logical expressiveness.

It's not even true that for type theories, decidability of proof validity implies normalization. Normalization is not logically equivalent to decidable type checking.

For example, we can have a term language for extensional type theory which is annotated with reduction traces. This is the kind of syntax that we get when we embed ETT inside ITT. It has decidable type checking, as the type checker does not have to perform reduction, it only has to follow traces. This kind of tracing is actually used in the GHC Haskell compiler to some extent. So we have decidable type checking for a surface syntax of a type theory, for a type theory which is a) consistent b) not strongly normalizing.

Re: Typing Is Hard

#55

Post by dnautics »

Is the comment about zig correct about its typing? It's certainly true about its compilation, but that's not the same thing. Also, if you're going to have a turing-complete compile time, you might as well have it in something that looks like a programming language, since that will fit your debugging mental model.

Re: Typing Is Hard

#56

Post by IshKebab »

It would be interesting to know the practical implications - given how many of these languages are very popular I'm assuming it doesn't really matter?

Re: Typing Is Hard

#57

Post by throwaway894345 »

remexre wrote: post #51
throwaway894345 wrote: post #49

Earlier quoted context omitted.

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 th…

> 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 wou…

> 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).

Re: Typing Is Hard

#58

Post by bmc7505 »

Kutta wrote: post #38
bmc7505 wrote: post #33

Earlier quoted context omitted.

Just because the current implementation of the Idris type checker always terminates due to the size change termination heuristic does not mean that type checking Idris is decidable. If the type system as specified allows an author to express undecidable statements, it should not be considered decidable, regardless of whether one type checking implementation terminates on all inputs. If some type checker does not impl…

Incorrect. Whether the language as a logic is capable of expressing undecidable statements, is orthogonal to whether type checking is decidable. Type checking is analogous to checking proof validity in logics. Commonly used proof systems for first-order or higher-orders logics admit decidable proof validity, and already many first-order theories allow expressing undecidable statements. ZFC is a rather obvious example…

I think you might be confusing the language and the type system. Not saying anything about the runtime characteristics of the language (which is obviously Turing Complete), but the type system itself, which is TC. If the type system allows you to encode a TM, then it is undecidable, regardless of whether it terminates due to an incomplete type checker. Since the Idris type system allows you to encode a TM, then the type system is undecidable due to the Halting problem.

Re: Typing Is Hard

#59

Post by Kutta »

bmc7505 wrote: post #58
Kutta wrote: post #38

Earlier quoted context omitted.

Incorrect. Whether the language as a logic is capable of expressing undecidable statements, is orthogonal to whether type checking is decidable. Type checking is analogous to checking proof validity in logics. Commonly used proof systems for first-order or higher-orders logics admit decidable proof validity, and already many first-order theories allow expressing undecidable statements. ZFC is a rather obvious example…

I think you might be confusing the language and the type system. Not saying anything about the runtime characteristics of the language (which is obviously Turing Complete), but the type system itself, which is TC. If the type system allows you to encode a TM, then it is undecidable, regardless of whether it terminates due to an incomplete type checker. Since the Idris type system allows you to encode a TM, then the t…

A type system cannot be TC. What you seem to talk about, is that if a type checker can simulate arbitrary TM's through an encoding of its input, then the type checker is necessarily non-total. This is correct. But the Idris checker is total and it is not possible to use it to simulate TMs.

The Idris type system does allow you to specify and formalize TMs internally, but that has no bearing on decidability of type checking, as I explained before.

Re: Typing Is Hard

#60

Post by johncolanduoni »

Kutta wrote: post #54
johncolanduoni wrote: post #45

Earlier quoted context omitted.

This is not true, as MLTT-style type theories have a different syntactical notion of proof than first order logical theories like ZFC. Proof of termination of type checking for Idris is equivalent to proof that all terms can be reduced to a normal form: for any given term, you can construct another term which when type checked requires fully normalizing the first term. It is well known that proving that the normal fo…

I don't see that "normalization implies consistency", which I'm aware of, relates to my previous comment in any relevant way. ZFC and MLTT do not differ in that decidability of proof validity is not related to logical expressiveness. It's not even true that for type theories, decidability of proof validity implies normalization. Normalization is not logically equivalent to decidable type checking. For example, we can…

You’ve actually hit on the difference here: in the type theory the witness term plus the reduction trace is equivalent to the ZFC proof. It’s true that checking this combination is decidable, regardless of consistency. The intentionality does not eliminate the limitations of this property, it only provides that the reduction trace is implicit given the witness term. The actual proofs of decidability of type checking (e.g. from Martin-Löf‘s original paper) are conditioned on the normalization theorem, which assumes consistency of the type theory.

Let’s come at this from the other direction. Suppose I find a non-normalizing term X of type false (like that produced by Girard’s paradox if we leave off stratification). What happens when I try to type check this?

id(X): ==(X, rec_0(0, X))

Where id is the constructor of the propositional equality type and rec_0 is the recursor for False.

Post reply on HN