Alexander Kuklev (akuklev) wrote,
Alexander Kuklev
akuklev

Gentle introduction to DOT, part I

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

  • Прогресс

    Десять дней назад, вторая ступень SpaceX'овского корабля Starship своим ходом слетала своим ходом на десять километров вверх, и усмепшно приземлилась…

  • О водосбережении

    Как известно, питьевая вода во многих странах дефицитный ресурс. И даже в дождливой Германии летом иногда случаются засухи, в результате которых она…

  • 36

    Традиционный деньрожденный пост. Год выдался необычный. :)

  • Post a new comment

    Error

    default userpic

    Your reply will be screened

    Your IP address will be recorded 

    When you submit the form an invisible reCAPTCHA check will be performed.
    You must follow the Privacy Policy and Google Terms of use.
  • 4 comments