If is a type and e is an expression then is an expression
If and are expressions then is an expression
If x is a variable, is a type, and e is an expression, then is an expression
The and the subscripts of,, and are sometimes omitted when they can be unambiguously determined from the context. Juxtaposition is often used as an abbreviation for a combination of and composition:
Typing rules
The presentation here uses sequents rather than hypothetical judgments in order to ease comparison with the simply typed lambda calculus. This requires the additional Var rule, which does not appear in Hasegawa In kappa calculus an expression has two types: the type of its source and the type of its target. The notation is used to indicate that expression e has source type and target type. Expressions in kappa calculus are assigned types according to the following rules: In other words,
Var: assuming lets you conclude that
Id: for any type,
Bang: for any type,
Comp: if the target type of matches the source type of they may be composed to form an expression with the source type of and target type of
Lift: if, then
Kappa: if we can conclude that under the assumption that, then we may conclude without that assumption that
The type can be regarded as the unit type. Because of this, any two functions whose argument type is the same and whose result type is should be equal – since there is only a single value of type both functions must return that value for every argument. Expressions with type can be regarded as "constants" or values of "ground type"; this is because is the unit type, and so a function from this type is necessarily a constant function. Note that the kappa rule allows abstractions only when the variable being abstracted has the type for some. This is the basic mechanism which ensures that all functions are first-order.
Categorical semantics
Kappa calculus is intended to be the internal language of contextually complete categories.
Examples
Expressions with multiple arguments have source types which are "right-imbalanced" binary trees. For example, a function f with three arguments of types A, B, and C and result type D will have type If we define left-associative juxtaposition as an abbreviation for, then – assuming that ,, and - we can apply this function: Since the expression has source type, it is a "ground value" and may be passed as an argument to another function. If, then Much like a curried function of type in lambda calculus, partial application is possible: However no higher types are involved. Note that because the source type of is not, the following expression cannot be well-typed under the assumptions mentioned so far: Because successive application is used for multiple arguments it is not necessary to know the arity of a function in order to determine its typing; for example, if we know that then the expression is well-typed as long as has type and. This property is important when calculating the principal type of an expression, something which can be difficult when attempting to exclude higher-order functions from typed lambda calculi by restricting the grammar of types.
History
Barendregt originally introduced the term "functional completeness" in the context of combinatory algebra. Kappa calculus arose out of efforts by Lambek to formulate an appropriate analogue of functional completeness for arbitrary categories. Hasegawa later developed kappa calculus into a usable programming language including arithmetic over natural numbers and primitive recursion. Connections to arrows were later investigated by Power, Thielecke, and others.
Variants
It is possible to explore versions of kappa calculus with substructural types such as linear, affine, and ordered types. These extensions require eliminating or restricting the expression. In such circumstances the type operator is not a true cartesian product, and is generally written to make this clear.
