Зачем делать целую ОС, если не хватает каких-то интеграций? Шансы того, что она станет популярной и что кто-то будет под неё что-либо делать крайне малы. Если нравится сам процесс разработки — то нет вопросов, почему бы и нет.
Мне кажется, куда более реалистично придумать что-то вроде модуля ядра/сервиса для существующих ОС, в котором будут все нужные API, чтобы можно было интегрировать что угодно с чем угодно (и пересылать, например, сообщения из одного приложения в другое, реализовав абстрактное апи Сообщений).
… а затем каким-то образом убедить всех разработчиков приложений, что им это нужно. Но чтобы навязать стандарт, нужно колоссальное количество ресурсов и времени, куда большее, чем на разработку, но однозначно меньше, чем делать целиком новую ОС.
Потому что это такой способ выражения рекурсивных анонимных функций. Если функция имеет собственное имя, то проблемы с рекурсивным определением не возникает: в таком случае самоприменение выражается через это самое имя. Например, банальный рекурсивный факториал:
Все эти if, =, −, ×, 0, 1 можно считать сокращениями (макросами), которые на самом деле раскрываются в нормальные комбинаторы (замкнутые абстракции):
Но вот F уже таким образом не раскроешь, так как она обращается к некоей переменной F, которая ни с чем не связывается ни одной лямбда-абстракцией внутри её определения. Если у нас есть глобальное окружение, которое магическим образом свяжет переменную F с функцией F внутри определения функции F, то проблемы с её рекурсивным определением не будет. Иначе остаётся только ухищрение в виде Y-комбинатора.
Суть ухищрения в явном использовании так называемых продолжений. Обычно считается, что функция возвращает своё значение в абстрактный «наверх» — тому, кто хочет получить вычисленное значение функции. Можно этот возврат значения сделать явным, передавая функции A другую функцию B, которую A вычислит, передав ей результат собственного вычисления в виде аргумента. Например, вычисление (+ 1 (+ 2 3)) можно представить в виде (+ 2 3 λx.(+ 1 x •)). Здесь функция + тернарная: принимает два слагаемых и продолжение, которому она передаёт результат сложения. Как видите, результат сложения 2 и 3 передаётся следующей функции под именем x, где к нему прибавляется 1, а результат сложения передаётся в некий •, что обозначает дальнейшие вычисления.
Такая форма записи (стиль передачи продолжений) явно показывает порядок вычислений и является функциональным аналогом SSA-формы, использующейся как представление императивных языков. Помимо всех остальных плюшек она позволяет очень легко записать рекурсию: ведь если функции передать в виде продолжения эту же функцию, то для рекурсии уже не надо никаких магических глобальных окружений — рекурсивная функция будет замкнутой и у неё будет локальная переменная, через которую она сможет сделать «самовызов».
Итак, задача сводится к тому, чтобы вызвать произвольную функцию f с одним аргументом — функцией-продолжением, которая вызывает f. (Остальные аргументы можно передать с помощью упомянутого каррирования.) Введём для этого специальный комбинатор Y.
Кульбит №1. Изящный способ удовлетворить предыдущее требование — это определить Y так, чтобы он возвращал то же, что передаёт в f. Тогда рекурсивный вызов (f n) можно записать в виде ((Y g) n), где g = λfn.• — рекурсивная функция f, в которой все рекурсивные вызовы делаются через локальную переменную f. Таким образом, должно выполняться равенство:
Однако, по этой формуле нельзя понять, как записать Y в виде лямбда-терма, не используя Y. Собственно, формула кристаллизует проблему, возникающую при рекурсивном вызове.
Окей, ссылаться на некий глобальный Y, чтобы получить такой же Y мы не можем. Но это ограничение можно обойти, передав нужную функцию как аргумент! Запишем Y по-другому, через функцию X, которой передадим такую же функцию X (которая не ссылается ни на X, ни на Y):
Кульбит №2. X надо записать в виде лямбда-терма:
причём в нём нельзя ссылаться на X или Y, можно использовать только свою переменную x или свободную переменную f. Аргументом X может быть некоторый другой терм Z, который равен X с точностью до альфа-конверсии (Z — такой же X, только его переменная x переименована в z). Вот именно этот хитрый момент и позволяет осуществить «рекурсивный вызов», применяя одную анонимную функцию к другой, но «такой же» анонимной функции — для этого надо считать вызов эквивалентной функции эквивалентным рекурсивному вызову функции.
Идём дальше, теперь немного очевидных наблюдений:
Синтезировав эти наблюдения, можно заметить, что
Кульбит №3. Cледим за руками. Предыдущее равенство подставляем в первое очевидное наблюдение:
и в то же время
то есть
Кульбит №4. Какой должна быть функция эта функция X
чтобы предыдущее свойство выполнялось? Достаточно заметить, что X используется таким образом, что переменная x внутри неё всегда связана с X (а вернее, с некоей функцией, которая ведёт себя так же, как X). Маленькое напряжение ума и желаемое определение становится очевидным:
Теперь подставляем X в Y и получаем определение Y-комбинатора из палаты мер и весов:
Как этим пользоваться. Возьмём факториал:
и дополним его её одним аргументом — функцией, которая вычисляет факториал.
Теперь F' не имеет рекурсии. Это обычный комбинатор (после раскрытия всяких if). Отлично, но что передать ему первым аргументом? От этой головной боли Y-комбинатор и избавляет:
Теперь F — это функция, которая принимает одно число, и рекурсивно вычисляет факториал. Проверим, выполняя редукцию в нормальном порядке (всё не раскрываю, так как запутаться можно же):
Да-да, мы с Andrey2008 тоже отшучивались на эту тему. :)
Зачем делать целую ОС, если не хватает каких-то интеграций? Шансы того, что она станет популярной и что кто-то будет под неё что-либо делать крайне малы. Если нравится сам процесс разработки — то нет вопросов, почему бы и нет.
Мне кажется, куда более реалистично придумать что-то вроде модуля ядра/сервиса для существующих ОС, в котором будут все нужные API, чтобы можно было интегрировать что угодно с чем угодно (и пересылать, например, сообщения из одного приложения в другое, реализовав абстрактное апи Сообщений).
… а затем каким-то образом убедить всех разработчиков приложений, что им это нужно. Но чтобы навязать стандарт, нужно колоссальное количество ресурсов и времени, куда большее, чем на разработку, но однозначно меньше, чем делать целиком новую ОС.
Потому что это такой способ выражения рекурсивных анонимных функций. Если функция имеет собственное имя, то проблемы с рекурсивным определением не возникает: в таком случае самоприменение выражается через это самое имя. Например, банальный рекурсивный факториал:
Все эти if, =, −, ×, 0, 1 можно считать сокращениями (макросами), которые на самом деле раскрываются в нормальные комбинаторы (замкнутые абстракции):
Но вот F уже таким образом не раскроешь, так как она обращается к некоей переменной F, которая ни с чем не связывается ни одной лямбда-абстракцией внутри её определения. Если у нас есть глобальное окружение, которое магическим образом свяжет переменную F с функцией F внутри определения функции F, то проблемы с её рекурсивным определением не будет. Иначе остаётся только ухищрение в виде Y-комбинатора.
Суть ухищрения в явном использовании так называемых продолжений. Обычно считается, что функция возвращает своё значение в абстрактный «наверх» — тому, кто хочет получить вычисленное значение функции. Можно этот возврат значения сделать явным, передавая функции A другую функцию B, которую A вычислит, передав ей результат собственного вычисления в виде аргумента. Например, вычисление (+ 1 (+ 2 3)) можно представить в виде (+ 2 3 λx.(+ 1 x •)). Здесь функция + тернарная: принимает два слагаемых и продолжение, которому она передаёт результат сложения. Как видите, результат сложения 2 и 3 передаётся следующей функции под именем x, где к нему прибавляется 1, а результат сложения передаётся в некий •, что обозначает дальнейшие вычисления.
Такая форма записи (стиль передачи продолжений) явно показывает порядок вычислений и является функциональным аналогом SSA-формы, использующейся как представление императивных языков. Помимо всех остальных плюшек она позволяет очень легко записать рекурсию: ведь если функции передать в виде продолжения эту же функцию, то для рекурсии уже не надо никаких магических глобальных окружений — рекурсивная функция будет замкнутой и у неё будет локальная переменная, через которую она сможет сделать «самовызов».
Итак, задача сводится к тому, чтобы вызвать произвольную функцию f с одним аргументом — функцией-продолжением, которая вызывает f. (Остальные аргументы можно передать с помощью упомянутого каррирования.) Введём для этого специальный комбинатор Y.
Кульбит №1. Изящный способ удовлетворить предыдущее требование — это определить Y так, чтобы он возвращал то же, что передаёт в f. Тогда рекурсивный вызов (f n) можно записать в виде ((Y g) n), где g = λfn.• — рекурсивная функция f, в которой все рекурсивные вызовы делаются через локальную переменную f. Таким образом, должно выполняться равенство:
Однако, по этой формуле нельзя понять, как записать Y в виде лямбда-терма, не используя Y. Собственно, формула кристаллизует проблему, возникающую при рекурсивном вызове.
Окей, ссылаться на некий глобальный Y, чтобы получить такой же Y мы не можем. Но это ограничение можно обойти, передав нужную функцию как аргумент! Запишем Y по-другому, через функцию X, которой передадим такую же функцию X (которая не ссылается ни на X, ни на Y):
Кульбит №2. X надо записать в виде лямбда-терма:
причём в нём нельзя ссылаться на X или Y, можно использовать только свою переменную x или свободную переменную f. Аргументом X может быть некоторый другой терм Z, который равен X с точностью до альфа-конверсии (Z — такой же X, только его переменная x переименована в z). Вот именно этот хитрый момент и позволяет осуществить «рекурсивный вызов», применяя одную анонимную функцию к другой, но «такой же» анонимной функции — для этого надо считать вызов эквивалентной функции эквивалентным рекурсивному вызову функции.
Идём дальше, теперь немного очевидных наблюдений:
Синтезировав эти наблюдения, можно заметить, что
Кульбит №3. Cледим за руками. Предыдущее равенство подставляем в первое очевидное наблюдение:
и в то же время
то есть
Кульбит №4. Какой должна быть функция эта функция X
чтобы предыдущее свойство выполнялось? Достаточно заметить, что X используется таким образом, что переменная x внутри неё всегда связана с X (а вернее, с некоей функцией, которая ведёт себя так же, как X). Маленькое напряжение ума и желаемое определение становится очевидным:
Теперь подставляем X в Y и получаем определение Y-комбинатора из палаты мер и весов:
Как этим пользоваться. Возьмём факториал:
и дополним его её одним аргументом — функцией, которая вычисляет факториал.
Теперь F' не имеет рекурсии. Это обычный комбинатор (после раскрытия всяких if). Отлично, но что передать ему первым аргументом? От этой головной боли Y-комбинатор и избавляет:
Теперь F — это функция, которая принимает одно число, и рекурсивно вычисляет факториал. Проверим, выполняя редукцию в нормальном порядке (всё не раскрываю, так как запутаться можно же):