Велокайф или по стопам Демосфена

Ыыы! Уже несколько лет у меня не было никакого прогресса в качестве веловождения. А вот сейчас я случайно открыл технику, которая дала немедленные результаты. У меня в макдаке остался недопитый поллитровый стакан колы. Выливать жалко, пить не хочется. И тут мне пришло в голову: что если просто поставить этот стакан на багажник велосипеда и попробовать прямо так поехать?

И я попробовал. Это класс! Мозг помнит о стакане колы и прикладывает все усилия, чтобы избегать горизонтальных ускорений. Тормозишь плавно, как в масло, выходишь из наклона в повороте, как аэробус под управлением опытного пилота. Пристально смотришь на дорогу, чтобы объезжать малейшие неровности. В начале я ехал медленно, потом приноровился и вышел на вполне крейсерские 22 км/ч. Проехал в общей сложности чуть больше трёх километров таким макаром. Мозг даже как-то отдохнул от такой смены деятельности.

“Наберите в рот камней, а затем артикулируйте, как обычно”

Кортежи и enum-типы в лямбда-исчислении

Коль скоро я в прошлом посте написал про теоретико-множественное представление пары, стóит, наверное, рассказать и про лямбда-исчисленческое представление и, заодно, про представление типов-перечислений.
Сразу предупрежу, лямбда-термы я люблю записывать вот так: [x|f(x)]. Вертикальных черт может быть несколько: [x|y|f(x,y)] = λx.λy.f(x,y).

Итак, кортеж представляется следующим образом:
(a, b) = [f|f a b]
(a, b, c) = [f|f a b c]
...

Операторы проекции применяются справа и обозначаются .1, .2 и так далее. Операторы проекции пар, троек и кортежей другой арности различаются:

.1(2) := [a|b|a] .2(2) := [a|b|b]

.1(3) := [a|b|c|a] .2(3) := [a|b|c|b] .3(3) := [a|b|c|c]

...

Несложно увидеть, что (a, b).1 = a,   (a, b).2 = b и так далее.

При использовании типизированного лямбда-исчисления верхний индекс как правило можно опускать, т.к. он однозначно определяется из контекста.
Лямбда-выражения, соответствующие кортежам и проекциям, не могут быть статически типизированы, поэтому в типизированных (первого порядка) вариантах лямбда-исчисления, они наделяются особенными типами: кортежи имеют тип A × B × ... × C, где A, B, ..., C — типы элементов кортежа, а операторы проекции арности n выделяют в специальный тип, обозначаемый n.

В основанных на лямбда-исчислении прикладных языках обычно вводится синтаксическая глазурь: можно объявлять типы-перечисления
Axis := #{x. y, z}
и именованные кортежи
point := (x: 1, y: 2.5, z: 0).
Представителями типа Axis в таком случае являются проекции .x^(Axix), .y^(Axix) и .z^(Axix), которые можно применять к именованным кортежам: point.x = 1. На деле эта синтаксическая глазурь преобразуется в обычные нумерные типы и проекции:
Axis ≡ 3,
point ≡ (1, 2.5, 0),
.z^(Axix) ≡ .3⁽³⁾.