В тибетской традиции есть такое понятие — Дхармадхату — пространтсво всех Дхарм. Это пространство всех мыслей которые существуют вне контекстов. Представить сложно — понятное дело. Но у нас есть 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 программ.

http://maxim.livejournal.com/479716.html

Ребята пишут про какой-то паттерн матчинг настоящий :-)
Про итеграцию и то, что это было в лиспах (ну не в лиспах, а в ACL2 — это все же не лисп). Ну и понятное дело все это пишут ебанаты, код которых так воняет по всему интернету что даже из гитхаба его удаляют :-) Невозможно понять как работает паттерн мачинг, если вы не поняли как раотает оператор J. Я написал за свою жизнь около 15 языков. И поверьте любые ваши попытки написать свой язык, в котором нет зависимых типов и бесконечного счетного количества вселенных — навсегда остануться костылями, которые никогда не будут восприниматься более-менее здоровыми психически людьми как нечно стоящее. Потратьте хотябы несколько лет в медитации, чтобы понять что А) мы (Групоид Инфинити) не занимается хуйней и Б) вы занимаетесь хуйней.

Originally posted by justy_tylor at Об универсальных языках программирования/моделирования 1
В начале века я ещё считал, что прогресс технологий работы с информацией сильно сдерживается существующими языками программирования, но достаточно заменить C++ чем-то более развитым по части функциональщины и метапрограммирования (но сохраняющим возможность генерации оптимального нативного кода), чтобы стало легко и удобно разрабатывать продукты любой сложности, уделяя внимание только проблемам предметной области, но не ограничениям предыдущего поколения инструментов. Был юный и тупой.

Замена отдельных языков более продвинутыми их аналогами чуть улучшает возможности записи отдельных программных фрагментов продукта. Но никак не облегчает их интеграцию, не позволяет избежать разноязыкового дублирования кода между. Иногда даже усложняет интеграцию, если увеличивается количество языковых представлений используемых моделей данных.

Можно сделать язык с полноценной реализацией pattern matching (а не как принято сейчас). С паттернами и комбинаторами в качестве первоклассных сущностей языка. И это уже польза. Однако.

Для определённых типов данных эффективнее создание индексов вместо полного перебора веток. Появляется выбор, либо через удобный pattern matching, либо через ручное решение с индексами. Ложный выбор. Средства метапрограммирования языка должны позволять создание подобных индексов в pattern matching, сочетая удобство написания и эффективность работы. И это ещё полезнее. Однако.

В реальном мире код работает не только с разными видами процессоров, памяти и периферии. Код работает с другим кодом. И существует множество информационных систем, где, например, выражения из паттернов/комбинаторов для регистрации на какие-то события указываются через XML-конфиг, а потом придумываются дублируемые идентификаторы, связывающие их с неким исполняемым кодом (часто тоже не нативным). И да, люди, создающие системы с ручным редактированием XML, достойны перерождения в виде жаб в Бангалоре. Но это не отменяет необходимости интеграции с такими системами. И здесь даже нет выбора. Только через конфиг. Хотя... Ведь и его можно сгенерировать. Ещё одна возможность трансляции pattern matching: что слева - в конфиг, что справа - в код.

То есть, язык, решающий проблемы разработки, должен решать проблемы интеграции. Поддерживать в процессе компиляции как пользовательские compile-time алгоритмы, так и описания таргетов из пользовательских библиотек. Здесь конфиг, там HTML, а кому-то вообще кусочек COBOL на мейнфрейм сгенерировать надо.

Но зачем тогда вообще писать что-то на COBOL (Java, C++, SQL, XML, bash, make, whatever...), если это можно сгенерировать из единой исполняемой спецификации, гарантируя отсутствие расхождений на стыках языков? Да, всё так, они оказываются лишь артефактами старых систем. Настоящий язык программирования должен быть универсальным, и заменить сразу все неуниверсальные. Что не значит, что он будет единственным (таким). Будут и другие универсальные, возможно (точнее: когда-то) лучше.

Что мне с этого? Вот уже несколько лет занимаюсь разработкой такого языка. И до представления работающего продукта ещё многое надо сделать. И сейчас, куда как лучше по сравнению с началом, я понимаю, почему никто ещё не создавал ничего подобного, хотя предпосылки были и десятилетия назад. Об этом (в частности) - в следующих постах серии.

http://maxim.livejournal.com/480048.html

Краткая история монадологии

Лейбниц монады не сам по себе первый придумал. он чужое подхватил. прослеживается такая цепочка: «характеры» и «монадология» Лейбница — на основе монад Ди — на основе «образов и мест» искусства памяти Джордано Бруно, герменевтиста, гностика и «христианского мага», художника и скульптора памяти, рисующего в душе и памяти (ср. диалог из «Теней»). искусство памяти Джордано Бруно — естественно основывается на луллизме (Раймонд Луллий), в противовес рамизму (Ramus) и схоластам, «педантам-грамматикам» и «антиаристотелю». далее машина с вращающимися кругами Р. Луллия для «распознавания образов» (наивный байесовский классификатор) через «театр памяти» Камилло и «тени идей» и францисканцы, далее до древней Греции и античности и досократиков — риторов (Федр, симонид и прочие киники, стоики и т.п.).

кстати, пифагоровы тела и многогранники; и платоновы идеи, и идея о том, что единица — основа всего. от этой божественной единицы один шаг до монады как «моноида в категории эндофункторов» и моноида := <множество объектов;нейтральный элемент, или единица моноида; композиция, или умножение в моноиде> .

есть мнение, что платон опять же не сам это придумал. а из египтян (см. диалоги «Тени» и «Печать Печатей» от Джордано Бруно — про «искусство внутреннего письма» ,«письма в памяти» и ругание Тота египетского Гермесом за то, что он изобрёл буквы — в результате чего «педанты-грамматики» разучились думать, и видят только форму схоластов, но не содержание образности. смотрят в книгу, а видят фигу).

читаем про египтян — представляем их учителей, то есть, атлантов, или гипербореев (до раскола на фракции).

Лейбниц же рулез прежде всего по трём причинам:

1. изобретение двоичной системы исчисления и калькулятора.
2. от «единицы как основы всего» двоичной один шаг до единицы моноида и алгебаических многочленов: гиперкомплексных и p-адических чисел; однако этот шаг он не делает, а делает шаг в сторону
3. в сторону «исчисления характеристик» для распознаватора образов и класификатора, а также «энциклопедии в исчислении характеристик» — то есть, по сути — гипертекста

«исчисление характеристик» он не доделывает до ума и полноценной теории котиков категорий; однако на этом пути он изобретает четвёртое
4. всеми нами любимый матанализ через дифференциальное исчисление, вариации бесконечно малых — просто и понятно, а не громоздко и нелепо — как Ньютон Исаак через «исчисление флюксионов».

вообще Ньютон в «математических началах философии, в натуре» пишет как типичный педант-грамматик, схоласт (это его «абсолютное время, в первом, математическом смысле» — например).

это он самый, а также Ф. Бэкон вкупе с Рене Декартом и его «Размышлениями о методе» в ответ на «отчёт о методах искуссвтва памяти», или «отчёт о методе» — виноваты в антиантиаристотилевщене, антидиксоновщине.

в том что «научный метод» схоластов и педантов-грамматиков (рамистов) вытеснил «искусство памяти» Джордано Бруно и «театр теней идей и образов» Камилло.

в том, что теория категорий опоздала в развитии лет на 300 и вместо образности искусства памяти «внутреннего письма» в прикладной метамагии и переносе инвариантов и теорем между когерентными теориями — и в итоге, в вашей альтернативной реальности победил «научный метод» схоластов и метанаука вместо метамагии

>>847290
Ты говорил, что в хаскеле нет категорий, вот черным по белому

>The main category we'll be concerning ourselves with in this article is Hask, which treats Haskell types as objects and Haskell functions as morphisms

Ты говорил, что в хаскеле функторы - это вообще не то, вот черным по белому

>The Functor typeclass you have probably seen in Haskell does in fact tie in with the categorical notion of a functor.

И еще

>Functors provide a good example of how category theory gets translated into Haskell. The key points to remember are that:

We work in the category Hask and its subcategories.

Objects are types.
Morphisms are functions.

Things that take a type and return another type are type constructors.

Things that take a function and return another function are higher-order functions.

Typeclasses, along with the polymorphism they provide, make a nice way of capturing the fact that in category theory things are often defined over a number of objects at once.

>Monads are obviously an extremely important concept in Haskell, and in fact they originally came from category theory. A monad is a special type of functor, from a category to that same category,

Ты говорил, что от паскаля это ничем не отличается в плане категорий, давай приводи примеры паскаля с монадами, функторами и композицией морфизмов

Ты либо унылый троль, либо тупой