We may need better specification for existing and future refinement types in the type system

On the one hand, the spec isn’t aimed at beginners, we don’t need to shy away from it getting more complicated, just precise with intention. On the other, we have woefully few established definitions for python’s use, and the specification wasn’t written starting from a set of common definitions.

The difference between an annotation specifying a type, a type, and a value satisfying that type as an annotation has established terminology in a few models of type theory, but we haven’t adopted any of those models nor do we have our own consistently used terminology for this in the specification, so as I’ve been going through things and implementing, I’ve found a few places already where the language of the specification appears to be specifying something different from what a few type checkers currently do, and it becomes important to figure out how much of that is language needing updates and how much of that is type checkers not implementing everything as specified.

I’m not immediately concerned with the specification describing this for beginners. We would still want that distinction covered somewhere in the documentation for users, but that’s probably easier to get right once we have the precise definitions we intend to use for specifications.

2 Likes