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);
miniblog.
Related Posts
1
I'm surprised there aren't more interpreted languages with a first party type checker.
Python has several good type checkers, Ruby has Sorbet, and there are others.
Having zero compilation time *and* a full IDE seems like such a compelling design, at least on paper.
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:
