Just what exactly _is_ a type? A common perspective is that types are _restrictions_. Static types restrict the set of values a variable may contain, capturing some subset of the space of “all possible values.” Under this worldview, a typechecker is sort...