3 ms·
This isn't right: `int -> Zero` is an "ordinary" type, but certainly does not correspond to a trivial property. The reason Rice's theorem doesn't apply to types
by consilient 3y ago
This isn't right: `int -> Zero` is an "ordinary" type, but certainly does not correspond to a trivial property. The reason Rice's theorem doesn't apply to types is that they're not purely "semantic" in the relevant sense, since they're not fully determined by the language a TM accepts.
- kaba0 3y agoWhat type system do you imagine having that type signature? Zero being a value is usually exempt from the type system (unless we have dependent types, but I would definitely not call those ordinary). Of course if it’s a special type with only a single elem with no relation to int, then it is again trivial.
- ashton314 3y agoTyped Racket (not a dependently typed system mind you) has zero as a type. It’s a fantastically useful type to have.
- consilient 3y agoAny language with function types and singletons. > Of course if it’s a special type with only a single elem with no relation to int, then it is again trivial. No, it isn't. "Trivial" in the context of Rice's theorem means either true of all Turing machines or false of all Turing machines.