Typechecking is undecidable when 'type' is a type (1989) [pdf]

pvillano 38 minutes ago | parent | next [-]

This stack exchange answer talks about the importance of decidability in type checking

https://langdev.stackexchange.com/a/2072

My interpretation

Decidability is of academic interest, and might be a hint if something is feasible.

But there are (1) ways of sidestepping undecidability, e.g. A valid C++/Rust program is one for which the typechecker terminates in x steps without overflowing the stack

And (2) things which are decidable, but physically impossible to calculate, e.g the last digit of the 10^10^10 th prime

What matters is being able to reject all incorrect programs, and accept most human written valid programs

▲

moomin 3 hours ago | parent | prev | next [-]

It feels like this is unsurprising, given we already have Goedel's theorems and halting theorems. Any system of self-describing complexity ends up in this territory.

▲

Animats 5 hours ago | parent | prev | next [-]

This sounds close to Russell's "class of all classes" paradox. Is it?

▲

enricozb 4 hours ago | parent [-]

Yes the type theoretic analog to Russel's (set theoretic) paradox is Girard's (as mentioned in the abstract) paradox.

▲

srcreigh 4 hours ago | parent [-]

This is incorrect. The set paradox it’s analogous to is the inability to make the set of all ordinals. Russel’s paradox is the inability to make the set of all sets.

▲

kibwen 3 hours ago | parent [-]

Since we're being pedantic, Russel's paradox involves the set of all sets that don't contain themselves.

▲

iterance 2 hours ago | parent [-]

Technically speaking, because it's not a set, we should say it involves the collection of all sets that don't contain themselves. But then, who's asking...

▲

afiori 18 minutes ago | parent | next [-]

The paradox is about the set of all sets that do not contain themselves, or a theorem that such a set does not exist.

In the context of the paradox you need to call it a set, otherwise it would not be a paradox

▲

nurettin 2 hours ago | parent | prev [-]

I'm asking. What prevents that collection from being a set?

	▲	scapp an hour ago \| parent \| next [-]
		This is the easiest of the paradoxes mentioned in this thread to explain. I want to emphasize that this proof uses the technique of "Assume P, derive contradiction, therefore not P". This kind of proof relies on knowing what the running assumptions are at the time that the contradiction is derived, so I'm going to try to make that explicit. Here's our first assumption: suppose that there's a set X with the property that for any set Y, Y is a member of X if and only if Y doesn't contain itself as a member. In other words, suppose that the collection of sets that don't contain themselves is a set and call it X. Here's another assumption: Suppose X contains itself. Then by the premise, X doesn't contain itself, which is contradictory. Since the innermost assumption is that X contains itself, this proves that X doesn't contain itself (under the other assumption). But if X doesn't contain itself, then by the premise again, X is in X, which is again contradictory. Now the only remaining assumption is that X exists, and so this proves that there cannot be a set with the stated property. In other words, the collection of all sets that don't contain themselves is not a set.
	▲	lmm 39 minutes ago \| parent \| prev \| next [-]
		The paradox. If you create a set theory in which that set exists, you get a paradox and a contradiction. So the usual "fix" is to disallow that from being a set (because it is "too big"), and then you can form a theory which is consistent as far as we know.
	▲	whiterock 35 minutes ago \| parent \| prev \| next [-]
		Let R = {X \notin X}, i.e. all sets that do not contain themselves. Now is R \in R? Well this is the case if and only if R \notin R. But this clearly cannot be. Like the barber that shaves all men not shaving themselves.
	▲	empath75 42 minutes ago \| parent \| prev [-]
		They redefined sets specifically to exclude that construction and related ones.

▲

rerdavies 2 hours ago | parent | prev | next [-]

Not getting it. Why would you want to do this? And why is no distinction made between `typeof(type)` and `type`? And doesn't the entire problem go away if you distinguish between `typeof(type)`, which is a value whose type is `type`?

	▲	lmm 33 minutes ago \| parent [-]
		> Why would you want to do this? It makes life much easier when you want to use fancier types. E.g. if you want to be able to have ListOfLength[4], it's much nicer to be able to use normal 4 which you can use normal arithmetic on (and therefore say that when you append ListOfLength[x] to ListOfLength[y] you get ListOfLength[x + y]), than to have to encode everything in types and make it some kind of ListOfLength[SpecialTypeLevel4] (and then when you append the two lists you get a ListOfLength[TypeLevelAdditionIsCommutative[TypeLevelAdd[x, y]]#Result] or something). To make that work you have to be able to use values as type parameters, i.e. types, so you have to be able to have e.g. types of type int, as well as types of type type, and it all gets a lot simpler and easier to work with if you just say that types have type type. > And why is no distinction made between `typeof(type)` and `type`? Well that's the whole point, to say that type is of type type. > And doesn't the entire problem go away if you distinguish between `typeof(type)`, which is a value whose type is `type`? No, because why would you ever use it as a value? The whole point of typeof is that it gives you a type that you can use as a type.

▲

randomNumber7 3 hours ago | parent | prev | next [-]

And still this type system could be the base for a very interesting and powerfull programming language imo.

▲

amelius 2 hours ago | parent | next [-]

Yeah we don't throw programming languages away because they are undecidable.

So why would we throw type systems away if they are undecidable?

▲

BalinKing 44 minutes ago | parent | next [-]

My 2¢ from an interactive theorem proving perspective: In so-called computational type theory, typechecking is indeed allowed to be undecidable, and you get a lot of cool expressive power (e.g. well-behaved quotients and subtypes) as a result. This was one of the big ideas behind NuPRL back in the day, and Istari[0] more recently.

[0] www.istarilogic.org

▲

ChadNauseam 2 hours ago | parent | prev [-]

Decidability isn't even that useful. If typechecking takes a million years, that's also bad. What you want is guarantees that correct programs typecheck quickly. Without this, you end up in swift land, where you can write correct code that can't be typechecked quickly and the compiler has to choose between being slow or rejecting your code

	▲	instig007 2 hours ago \| parent [-]
		> What you want is guarantees that correct programs typecheck quickly. In practice there's wealth of lemmas provided to you within the inference environment in a way standard library functions are provided in conventional languages. Those act like a memoization cache for the purpose of proving your program's propositions. A compiler can also offer a flag to either proceed with ("trust me, it will infer in time") or reject the immediately undecidable stuff.

▲

rerdavies 2 hours ago | parent | prev | next [-]

Presumably with the rather unpleasant side-effect of compiles that may never finish. :-P

▲

solomonb 2 hours ago | parent | prev [-]

This really isn't a big deal as it resolved via type universes.

▲

noosphr 2 hours ago | parent | prev | next [-]

Type systems aren't magic. They do stop all incorrect programs from running, but also the majority of correct programs too.

	▲	anon291 2 hours ago \| parent \| next [-]
		Luckily most everyday programs are typeable.
	▲	rerdavies 2 hours ago \| parent \| prev [-]
		... for some spectactularly inconsistent and arbitrary definition of "correct program".

▲

marcosdumay 4 hours ago | parent | prev | next [-]

Hum... I'm getting 403, forbiden. Is it down?

	▲	rerdavies 2 hours ago \| parent \| next [-]
		Working for me, but very very slow to load (which I assume is most of the way to 403).
	▲	zem 4 hours ago \| parent \| prev [-]
		still working for me

▲

cwmoore 5 hours ago | parent | prev [-]

Similar to the difficulty in finding Title Search companies on Indeed.