Зачем нам нужны отдельные обозначения для П-типов?

Question

Главная

Меня смущает мотивация, стоящая за необходимостью отдельного обозначения для П-типов, которые вы можете найти в системах типов начиная с λ2.Ответ обычно звучит примерно так - подумайте о том, как можно представить сигнатуру функции идентификации - это может быть λa:type.λx:a.x или λb:type.λx:b.x.Тонкость, по их словам, заключается в том, что эти две подписи не только not equal, они не являются альфа-эквивалентами в качестве переменных типа a и b являются свободными переменными внутри соответствующих им абстракций.Итак, чтобы преодолеть эту досадную синтаксическую проблему, мы представляем П binder, который прекрасно сочетается с альфа-преобразованием.

Итак, вопрос:почему это так?Почему бы просто не зафиксировать понятие альфа-эквивалентности?

ОБНОВЛЕНИЕ z:

О, глупо с моей стороны, λa:type.λx:a.x и λb:type.λx:b.x являются альфа-эквивалентом.Но почему a:type -> a -> a и b:type -> b -> b не тогда.

ОБНОВЛЕНИЕ suck z:

Ага, интересно, я думаю, это идеальный пример избирательной слепоты =D

Я читаю эту книгу Теория типов и формальное доказательство, а в главе о lambda2 автор мотивирует существование П используя именно такую аргументацию, нельзя сказать, что \t:*.\v:t.v : * -> t -> t потому что это создает два альфа-эквивалентных термина\t:*.\v:t.v и \g:*.\v:g.v имеют разные типы, так как соответствующие типы не являются альфа-эквивалентными, где типы типа t:* -> t -> t на самом деле они альфа-инвариантны. Обратите внимание на разницу между t:* -> t -> t и * -> t -> t.Но не делает ли это этот аргумент немного тривиальным, и имеет ли вообще смысл говорить о типе a -> b где a и b не связаны никакими переменными-квантификаторами.Andrej Bauer указал в комментариях , что П это действительно напоминает лямбда-абстракцию с несколькими дополнительными прибамбасами.

В общем, с этим я покончил, спасибо вам, ребята.

Answer 1

Я думаю, нам просто нужно кое-что прояснить здесь:

1. В выражении $\лямбда a :\mathsf{тип} .\лямбда x :a.x$ переменная $a$ связан (по внешнему $\лямбда$).Выражения $\лямбда a :\mathsf{тип} .\лямбда x :a.x$ и $\ лямбда b :\mathsf{тип} .\лямбда x :b.x$ являются $\альфа$-равный.
2. Выражение $\лямбда a :\mathsf{тип} .\лямбда x :a.x$ является функция идентификации, это нет "сигнатура функции идентификации".
3. Если под "сигнатурой идентификационной функции" вы имеете в виду "тип идентификационной функции", то это было бы что-то вроде $\Pi_{a :\mathsf{тип}} .(a \к a)$, или если вам нужны только типы продуктов, то это $\Pi_{a :\mathsf{тип}} \Pi_{x :a} a$.

Есть ли еще вопросы?

Может быть, это поможет:

• тип идентификационной функции $\лямбда x :a.x$ является $a \к a$
• тип идентификационной функции $\лямбда y :b.y$ является $b \к b$
• функции $\лямбда x :a.x$ и $\лямбда y :b.y$ они разные
• типы $a \к a$ и $b \к b$ они разные
• тип самого полиморфный функция идентификации $\лямбда-c :\mathsf{тип} .\лямбда z :c.z$ является $\Pi_{c :\mathsf{тип}} .c \к c$.
• функции $\лямбда a :\mathsf{тип} .\лямбда x :a.x$ и $\лямбда-c :\mathsf{тип} .\лямбда z :c.z$ являются $\альфа$-равный
• типы $\Pi_{a :\mathsf{тип}} .a \к a$ и $\Pi_{c :\mathsf{тип}} .c \к c$ являются $\альфа$-равный.

Дополнительный: После разговора с Алексом Симпсоном за чашкой чая я могу сказать еще кое-что.Мы этого не делаем потребность отдельный $\лямбда$ и $\Пи$ конструкторы, поскольку они оба имеют точно такую же синтаксическую форму (принимают два аргумента, привязывают одну переменную).На самом деле, если мне не изменяет память, Автомат использовал те же обозначения для $\лямбда$-абстракции и $\Пи$-типы.Но дело в том, что мы хотеть использовать два разных конструктора, потому что они обозначают разные концепции.