Typechecking is undecidable when 'type' is a type (1989) [pdf]
dspace.mit.edu79 points by zem 4 days ago
79 points by zem 4 days ago
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
Decidability of a type system is like well-typedness of a program. It doesn't guarantee it's sensible, but not having the property is an indicator of problems.
I'm not entirely smart enough to connect all of these things together but I think there is a kind of subtlety here thats being stepped on.
1. Complete, Decidable, Well founded are all distinct things.
2. Zig (which allows types to be types) is Turing complete at compile time regardless. So the compiler isn't guaranteed to halt regardless and it doesn't practically matter.
3. The existance of a set x contains x is not enough by itself to create a paradox and prove false. All it does is violate the axiom of foundation, not create a russles paradox.
4. The axiom of foundation is a weird sort of arbitrariness in that it implies this sort of DAG nature to all sets under set membership operation.
5. This isn't nessesarily some axiomatically self evident fact. Aczel's anti foundation axiom works as well and you can make arbitrary sets with weird memberships if you adopt that. https://en.wikipedia.org/wiki/Aczel%27s_anti-foundation_axio...
6. The Axiom of Foundation exists to stop you from making weird cycles, but there is parallel to the axiom of choice, which directly asserts the existance of non computable sets using a non algorithmicly realizable oracle anyway....
Your other points are more relevant to the content of the article, but point 2. relates the practical consequences of undecidable type-checking, so I'll reply to that.
I don't have a problem with compile time code execution potentially not terminating, since it's clear to the programmer why that may happen. However, conventional type checking/inference is more like solving a system of constraints, and the programmer should understand what the constraints mean, but not need to know how the constraint solver (type checker) operates. If it's undecidable, that means there is a program that a programmer knows should type check, but the implementation won't be happy with; ruining the programmer's blissful ignorance of the internals.
> 2. Zig (which allows types to be types) is Turing complete at compile time regardless. So the compiler isn't guaranteed to halt regardless and it doesn't practically matter.
Being Turing complete at compile time causes the same kinds of problems as undecidable typechecking, sure. That doesn't make either of those things a good idea.
> 3. The existance of a set x contains x is not enough by itself to create a paradox and prove false. All it does is violate the axiom of foundation, not create a russles paradox.
A set that violates an axiom is immediately a paradox from which you can prove anything. See the principle of explosion.
> 4. The axiom of foundation is a weird sort of arbitrariness in that it implies this sort of DAG nature to all sets under set membership operation.
Well, sure, that's what a set is. I don't think it's weird; quite the opposite,
> 5. This isn't nessesarily some axiomatically self evident fact. Aczel's anti foundation axiom works as well and you can make arbitrary sets with weird memberships if you adopt that.
I don't think this kind of thing is established enough to say that it works well. There aren't enough people working on those non-standard axioms and theories to conclude that they're practical or meet our intuitions.
> 6. The Axiom of Foundation exists to stop you from making weird cycles, but there is parallel to the axiom of choice, which directly asserts the existance of non computable sets using a non algorithmicly realizable oracle anyway....
The Axiom of Foundation exists to make induction work, and so does the Axiom of Choice. They both express a sense that if you can start and you can always make progress, eventually you can finish. It's very hard to prove general results without them.
Does Rice's theorem cover this?
> [ all non-trivial semantic properties of programs are undecidable ]
https://en.wikipedia.org/wiki/Rice's_theorem
Found here:
From Sumatra to Panama, from Babylon to Valhalla
No. Being well typed is not a semantic property of of a program - in a language where it makes sense to talk about running badly typed code, a piece of code that starts with an infinite loop may be well or badly typed after that point with no observable difference in program behaviour.
There are decidable type systems for Turing complete languages (many try to have this property), and there are languages in which all well typed programs terminate for which type checking is undecidable (System F without all type annotations).
This sounds close to Russell's "class of all classes" paradox. Is it?
Yes the type theoretic analog to Russel's (set theoretic) paradox is Girard's (as mentioned in the abstract) paradox.
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.
Perhaps I overstated how related the two were. I was pulling mostly from the Lean documentation on Universes [0]
> The formal argument for this is known as Girard's Paradox. It is related to a better-known paradox known as Russell's Paradox, which was used to show that early versions of set theory were inconsistent. In these set theories, a set can be defined by a property.
[0]: https://lean-lang.org/functional_programming_in_lean/Functor...
Since we're being pedantic, Russel's paradox involves the set of all sets that don't contain themselves.
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...
I'm asking. What prevents that collection from being a set?
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.
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.
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.
They redefined sets specifically to exclude that construction and related ones.
And still this type system could be the base for a very interesting and powerfull programming language imo.
Yeah we don't throw programming languages away because they are undecidable.
So why would we throw type systems away if they are undecidable?
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
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
> 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.
Presumably with the rather unpleasant side-effect of compiles that may never finish. :-P
This seems strange to me, but it's hours past my bed time and I haven't tried reading lambda calculus or lambda-star calculus theory in about 20 years.
Many programming languages have a variant or object type. In C#, any instance of a class will also say that it is of type System.Object. That does nearly make that a type of all types.
There is some nuance and special cases. Like any null is considered a null instance of any nullable object, but you're also not permitted to ask a null value what type it is. It just is a null. Similarly, C# does differentiate between a class and an instance of a class. Both a class and an instance are of a given type, but a class is not an instance of a class.
Presumably the difference is either in one of those nuances, or else in some other axiomatic assertion in the language design that this paper is not making.
Or else I'm very much missing what the author is driving at, which at this time of the morning seems equally possible.
> Many programming languages have a variant or object type. In C#, any instance of a class will also say that it is of type System.Object. That does nearly make that a type of all types.
That's a type of all values, not a type of all types.
In richer programming languages, you can do operations on types much like you can do operations on values. E.g. in C# you can write "List<String>", but you can't do something like "var x = List; var y = String; x<y>". (Which might seem pointless, but it allows you to do things like write a conversion from x<Int> to x<String> that you can reuse with different x types). So then you need a type for x and y, which is conventionally type, and you have to ask what the type of type is. (And if it's type, then that's very natural and makes some things very easy - but at the cost of making typechecking undecidable, as per the article).
> Similarly, C# does differentiate between a class and an instance of a class. Both a class and an instance are of a given type, but a class is not an instance of a class.
Incidentally one of the things I missed from Delphi in C#. In Delphi you can declare
type TWidgetClass = class of TWidget;
var widgetClass := TTextWidget;
var myWidget := widgetClass.Create();
System.Object is a type of all objects, NOT a type of all types. That is, all objects are System.Object. If one has a class Foo, then every object of type Foo is also of type System.Object. But what is the type of Foo itself? Not of an instance of Foo, but Foo itself. In the languages this paper is about, the type system can recurse upon itself, allowing types themselves to have type. It’s sort of like C#’s System.Type, except System.Type is a class that holds type information for runtime type inspection, whereas the type of types in this paper is for compile-time generics that can abstract over not just types but the types of types as well.
Type systems aren't magic. They do stop all incorrect programs from running, but also the majority of correct programs too.
Luckily most everyday programs are typeable.
And you don't need cut in logic either: https://philpapers.org/rec/BOODEC
It's just that your typeable program might take more data to store than there are bits in the universe.
I'm not saying that types are bad. They aren't.
I'm saying they aren't magic and they come with a trade off.
... for some spectactularly inconsistent and arbitrary definition of "correct program".
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.
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`?
> 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.
Hum... I'm getting 403, forbiden. Is it down?
Working for me, but very very slow to load (which I assume is most of the way to 403).
Similar to the difficulty in finding Title Search companies on Indeed.
[dead]