Title:
Contexts and Derivations as Semimodules over a Semiring of Resources
Abstract:
The knotty question of how to combine linearity with dependent typing is
often addressed by rejecting dependency on resource-controlled values
rather than accounting for it. The resulting systems typically have a
dependent arrow from unlimited sources, but a non-dependent lollipop. Not
content with this situation, I have been trying to find a reasonable
formulation of a dependent lollipop (x : S) -o T[x], where the return type
can depend on whatever the input value used to be. I think I've come up
with something promising. The key is that resources live in a semiring,
and that contexts and typing derivations, appropriately annotated with
resources, form semimodules over that semiring. The zero of the semiring
represents the amount of resource required to contemplate something, even
if one cannot consume it. Typechecking is a contemplative activity, but
when we multiply a typing derivation by zero, we learn that anything which
can be constructed, given whatever resources, can be contemplated with
none. The semiring {0, 1, lots} gives a linear dependent type system with
quantifiers corresponding to intersection, lollipop and Pi, respectively.