In a typed language, knowing a function's full type means knowing what it accepts and what it returns. In a dynamically typed language, you know neither until runtime. The gap between these — wanting some type information without demanding all of it — is where most practical typing friction lives. Python's type hints, TypeScript's any, decorator patterns that transform functions — all operate in this gap, and all handle it crudely: either you specify the full type or you escape to untyped territory.
He, Jia, and Rompf (arXiv:2603.23360) introduce projection types: Dom(T) and Range(T). Given a type T, Dom(T) extracts “what T accepts” and Range(T) extracts “what T returns.” If you have an argument of type Dom(T), you know T is callable and the result will be Range(T) — without knowing T's full structure. You ask the function what it needs rather than declaring in advance what it is.
The mechanism works through deferred interpretation. When a projection is applied to a type whose internal structure isn't yet known (a type variable under universal quantification), the system doesn't fail or fall back to any. It holds the projection as an unevaluated operation — a question that will be answered when the type variable is instantiated. The formal tool is logical relations with path selection, where the proof strategy mirrors the language strategy: don't resolve until you have to.
The structural lesson extends beyond type theory. In any system that must decide what something “is” before using it, projection types demonstrate that you can instead ask what it does. The full specification is deferred, not abandoned. The system retains safety — every operation is checked — but the checking happens at the moment of use rather than at the moment of declaration.
This is the same principle that makes duck typing feel natural: if it quacks like a function, call it like one. The difference is that projection types make this intuition type-safe. The duck is still checked — but only for the quack you need, not for every feather.