Dependency Free Capture Tracking

Abstract

Type systems usually characterize the shapes of values but not usually their free variables. Many desirable safety properties could be guaranteed by the type system if it knew exactly which variables were free in values. There has been much recent work investigating such systems, with an eventual goal of incorporating a capture tracking system into Scala. These systems are unfortunately complicated by advanced features in Scala’s type system, particularly dependent types. We explore what a capture tracking system could look like without the full complication of dependent types.