Infinite Sheldon

Posted on February 24, 2020
But, said Alice, if the world has absolutely no sense, who’s stopping us from inventing one?
—Lewis Caroll, Alice in Wonderland

Разрешите представить:

Что интересного в этой функции? Много чего, но начнем пожалуй с того что это не функция. Давайте разберем как работает эта модель.

Выглядит как функция от одного аргумента - a. В теле модели видим объявление:

Похоже на функцию которая принимает два аргумента - self и a и затем вызывает self, т.е. предполагается что self - функция. Выглядит как обычная fixpoint обвязка. Но давайте посмотрим - что же у нас передается под символом self? Это первый аргумент вызова (вторая строка apply) и это действительно функция (по крайней мере похожа):

Хм. То же самое что и в первой строке. Это действительно похоже на fixpoint, но есть отличие. Видя модель (вторая строка) мы можем понять что имеем дело с partial apply (первая строка), так как аргументов у модели - два (self и a) а передается только один - self.

Что происходит при partial apply? Освежить знания можно здесь, если в двух словах - возвращается новая функция, у которой в аргументах будут только те переменные которые не были указаны в partial apply, а все что было указано - будет спрятано в теле модели.

Следовательно self self вернет модель вида:

Интересно. Это именно то с чего мы начали. Получается что это функция возвращающая саму себя, независимо от того какой аргумент мы ей передали. Причем это не бесконечно выполняющаяся функция, она строго завершается на любом вызове. Ок.

Но если это функция - то какой у нее тип? Да без проблем - мы видим что можем передать ей что угодно, то есть область определения у нее - *. А область значений?

Ну она возвращает сaму себя. То есть значение одно (что то вроде unit ) Ок. Но если возвращается функция - то какой тип у возвращаемой функции? Да такой же. На входе *, а на выходе функция. А какого типа функция? И так до бесконечности.

При попытке записать тип этой модели получаем:

Получаем модель которая на любое значение возвращает саму себя и которая при попытке прочитать ее как функцию не типизируется.

Только не путайте её с Y-комбинатором из λ-calculus.

Y-комбинатор для терма X - это такой Y что YX = X (YX)

Fixed point для функции F - это такой X что FX = X

В данном случае у нас FX = F, что значит что Infinite Sheldon - это не комбинатор неподвижной точки, это и не сама неподвижная точка.

Выглядит как интересная безделица, но при моделировании state машин и IO мы еще к ней вернемся.