почитал и не понимаю, почему это преподносится как спасение от проблемы импредикативности. По-моему, слишком ad hoc и unprincipled
+50
Реализация ad hoc, но она покрывает многие примеры, которые, как ожидается, будут нужны на практике. К сожалению, этот тезис невозможно проверить, пока её (импредикативность) собственно не начнут использовать достаточно широко. Так что поживём — увидим. Реализация не должна сильно волновать пользователя. Проблема в том, что предыдущие подходы или требовали введения абсолютно новых сущностей (разных видов типов) или переписывания пол компилятора (так было в Guarded Impredicativity). Текущая идея не требует ни того ни другого, поэтому ей и был дан зелёный свет.
Обсуждают сегодня