👩💻 Join our community of thousands of amazing developers!
Sized types hold great potential as a very practically useful way to do type-based termination checking, but sufficiently expressive sized types in dependent type theory come with a host of problems, mostly related to its incompatibility with the infinite size found in most simpler or nondependent type systems. This post attempts to describe some potential but ultimately unsatisfying solutions. The Latest and Greatest in Sized Types If you’re already familiar with sized types, in particular the...