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

о, покажите мне этого фаната Идриса. прямо заинтересовали.

> I want to write object.methodName, not ModuleName.objectTypeMethodName object

а Object.methodName кто запрещает писать?

https://capnproto.org/news/2013-08-12-capnproto-0.2-no-more-haskell.html

а стыдно до сих пор

Я прочитал только резюме и первый абзац и понимаю, что вы с моим текстом сделали тоже самое 😆

> языки в поледние годы плодятся, как грибы например?

Аргумент 99 уровня. У Вас тоже

Вы изначально отказались обсуждать содержательно, сказав, что "не читали". каких ответных аргументов Вы ожидали?

Нет, я пошутил о том, что вы не осилили даже прочитать мою простыню

Нет, я пошутил о том, что вы не осилили даже прочитать мою простыню

"за двадцать лет аж 0" лол. я же говорю "закроем глаза". сейчас свои языки не пишет только ленивый.

а пурс это точно что-то новое? это не то, что хотел сделать автор disciple, но не осилил?

что-то не вижу перечисления

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

его и не обещалось. Вас в гугле забанили?

сколько здесь хаскелльного самомнения, прямо сочится и капает