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)
шерстяной ленин

September 2017

S M T W T F S
      1 2
3 4 5 6 7 8 9
1011 12 13 14 1516
1718 1920212223
24252627282930

Syndicate

RSS Atom

Most Popular Tags

Style Credit

Expand Cut Tags

No cut tags
Page generated Sep. 20th, 2017 02:06 am
Powered by Dreamwidth Studios