miniblog.

I keep thinking about the parallels between type checkers and abstract interpretation. E.g. abstract interpretation saying "this is one of two values, but I don't know which" feels very much like type checking a boolean. Have any tools taken advantage of this?

Excellent post on dependent types, why parametric polymorphism is good, and building inscrutable type checkers:

One thing I've really come to appreciate from working on type checkers: There's a crucial difference between the type system and checks you can do on type-inferred code. E.g. using a bottom type is totally well-typed, but users expect warnings: x = exit(0);