Теория типов: возможные экземпляры в системе с полиморфизмом

[Mysterious Light]

Добрый день

Рассматривается $\lambda$-исчисление с явным полиморфизмом (Рейнольдс).

Есть известное утверждение о том, что только $\mathrm{id} : \forall \alpha.\alpha\to\alpha$ обладает указанным типом, а для типа $\forall \alpha.\alpha\to(\alpha\to\alpha)$ существуют только $\mathrm{fst}=\Lambda\alpha\lambda x:\alpha.\lambda y:\alpha.x$ и \mathrm{snd}=$\Lambda\alpha\lambda x:\alpha.\lambda y:\alpha.y$.

Первое утверждение можно доказать неким косвенным образом, сославшись на теорему

$$(\forall f:\forall \alpha.\alpha\to\alpha) (\forall \alpha)(\forall \beta) (\forall g:\alpha\to\beta) (f_\beta\circ g = g \circ f_\alpha),$$

положив $g=\lambda xy.x$ и применив принцип экстенсиональности.

Каким образом можно доказать второе утверждение?

Кроме этого, пусть система типов содержит в себе тип списка и соответствующие иму операции композиции/декомпозиции и свёртки. Можно ли как-то доказать, что любая функция с типом $\forall \alpha.[\alpha]\to\alpha$ представима в виде $\lambda l.El(n(\mathrm{length}\, l))$, где $Elm$ возвращает $m$-й элемент списка $l$, для некоторой функции $n:\mathbb{N}\to\mathbb{N}$?

Кто подобные вопросы рассматривал?

[Xaositect]

Это называется параметричность (parametricity). Ссылки: J. C. Reynolds "Types, Abstractions and Parametric Polymorphism", P. Wadler "Theorems for free!".

Mysterious Light в сообщении #1098138 писал(а):

Первое утверждение можно доказать неким косвенным образом, сославшись на теорему

$$(\forall f:\forall \alpha.\alpha\to\alpha) (\forall \alpha)(\forall \beta) (\forall g:\alpha\to\beta) (f_\beta\circ g = g \circ f_\alpha),$$

Аналогично этой теореме, есть свободная теорема для $\forall \alpha. \alpha \to \alpha \to \alpha$:

$$(\forall f:\forall \alpha.\alpha\to\alpha\to\alpha) (\forall \alpha) (\forall \beta) (\forall g\colon\alpha\to\beta) (\forall x, y \colon\alpha) (f_{\beta} (g x) (g y) = g (f_{\alpha} x y)).$$

Для того, чтобы вывести отсюда существование ровно двух функций, возьмем сначала $g = \operatorname{const} u$, получим $f u u = u$, а потом $\alpha = \mathbf{2}$. Есть два варианта функции $f_{\mathbf{2}}$ и с помощью произвольной $g$ они распространяются на два варианта полиморфной функции $f$.

Mysterious Light в сообщении #1098138 писал(а):

Кроме этого, пусть система типов содержит в себе тип списка и соответствующие иму операции композиции/декомпозиции и свёртки. Можно ли как-то доказать, что любая функция с типом $\forall \alpha.[\alpha]\to\alpha$ представима в виде $\lambda l.El(n(\mathrm{length}\, l))$, где $Elm$ возвращает $m$-й элемент списка $l$, для некоторой функции $n:\mathbb{N}\to\mathbb{N}$?

Тут нужен тип непустого списка, иначе неоткуда брать значение на пустом аргументе (обратите внимание на $[\mathbf{0}] \to \mathbf{0}$). Если рассматривать непустые списки, то можно свести случай к предыдущему: по функции $f \colon \forall \alpha. \alpha^{+} \to \alpha$ можно определить функции $f_{n, i} x y = f [x, \dots, x, y, x, \dots, x]$ (всего $n$ элементов в списке, на $i$-м месте $y$). Рассматривая их на типе $\mathbf{2}$, можно доказать, что ровно для одного $i$ это будет $\operatorname{snd}$.