Немного Мадхьямики в MLTT сеттинге

В тибетской традиции есть такое понятие — Дхармадхату — пространтсво всех Дхарм. Это пространство всех мыслей которые существуют вне контекстов. Представить сложно — понятное дело. Но у нас есть MLTT теория которая поможет это представить.

Представьте себе пространство всех языков программирования — понятно дело все знают про лямбда исчисление. Но не многие же рубисты или ПХП программисты задумываются, что они пишут на языке пространства — которое с точностью до битов моделируется теорией типов Мартина Лефа (надо только вселенные правильно отконфигурировать, это научились делать в 2001 году, когда Coq все дружно писали). Конечно я сам в это по началу не верил, и думал что есть все-таки ограничения и что Данила Мастер, который вручную все сам делает вместо того чтобы экстрактить это из Инфинити Топоса делает ненапрасный труд. Мне пришлось написать прувер чтобы понять — таки да, каждый Данила Мастер, который считает себя инженером — производит временный и бесполезный труд, давая ярлыки феноменам не видя их сути.

Пространство типов безгранично и все типы одновременно живут в этом бесконечномерном пространстве — где каждое его измерение наслаивается друг на друга, а сами типы образуют паттерны, похожие на гомотопические группы. Так как изоморфных типов в пространстве бесконечного топоса хватает, то в MLTT тоже есть что-то похожее на матрицу гомотопических групп. Они имеют разные имена и могут в принципе не проходить чеканье на равенство и т.д., но при компиляции в нетимизированную лямбду изоморфные типы будут генерировать совместимый код.

У всех типов есть четкая логика заселения пространства бесконечного топоса, подобно тому как жители самсары заселяют шесть лок. Начинается все с нижнего дна ада — Bottom типа. И потом по кирпичику начиная с Unit (), потом A -> A, потом Nat, потом Stream, потом List, потом ... и так далее вплоть до инфинити-групоида, потом все начинает повторятся и узор начинает меняться. Где у этого узора дырки я пока не вижу, и какая у него структура, но как бы чувствую немного дыхание этой мандалы. Эта мандала доступна впринципе всем программистам, которые могут писать циклы, складывать числа, больше уровня не нужно. Всю эту математику можно переформулировать так, чтобы MLTT преподавать 11 летним детям — считайте, что эксперимент начат.

Не многие знают, что имя линии передачи, которую мы официально представляем в Киеве, называется Лонгчен Ньингтик. KLONG по тибетски — это пространство, пространство всех феноменов, KLONG CHEN NYING THIG обширное пространство сердечной сущности. Так же как Инфинити Топос — это пространство всех MLTT типов, которое объединяет континуум и дискретное, а также проглатывает всю математику со всеми ее логиками и теориями, так как все математики разговаривают уже давно на этом языке кванторов и бесконеченых вселенных.

Так вот, точно также как все языки рождены из этого пространства, так же и мысли все рождаются из одного пространства, и все они проименованы, точно также, как проименованы все типы во всех вселенных. Рождаются тут условно, так как List не рождается, его можно обнаружить понять, но он всегда присуствует в Топосе во всех уровнях вселенных. Все типы являются несозданными, пока их не объявит программист в виде аксиом MLTT. Но если их рассматривать через призму нечистого видения — нетипизированного лямбда исчисления, то рассмотреть их не получится или очень сложно (Алонсо Черч и Боем с Берардуччи не смогли этого сделать). Ну а аналогия просветления — это выход в эту мандалу, где видны все типы сразу, или куда не кинешь взор, видишь везде похожие паттерны. Послушай функциональный программистов — натуральные же шизофреники, видят какие-то катаморфизмы там, где обычный человек видит while или for; видят группы, там где обычный человек видит record; чему обычные инженеры дали уже тысячу ярлыков. Знаете есть такое в духовных практиках быть остраненным и не вешать ярлыки на феномены, потому что это бессмылсенно. Это тоже самое что List/Cons и Stream/Mk — миллионы програмистов дали разныне названия этим штукам, но штуки эти существуют сами по себе и увидеть их можно при индуктивном рассмотрениии заполнения пространства типами начиная с Unit, и сделать это можно начиная уже с третьего шага.

Вообщем аналогии настолько прочные, что я могу в священных тибетских текстах заменять Дхармадхату на "Инфинити Топос", SEMS или Ум на "правила вывода" (кстати один из переводов SEMS — это вычислитель) или на "компютешинал аксиомы", CHOS или DHARMA (Феномен) на Тип и ничего почти не изменится. Процесс мышления — это то как вы конструируете теоремы, как вы выстраиваете рекурсивные цепочки, т.е. как вы композируете мысли (рекурсия и индукция). Если у типа нет рекурсора, значит вы не можете пустить мысль по этому феномену. А пустить мысль по феномену означет его осознание т.е. освобождение в дхармакае, что впринципе соотвествует этимологии слова элиминатор.

Пора положить конец спорам различных школ Мадхьямики (модели сватантрик) и описать все эти логики в виде MLTT программ.