The Calculus of Semantic Universes

The Calculus of Semantic Universes (CSU) is a stratified, extensional type theory. An infinite stack of categories 𝒞0, 𝒞1, 𝒞2, … — values, types, kinds, and so on — is generated by a single grammar parameterised by the level. Each level is interpreted as sets of objects of the level below; subtyping is inclusion and is decided by one emptiness check. There is no typeof: the only way up a level is the singleton lift, which carries compile-time values into types. Functions and metafunctions are identified by their bodies, behavioural equivalence is established only by theorems, and a program may be inspected only from strictly above it. Refinements are intersections with the acceptance set of a predicate, and mutability is carried by the distinction between a union of singletons and the singleton of a union, from which reference invariance is derived rather than postulated. All type information is erased before code generation. Each section states the mathematics precisely and ends with a box, Interpretation: the idea of …, that says the same thing in plain language. Appendix 1 specifies the core intermediate representation of a compiler for the calculus, Appendix 2 surveys related research, and Appendix 3 is a glossary of notation and terminology.