bamalip: (NGE)
Зачастую попытки втиснуть в 1-категорию информацию о разных уровнях приводят к запутанной структуре. Опишем структуру на 2-категории, идеальным образом задающую язык с типами SystemF и тайпклассами. В следующих версиях попытаемся это описание улучшить (прежде всего, ленивость). Все 2-категории с такой структурой можно считать моделями нашей теории типов (все вместе они образуют большую 3-категорию), а инициальную из них можно называть синтаксической категорией - все элементы последней будут описываться деревьями-словами соответствующего языка, на ней будут выполняться обобщенные бесплатные теоремы, и даже рекурсор у нее будет, как в лучших домах Лондона, Парижа и Филадельфии.

Чтобы понимать прагматику, мы скажем, что объекты нашей произвольной 2-категории описывают тайпклассы (каждый с параметром из некоторого кайнда). Выделен один фиксированный объект Type, он же *, означающий базовый кайнд всех типов (с пустым тайпклассом). Наша 2-категория должна иметь конечные произведения и быть декартово замкнутой, что сразу порождает остальные кайнды. Type должен иметь конечные пределы, копределы, быть декартово замкнутым (это простые алгебраические типы). Задана операция перехода к дуальному объекты (прагматика такая, что каждый тайпкласс означает категорию и мы хотим менять стрелочки) (TODO - вместо этого можно рассматривать отдельно профункторы).

Для порождения тайпклассов мы возьмем операцию взятия категории диалгебр на профункторе, вернее, интернализованную версию (TODO - упростить/обобщить до "взвешенных 2-пределов"). В принципе, можно считать предыдущую операцию опциональной, рассматривая тайпклассы как сахар; это соответствует разделению языка на верхний (с тайпклассами) и нижний (без них).

Кванторы на типах. Это сопряженные 1-морфизмы к константному A->(A^B). (TODO - проверить выразимость всех расширений Кана и поменять эту аксиому на них). Фактически это пределы (т.е. мы реализуем часть бесплатных аксиом).

Минимальная и максимальная неподвижные точки функтора. Вычисляются через кванторы.

Основной эффект ленивости: изоморфность минимальной и максимальной неподвижных точек. (TODO: усложнить утверждение, добавив явную ленивость, и ограничив аксиому только ленивыми (lifted) типами).

И всё, больше ничего не надо! Эквациональные рассуждения прилагаются бесплатно.
bamalip: (NGE)
(уже несколько лет, как я заинтересовался вопросом, хожу по блогам и спрашиваю воздух - а какое равенство в Hask? вы где-нибудь видели, как оно определяется?)

Сейчас произошел вброс на высшем уровне http://math.andrej.com/2016/08/06/hask-is-not-a-category/

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

Вобщем я решил стартовать с самого простого варианта, пока даже без ленивости. Так что это будет не Хаскелль, а, допустим, фрагмент Идриса без зав-типов, с System F. Не будет кучи "расширений", все изображено компактно. В следующей версии добавим опциональную ленивость. Будет undefined. Ужасного seq не будет, поскольку это костыль для достижения неленивости в изначально ленивом мире. В неленивом мире seq не нужен. Тьюринг-полноты пока не будет, но мы над этим работаем.

И еще. В посте по ссылке обыгрывается глагол pretend. Привычная Hask pretends быть категорией, но не определена достаточно хорошо. Та категория, которую я сейчас опишу, pretends на соответствие Хаскеллю, но слишком хороша для него. И даже наоборот, я бы сказал, реальный Хаскелль - это инженерное решение, стремящееся в идеале соответствовать ей.

UPD. 2-Hask, v0.1

Profile

bamalip: (Default)
шерстяной ленин

July 2017

S M T W T F S
       1
2 3 4 56 7 8
9 1011 12 13 14 15
161718 19 2021 22
23242526272829
3031     

Syndicate

RSS Atom

Most Popular Tags

Style Credit

Expand Cut Tags

No cut tags
Page generated Jul. 22nd, 2017 06:45 pm
Powered by Dreamwidth Studios