We propose a type-directed garbage collection (GC) scheme for a programming
language with static memory management based on a linear type system.
Linear type systems, which can guarantee certain values (called linear
values) to be used only once during program execution, are useful for
memory management: memory space for linear values can be reclaimed
immediately after they are used. However, conventional pointer-tracing GC
does not work under such a memory management scheme: if the memory space
for used linear values is still reachable through pointers, dangling
pointers are created.
This problem is solved by exploiting static type information during garbage
collection in a way similar to tag-free GC. Type information in our linear
type system represents not only the shapes of heap objects but also how
many times the heap objects are accessed in the rest of computation. Using
such type information at GC-time, our GC can avoid tracing dangling
pointers. In addition, our GC can reclaim even reachable garbage. We
formalize such a GC algorithm and prove its correctness.
