Hask, preliminary

zeit_raffer — 07.08.2016 (уже несколько лет, как я заинтересовался вопросом, хожу по блогам и спрашиваю воздух - а какое равенство в Hask? вы где-нибудь видели, как оно определяется?)

Сейчас произошел вброс на высшем уровне http://math.andrej.com/2016/08/06/hask-is-not-a-category/

Только я бы различал вопросы. Необходимость построения полной операционной семантики для дефолтно-ленивого языка это одно (она, возможно, будет сложна, чтобы описать мемоизацию, в том числе). А другое - это синтаксическая категория, которая просто состоит из термов, и ни о какой семантике не знает. Автор того блога связывает эти вопросы через обсервационную (наблюдаемую) эквивалентность, но это совсем не обязательно.

Вобщем я решил стартовать с самого простого варианта, пока даже без ленивости. Так что это будет не Хаскелль, а, допустим, фрагмент Идриса без зав-типов, с System F. Не будет кучи "расширений", все изображено компактно. В следующей версии добавим опциональную ленивость. Будет undefined. Ужасного seq не будет, поскольку это костыль для достижения неленивости в изначально ленивом мире. В неленивом мире seq не нужен. Тьюринг-полноты пока не будет, но мы над этим работаем.

И еще. В посте по ссылке обыгрывается глагол pretend. Привычная Hask pretends быть категорией, но не определена достаточно хорошо. Та категория, которую я сейчас опишу, pretends на соответствие Хаскеллю, но слишком хороша для него. И даже наоборот, я бы сказал, реальный Хаскелль - это инженерное решение, стремящееся в идеале соответствовать ей.

Оставить комментарий

Популярные посты:

• Ранее
• Архив