Observations

Стал искать, где бы понадыбать приятных теорем про CCC. Обнаружил, что а) CCC вообще никого не интересует, а интересует типизированный лямбда-калкулюс (хоть Барендрегта читай; который? Curry?) и б) единственная ссылка везде - это С.Соловьев, 1983. Я когда-то полагал, что Соловьев, конечно, классную тему поднял, но это было сильно по мотивам статейки Маклейна. А теперь Маклейна все забыли (ну только что в книге есть), а только Соловьев. Соловьева еле нашел, его даже на википедии нету; слава те господи, он в Тулузе, лямбду преподает в университете. Неплохо бы, конечно, заскочить к нему летом, если удастся.

Фигня какая-то получается. Посмотрю, какие из "аксиом CCC" следуют из ее категорного определения. Ну и BCCC, наверно, тоже надо впендюрить будет.

Но для меня сюрприз, что CCC - это чисто софтверное (или логическое) понятие.

И кстати, только что узнал, что CAML означает "categorical abstract machine language". Имея в виду ту же типизированную лямбду.

  def ×[A,B,C,D](f:A=>C)(g:B=>D): (A,B) => (C,D) = (a,b) => (f(a), g(b))

Big deal, right?