Comment by ChadNauseam

QTT supports three different "multiplicities". I discussed "used 0 times at runtime" (can be erased) and "used any amount of times at runtime" (cannot be erased). The remaining one is "used exactly once at runtime". These also cannot be erased, but allowing this constraint allows you to encode some very interesting things in the type system. The classic example is "resource protocols", e.g. file handles that force you to close them (and that you cannot use after closing).