![]() |
От: |
samius
|
http://sams-tricks.blogspot.com |
Дата: | 22.02.17 20:12 | ||
Оценка: |
Вот кстати, из Пирса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>Понятие параметричности было введено Рейнольдсом (Reynolds, 1974, 1983). В дальнейшем ее, наряду с родственными понятиями, исследовали ...
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>Рейнольдс расширяет реляционную семантику до полиморфных типов, восстанавливает теорему абстракции, и утверждает, что теорема фиксирует (покрывает) неофициальное понятие Стрейчи о параметричности.