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

21–30 of 83 posts

Re: Typing Is Hard

#21

Post by guerrilla »

fnord77 wrote: post #19

what's the connection between being undecidable and turing complete?

Type checking is undecidable for type theories that are Turing-complete. Type theories are Turing complete if they can simulate a turing machine. Roughly, type chicking for a type theory is undecidable if its not decidable whether every term has the type assigned to it by the programmer. The halting problem is the connection, which the website states but the author is inviting bug reports, so maybe its a good idea to ask them to clarify it.

Re: Typing Is Hard

#22

Post by pcstl »

fnord77 wrote: post #19

what's the connection between being undecidable and turing complete?

tl;dr: Every Turing Complete system is undecidable - i.e. for every Turing Complete system which answers "yes" or "no", you can't determine in finite time whether, for any given input, the program will accept it or not.

Long version:

Being Turing Complete means that a system can compute everything that a Turing Machine can compute.

For a long time, it was an open question whether there was a way to determine whether, for a given statement, one could determine whether it was universally valid.

Alan Turing's creation of the Turing Machine was originally in order to try to answer this question. The idea was that to determine if a statement was universally valid, one would need to be able to mechanically derive the statement from the axioms of logic - i.e., there would be an algorithm (which Turing formalized as a "Turing Machine") that would be able to take the input and decide whether it was universally valid.

Turing then proved - likely his greatest claim to fame - that such an algorithm could not exist - as one can always build an input for which it will be forced to give the wrong answer.

Hence, Turing showed that for any Turing Machine - or any system equivalent to a Turing Machine - which answers "yes" or "no" to some input, it is impossible to decide whether it accepts its input in finite time.

Re: Typing Is Hard

#23

Post by gpm »

fnord77 wrote: post #19

what's the connection between being undecidable and turing complete?

If your type system is turing complete, then it's undecidable. This is easily seen through rices theorem [0] which states that all non-trivial (not always true or always false) semantic properties (i.e. about what inputs it maps to what outputs) of turing complete programs are undecidable. In particular what type something is going to be is undecidable.

Intuitively you should probably think of this as a slight extension of the halting problem, you can't always tell whether or not something (your type checking) halts. It's not that much of a leap to say that you can't tell whether it will halt after an even number or odd number of steps if it does halt (this doesn't immediately follow from the halting problem, but it is true). Imagine if you had a type that said "if it takes an even number of steps for some given computation to halt, I'm 'type A', if it takes an odd number I'm 'type B'". That's something a turing complete type system can do, and since you can't tell whether it will take an even or odd number of steps you can't tell whether or not the variable is 'type A' or 'type B'.

If it's undecidable it's not necessarily turing complete, but it's very easy to be accidentally turing complete, so it probably is.

[0] https://en.wikipedia.org/wiki/Rice%27s_theorem

Re: Typing Is Hard

#24

Post by riwsky »

Correction: Java’s type system has been unsound since version 5; version 8 (which TFA describes as the start of the issue) just happened to be the latest version at the time it was discovered.

Re: Typing Is Hard

#26

Post by riwsky »

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 for asserting the problem of picking one is undecidable.

Re: Typing Is Hard

#27

Post by mathgladiator »

This is great, and I'm developing a static type system for my programming language (for board games), and I've messed up the type system so many times.

The challenge beyond the math is then making the error messages useful, and also being able to make progress beyond the first error in a useful way.

Re: Typing Is Hard

#28

Post by intortus »

ekidd wrote: post #15

Pretty much any language supporting something like C++'s "template metaprogramming" will allow the programmer to perform arbitrary computation at compile time. This is, of course, "undecidable", because it's Turing complete. This is not necessarily the end of the world. If you go out of your way to write an actual compile-time program by abusing your type system, and that program contains an endless loop, you probabl…

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.

Re: Typing Is Hard

#30

Post by dleslie »

intortus wrote: post #28
ekidd wrote: post #15

Pretty much any language supporting something like C++'s "template metaprogramming" will allow the programmer to perform arbitrary computation at compile time. This is, of course, "undecidable", because it's Turing complete. This is not necessarily the end of the world. If you go out of your way to write an actual compile-time program by abusing your type system, and that program contains an endless loop, you probabl…

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.

Stage early and stage often; if a single-but-syntactically-valid typo will break your build then you should only be a commit away from something that works.
Post reply on HN