Как правило, вы используете двоичную параметричность, чтобы доказать эквивалентность программы. Это неестественно делать с унарной моделью, так как она говорит только об одной программе за раз.
Обычно вы используете унарную модель, если все, что вас интересует, это унарное свойство. Например, см. Наш недавний проект « Поверхностно-субструктурные типы» , в котором мы доказываем результат правильности типа, используя унарную модель. Поскольку разумность говорит о поведении одной программы (если то она либо расходится, либо уменьшается до значения v : A ), унарной модели достаточно. Если бы мы хотели дополнительно доказать эквивалентность программы, нам понадобилась бы бинарная модель.е : АV : A
РЕДАКТИРОВАТЬ: Я только что понял, что если вы посмотрите на нашу статью, она выглядит просто как старая модель логических отношений / реализуемости. Я должен сказать немного больше о том, что делает его (и другие модели) параметрическим. По сути, модель является параметрической, когда вы можете доказать для нее лемму расширения тождества: то есть для любого выражения типа, если все переменные свободного типа связаны с отношениями тождества, то выражение типа является отношением тождества. Мы явно не доказываем это как лемму (я не знаю почему, но вам редко нужно это делать при работе с операционными моделями), но это свойство существенно для устойчивости нашего языка.
Определение «отношения» и «отношения идентичности» в параметричности на самом деле немного подходит, и эта свобода действительно необходима, если вы хотите поддерживать причудливые типы, такие как более высокие или зависимые типы, или хотите работать с более интересными семантическими структурами. Наиболее доступное изложение, которое я знаю, находится в проекте Боба Атки « Реляционная параметричность для высших видов» .
Если у вас хороший аппетит к теории категорий, это было впервые сформулировано Розолини абстрактно в его статье « Рефлексивные графы и параметрический полиморфизм» . С тех пор он был развит Данфи и Редди в их работе « Параметрические пределы» , а также Биркедалом, Могельбергом и Петерсеном в « Теоретических моделях параметрического полиморфизма» .