3 ms·
Type systems push semantic properties into syntactic ones, thereby making them decidable. Note that there are halting programs which will fail to type check, bu
by ashton314 3y ago
Type systems push semantic properties into syntactic ones, thereby making them decidable. Note that there are halting programs which will fail to type check, but that’s the trade off.
- kaba0 3y ago> Type systems push semantic properties into syntactic ones Ordinary types are so-called trivial properties though, so Rice’s theorem doesn’t apply to them.
- mrkeen 3y agoYou can get a lot better than trivial. Transactions for instance.
- consilient 3y agoThis 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.