*Preliminaries: rudimentary knowledge of category theory and Scala syntax.*

**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.

Grammar:

expr ::= identifier | identifier expr

Typing:

– 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.