ага

я почему-то когда слышу про это все время вспоминаю гошников с их гениальным обоснованием корутин.

Любой боттом, Hask тьюринг-полный, поэтому в любом типе целое счётное количество значений (всевозможных бесконечных циклов, условно)

Я думал Hask от Set тем и отличается что там боттомы не считаются

Ну это тогда совсем не категория получится, хаскель же ленивый, нельзя просто взять и выкинуть боттомы

Легко придумать нормализующийся терм, имеющий ненормализующийся подтерм

Я думаю, что Вам нужно взять какой-нибудь тотальный язык, тогда таких проблем не будет. Например доказать, что в System F, (foral a.a ->a) населён только одним термом

Hask от Set гораздо большим отличается, в Hask нет произвольных лимитов, колимитов, бесконечных произвольных сумм и произведений , а самое главное, subobject classifier

Надо написать всё-таки пост о том, что Hask это DCPO-enriched категория

Это очень неочевидно, что в Hask нет subobject classifier. По-моему если TypeInType включить, то есть

Боюсь глупость сказать, но мне казалось, что наличие subobject classifier означает разрешимость любого proof irrelevant свойства. Думал, что в Hask, где морфизмы - вычислимые тотальные функции это будет противоречить какой-то теореме Гёделя

Ну я всяческий противник смотреть на Hask как на категорию, где морфизмы - вычислимые тотальные функции потому что это невозможно :)

На днях в хаскеляч залетел фанат Idris'а. Замечу, что любые попытки построить тьюринг-полный язык с тотальным подмножеством, основанном на MLTT, должны вызывать справедливый интерес haskell-коммьюнити, а чаты по идрису и хаскелю в значительной мере пересекаются. Естественно в дискуссии всплывал вопрос о целесообразности ленивой стратегии редукции. Кроме стандартных аргументов в духе "это сложно и не нужно" всплыл ещё один, претендующий на объективность и достоверность.
 Утверждалось, что ленивая стратегия редукции -- основная причина сложности построения денотационной семантики хаскеля, основанной на теории категорий. Но так ли это?
 По языку программирования мы хотим построить такую категорию, что каждому типу будет соответствовать объект категории, а каждой функции из A в B -- соответствующую стрелку. При этом мы хотим, чтобы функциям f,g :: A-> B соответствовали одинаковые стрелки тогда и только тогда, когда для любого a из A f(a) = g(a)
 Сложность наступает как только мы берём тьюринг-полный язык. Ведь далеко не все функции останавливаются! Как приравнять функции, которые работают бесконечно долго? Есть два выхода из этой ситуации. Оба работают только для языков с энергичной редукцией. Первый -- просто выкинуть нетотальные функции из категории, сделать вид что их просто нет. Естественно при этом теряется всякая доказательная сила рассуждений об этом языке с помощью теории категорий, ведь о частичных функциях мы не может сказать вообще ничего.
Второй -- "добавить" внутрь типа специальный элемент _|_ и сказать, что дополнить f(a) = _|_, если она f(a) не останавливается. Так мы получим корректное равенство на стрелках, но что будет, если мы начнём над этой категорией рассматривать эндофункторы и интерпретировать их в терминах computer science? Ничего хорошего: ведь мы можем легко переводить тотальные функции в нетотальные и наоборот, информация о том кто из них кто абсолютно теряется. Мы столкнулись с той же проблемой, что и в первом случае, но подошли с ней с другой стороны.
Резюмируя: корректной категориальной денотационной семантики не может быть ни у одного тьюринг-полного языка. Но что же делать со всеми наработками в этой области? Ведь на практике они работают. Чуть позже я постараюсь сделать наброски ответа на него

Я же про это писал :)

Скоттненько :-)

Я, кстати, не знаю что лучше — internal in DCPO или DCPO-enriched брать

Но кажется, что с enriched больше стандартных инструментов работать будет

Обогащённая чуть попроще и работать попроще.
Но не всегда хватает.

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

Привет всем! Извиняюсь если не в тему. Как переводятся на русский fibration и bundle?