Здравствуйте, vdimas, Вы писали:
V>Здравствуйте, samius, Вы писали:
V>>>Не останавливайся на достигнутом. Откажись считать себя программистом. 
S>>На том основании, что ты не распарсил слово "function" в определении, которое пытался выдать за определение полиморфизма? Это несерьезное основание.
V>Я давал тебе самое серьезное из всех современных обоснований — это HoTT.
V>В нем полиморфизмом называются "зависимые функции".
В нем нет упоминания слова polymorphism. Но куча упоминания polymorphic function. Т.е. даже не читая, можно предположить что ты читал невнимательно.
V>Иерархию я приводил:
V>http://www.rsdn.org/forum/flame.comp/6700097.1
видел, комментировал.
V>Аналогично по чуть менее серьезному, что всё еще самому серьезному среди оставшихся — это книга Пирса "Типы в ЯП".
V>Там он посвящает понятию "полиморфизма" целую главу V.
V>В этой главе о полиморфизме рассматриваются:
V>* Типизация на основе ограничений
V>* Унификация (принцип Хиндли-Милнера, когда компилятором выбирается более специализированная перегрузка в текущем контексте, т.е. более специализированное имеет преимущество над менее специализированным; в С++ похожие правила вывода с некоторыми ограничениями на сценариях автоприведения типов + конструкторов).
V>* определение полиморфизма (Система F) —
V>V>Система F является расширением типизированного лямбда-исчисления.
Вот кстати, из Пирса
The term polymorphism refers to a range of language mechanisms that allow a single part of a program to be used with different types in different contexts (§23.2 discusses several varieties of polymorphism in more detail).
Если Пирсу не доверяешь, так и скажи. А то "тут не гляди, тут гляди"!
V>* параметричность
V>Тут Пирс ничего не говорит сам, а отсылает к целому списку авторов:
Как не говорит сам? Я устал цитировать то что он "не говорит сам". И на этой неделе уже тоже цитировал.
V>V>Понятие параметричности было введено Рейнольдсом (Reynolds, 1974, 1983). В дальнейшем ее, наряду с родственными понятиями, исследовали ...
V>Что пишут о работах Рейнольдса (сами работы доступны как картинк-сканы, приводить их неудобно, поэтому рецензия):
V>http://www.ccs.neu.edu/home/matthias/369-s10/Transcript/parametricity.pdf
V>V>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.
V>...
V>The main generalization introduces the polymorphic λ-calculus for defining functions that are parametrically plymorphic in the sense of Strachey.
V>Reynolds extends the relational semantics to polymorphic types, reestablishes the abstraction theorem, and argues that the theorem captures Strachey’s informal notion of parametricity.
V>Переведу на русский, чтобы опять кто-то не запутался:
V>V>Основным обобщением вводится полиморфное лямбда-исчисление для определения функций, которые являются параметрически полиморфными в смысле Стрейчи.
V>Рейнольдс расширяет реляционную семантику до полиморфных типов, восстанавливает теорему абстракции, и утверждает, что теорема фиксирует (покрывает) неофициальное понятие Стрейчи о параметричности.
О, видишь, "полиморфные типы". А ты говорил, что нет таких.
V>Так вот. Полиморфное лямбда-исчисление — это Система F, которая, в свою очередь, является расширением типизированного лямбда-исчисления.
V>Круг замкнулся. 
V>Т.е., PP по Пирсу — это развитие типизированного лямбда исчисления (типизация на основе ограничений). ТЧК.
Это демагогия чистой воды. Пирс дал определение ПП и я его приводил. ПП по Пирсу — это именно оно. А вот то что ты написал — это "ПП по Пирсу с колокольни vdimas-а". Буду уверен в этом до тех пор, пока не приведешь цитату Пирса с тем, что ты ему приписываешь.
