Extensive Challenges for Static Typing
Barry Jay – 18 September 1996
This brief talk will be an exploration of some challenges, rather than a presentation of results.
The ability to check the types of programs places some constraints on the power of the type system. Additional constraints arise if types are checked statically, i.e. during compilation of the program.
If we model types as objects of a category, with programs as morphisms, then the constraints on typing do not allow us to assume the existence of all finite limits. Further, static typing is in conflict with extensivity, which already assumes the existence of a generous class of pullbacks. The problems arise when *assuming* the existence of finite limits.
To anyone (like me) who has used lextensivity as a foundational tool in the study of computation (as opposed to specification), this is somewhat disturbing. I conjecture that the limits required for type analysis can be constructed without first assuming their existence.
Back