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