1. Rejecting all buggy programs, for some class of bugs, at the cost of also rejecting some valid programs is precisely what most (published) type do. "soft type systems" are the ones that let you run any valid program you want, and only catch some bugs. A type system should
Reject all buggy programs
Accept all bug-free programs (an untyped program is "accepted" if there is any way of assigning types to get a well-typed program)
Have decidable type inference (starting from a completely untyped program)
The full theorem says you get two. It's actually possible to get two. Say you start with the untyped lambda calculus, and want to avoid expressions that don't terminate.
The untyped lambda calculus already trivially accepts all terminating expressions and has decidable type inference (but also accepts all diverging expressions).
The simply typed lambda calculus rejects all non-terminating expressions and has decidable type inference (but rejects plenty of good programs too).
System F accepts all terminating expressions and rejects all nonterminating expressions (but inference is undecidable).
2 "Stronger" doesn't always mean the same thing, but lots of the work on already-sound type systems are about accepting more valid programs while still completely excluding some class of bugs. If you are just worried about keeping the wrong primitive types aways from case statements then simple types, Hindley-Milner and MLF are all safe, but the stronger ones accept more programs.
There's a "full-employment" theorem here, saying you can improve a type system on one of the axes above without making it worse on the other two. Trivially, just hardcode some program mishandled by the existing system - maybe there's a more interesting result? (You can quantify decidability by looking at how much type information you have to add for your algorithm to infer the rest).
A perfect type system (scratch the static!) is impossible, but that means any type system can be improved.
![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png){kind=small}
Limits of type systems
1. Rejecting all buggy programs, for some class of bugs, at the cost of also rejecting some valid programs is precisely what most (published) type do. "soft type systems" are the ones that let you run any valid program you want, and only catch some bugs. A type system should
- Reject all buggy programs
- Accept all bug-free programs (an untyped program is "accepted" if there is any way of assigning types to get a well-typed program)
- Have decidable type inference (starting from a completely untyped program)
The full theorem says you get two. It's actually possible to get two. Say you start with the untyped lambda calculus, and want to avoid expressions that don't terminate.- The untyped lambda calculus already trivially accepts all terminating expressions and has decidable type inference (but also accepts all diverging expressions).
- The simply typed lambda calculus rejects all non-terminating expressions and has decidable type inference (but rejects plenty of good programs too).
- System F accepts all terminating expressions and rejects all nonterminating expressions (but inference is undecidable).
2 "Stronger" doesn't always mean the same thing, but lots of the work on already-sound type systems are about accepting more valid programs while still completely excluding some class of bugs. If you are just worried about keeping the wrong primitive types aways from case statements then simple types, Hindley-Milner and MLF are all safe, but the stronger ones accept more programs.There's a "full-employment" theorem here, saying you can improve a type system on one of the axes above without making it worse on the other two. Trivially, just hardcode some program mishandled by the existing system - maybe there's a more interesting result? (You can quantify decidability by looking at how much type information you have to add for your algorithm to infer the rest).
A perfect type system (scratch the static!) is impossible, but that means any type system can be improved.
-Brandon (brandon_m_moore on Yahoo)