# Lab Lunch by Conor McBride

**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.