PLClub Discussion Group

Decidable Type-Checking in Practice

For many programming languages, type-checking is undecidable in theory but “decidable in practice”. Or, at least, that is the common perception that has led many to discount decidability as a practical concern. But that perception does not match reality, and those that design and maintain major industry languages know this and wish there were more guidance on the issue. To illuminate the topic, I will demonstrate how (un-)decidability affects major languages, illustrate why type-checking can appear to be decidable in practice, and explore what becomes possible once we understand and take proper advantage of this phenomenon.