Здравствуйте, samius, Вы писали:

S>>>Я неоднократно ответил. Отказываюсь считать определением полиморфизма определение полиморфной функции.
V>>Не останавливайся на достигнутом. Откажись считать себя программистом.
S>На том основании, что ты не распарсил слово "function" в определении, которое пытался выдать за определение полиморфизма? Это несерьезное основание.

Я давал тебе самое серьезное из всех современных обоснований — это HoTT.
В нем полиморфизмом называются "зависимые функции".
Иерархию я приводил:
http://www.rsdn.org/forum/flame.comp/6700097.1

Аналогично по чуть менее серьезному, что всё еще самому серьезному среди оставшихся — это книга Пирса "Типы в ЯП".
Там он посвящает понятию "полиморфизма" целую главу V.
В этой главе о полиморфизме рассматриваются:
* Типизация на основе ограничений
* Унификация (принцип Хиндли-Милнера, когда компилятором выбирается более специализированная перегрузка в текущем контексте, т.е. более специализированное имеет преимущество над менее специализированным; в С++ похожие правила вывода с некоторыми ограничениями на сценариях автоприведения типов + конструкторов).
* определение полиморфизма (Система F) —

Система F является расширением типизированного лямбда-исчисления.

* параметричность
Тут Пирс ничего не говорит сам, а отсылает к целому списку авторов:

Понятие параметричности было введено Рейнольдсом (Reynolds, 1974, 1983). В дальнейшем ее, наряду с родственными понятиями, исследовали ...

Что пишут о работах Рейнольдса (сами работы доступны как картинк-сканы, приводить их неудобно, поэтому рецензия):
http://www.ccs.neu.edu/home/matthias/369-s10/Transcript/parametricity.pdf

In this paper Reynolds formalizes the idea of data abstraction: what does it mean for a client of a data type to be insensitive to the type’s choice of internal representation? An abstract data type exposes a type name and a set of operations on the type, and a client program respects the abstraction if it cannot make a concrete observation to distinguish different choices of representation for the abstract type.
...
The main generalization introduces the polymorphic λ-calculus for defining functions that are parametrically plymorphic in the sense of Strachey.

Reynolds extends the relational semantics to polymorphic types, reestablishes the abstraction theorem, and argues that the theorem captures Strachey’s informal notion of parametricity.

Переведу на русский, чтобы опять кто-то не запутался:

Основным обобщением вводится полиморфное лямбда-исчисление для определения функций, которые являются параметрически полиморфными в смысле Стрейчи.

Рейнольдс расширяет реляционные семантику до полиморфных типов, восстанавливает теорему абстракции, и утверждает, что теорема фиксирует (покрывает) неофициальное понятие Стрейчи о параметричности.

Так вот. Полиморфное лямбда-исчисление — это Система F, которая, в свою очередь, является расширением типизированного лямбда-исчисления.

Круг замкнулся.
Т.е., PP по Пирсу — это развитие типизированного лямбда исчисления (типизация на основе ограничений). ТЧК.

Здравствуйте, samius, Вы писали:

S>>>Я неоднократно ответил. Отказываюсь считать определением полиморфизма определение полиморфной функции.
V>>Не останавливайся на достигнутом. Откажись считать себя программистом.
S>На том основании, что ты не распарсил слово "function" в определении, которое пытался выдать за определение полиморфизма? Это несерьезное основание.

Я давал тебе самое серьезное из всех современных обоснований — это HoTT.
В нем полиморфизмом называются "зависимые функции".
Иерархию я приводил:
http://www.rsdn.org/forum/flame.comp/6700097.1

Аналогично по чуть менее серьезному, что всё еще самому серьезному среди оставшихся — это книга Пирса "Типы в ЯП".
Там он посвящает понятию "полиморфизма" целую главу V.
В этой главе о полиморфизме рассматриваются:
* Типизация на основе ограничений
* Унификация (принцип Хиндли-Милнера, когда компилятором выбирается более специализированная перегрузка в текущем контексте, т.е. более специализированное имеет преимущество над менее специализированным; в С++ похожие правила вывода с некоторыми ограничениями на сценариях автоприведения типов + конструкторов).
* определение полиморфизма (Система F) —

Система F является расширением типизированного лямбда-исчисления.

* параметричность
Тут Пирс ничего не говорит сам, а отсылает к целому списку авторов:

Понятие параметричности было введено Рейнольдсом (Reynolds, 1974, 1983). В дальнейшем ее, наряду с родственными понятиями, исследовали ...

Что пишут о работах Рейнольдса (сами работы доступны как картинк-сканы, приводить их неудобно, поэтому рецензия):
http://www.ccs.neu.edu/home/matthias/369-s10/Transcript/parametricity.pdf

In this paper Reynolds formalizes the idea of data abstraction: what does it mean for a client of a data type to be insensitive to the type’s choice of internal representation? An abstract data type exposes a type name and a set of operations on the type, and a client program respects the abstraction if it cannot make a concrete observation to distinguish different choices of representation for the abstract type.
...
The main generalization introduces the polymorphic λ-calculus for defining functions that are parametrically plymorphic in the sense of Strachey.

Reynolds extends the relational semantics to polymorphic types, reestablishes the abstraction theorem, and argues that the theorem captures Strachey’s informal notion of parametricity.

Переведу на русский, чтобы опять кто-то не запутался:

Основным обобщением вводится полиморфное лямбда-исчисление для определения функций, которые являются параметрически полиморфными в смысле Стрейчи.

Рейнольдс расширяет реляционную семантику до полиморфных типов, восстанавливает теорему абстракции, и утверждает, что теорема фиксирует (покрывает) неофициальное понятие Стрейчи о параметричности.

Так вот. Полиморфное лямбда-исчисление — это Система F, которая, в свою очередь, является расширением типизированного лямбда-исчисления.

Круг замкнулся.
Т.е., PP по Пирсу — это развитие типизированного лямбда исчисления (типизация на основе ограничений). ТЧК.