Hask, preliminary

Сейчас произошел вброс на высшем уровне http://math.andrej.com/2016/08/06/hask-is-not-a-category/
Только я бы различал вопросы. Необходимость построения полной операционной семантики для дефолтно-ленивого языка это одно (она, возможно, будет сложна, чтобы описать мемоизацию, в том числе). А другое - это синтаксическая категория, которая просто состоит из термов, и ни о какой семантике не знает. Автор того блога связывает эти вопросы через обсервационную (наблюдаемую) эквивалентность, но это совсем не обязательно.
Вобщем я решил стартовать с самого простого варианта, пока даже без ленивости. Так что это будет не Хаскелль, а, допустим, фрагмент Идриса без зав-типов, с System F. Не будет кучи "расширений", все изображено компактно. В следующей версии добавим опциональную ленивость. Будет undefined. Ужасного seq не будет, поскольку это костыль для достижения неленивости в изначально ленивом мире. В неленивом мире seq не нужен. Тьюринг-полноты пока не будет, но мы над этим работаем.
И еще. В посте по ссылке обыгрывается глагол pretend. Привычная Hask pretends быть категорией, но не определена достаточно хорошо. Та категория, которую я сейчас опишу, pretends на соответствие Хаскеллю, но слишком хороша для него. И даже наоборот, я бы сказал, реальный Хаскелль - это инженерное решение, стремящееся в идеале соответствовать ей.
|
</> |