Категорические вычисления

А вот можно ли вычислить ответ на главный вопрос, пользуясь одной лишь теорией категорий? Оказывается, можно. Давным-давно в одной далекой галактике Tatsuya Hagino придумал язык CPL (Categorical Programming Language), а чуть менее давно другой японец Masahiro Sakai сделал годный его интерпретатор. Hagino свою реализацию делал на Лиспе, а Sakai догадался таки задействовать языки программирования - сперва Руби, затем Хаскель (ибо Руби медленный, на Хаскеле в сто раз быстрее заработало). И вот полный текст программы на CPL:

right object 1 with !
end object;

right object prod(a,b) with pair is
  pi1: prod -> a
  pi2: prod -> b
end object;

right object exp(a,b) with curry is
  eval: prod(exp,a) -> b
end object;

left object nat with pr is
  zero: 1 -> nat
  s: nat -> nat
end object;

let add=eval.prod(pr(curry(pi2), curry(s.eval)), I);
let mult=eval.prod(pr(curry(zero.!), curry(add.pair(eval, pi2))), I);
let h = mult . pair(s, I);
simp h.h.h.s.zero;

которая выводит результат
s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.s.zero
т.е. ровно 42.

Что же тут происходит? ( Read more... )