Part I: Basic typed languages
We're going to speak about typed languages. By language I mean a grammar that defines what an expression in this language is. By typed I mean there is a rule to figure out when expression makes sense in a given context Г.
The most basic typed language is the composition calculus. It's a language where whenever we have two transitions f: A => B and g: B => C we can compose them and get g f: A => C.
expr ::= identifier | identifier expr
– Context Г is a set of pairs (identifier: Type => Type)
– Expression is well-typed iff it contains only identifiers available in the context and types of adjacent identifiers in the expression match.
– Every context contains identifiers id[T]: T => T (the "do nothing" transitions) for every type T.
It's the most basic typed language for it is present in any category C of types and transitions between them. All other langages are available only in categories with additional structures or properties.
For example, iff the category has a terminal object Unit (i.e. we have a new family of identifiers cancel[A]: A => Unit which are the only transitions into the Unit type), the same language turns out to be composition-application language. The transitions v: Unit => T are called values of type T. We'll write =>T instead of Unit => T for better readability. If we compose a transition f: A => B and value v: =>A, we get a (f v): =>B, a value of type B. So from the POV of a category theorist, application is a special case of composition, not the other way round. It seem very unnatural but there are very good reasons to do so.
Closed calculus is a typed language, where transitions are values too.
It is, for any pair of types (A, B) we have a type constructor (A => B) and in the language we have two "lift"-operators:
abstraction turns a transition f: A => B into (K f): =>(A => B) and
application f(x) that applies abstracted transition f: =>(B => C) to transition x: A => B
The grammar becomes:
expr ::= identifier | identifier expr | K expr | expr(expr)
1) We can abstract and deabstract every transition f: A => B this way: (K f)(id[A]) = f
2) We can express value-level composition, i.e. if we have two abstracted transitions f: =>(A => B) and g: =>(B => C), we can produce their abstracted composition: K g(f(id[A])): =>(A => C)
3) The most distinctive feature of this language is the ability to represent functions of multiple arguments:
f: A => (B => C)
g: A => (B => (C => D))
For a: =>A, b: =>B and c: =>C, that's how we apply them:
(f a)(b): C
(f a)(b)(с): D
Closed calculi are available in closed categories. You should not think that all reasonable calculi are closed! Consider the category of typed streams and stream transformers. A stream transformer is not a stream, so the category is not closed. So are calculi for digital electrical circuits with typed interfaces, calculi for quantum computations and so on.
Simply typed lambda calculus is a closed calculus where we can construct functions that use their argument multiple times. In generic closed calculus we can have a function sum: N => (N => N), but cannot make function twice(x) = sum(x, x) out of it.
To make it possible, we'll introduce a new operator S, generalised value-level composition. Recall that value level composition normally makes h: =>(A => C) out of f: =>(A => B) and g: =>(B => C). The generalized form makes (g S f): X => (A => C) out of f: X=>(A => B) and g: X=>(B => C). The idea is that f is a function from A to B that additionally depends on ‘environment variable’ of type X, and so is g. (f S g) produces another ‘environment-dependent function’ that first delivers copies of environment to f and g and then composes them: (f S g) x = (g x)(f x)
Simply-typed lambda calculus is the language available in cartesian-closed categories.