Переменная типа: различия между версиями
| [отпатрулированная версия] | [отпатрулированная версия] |
Содержимое удалено Содержимое добавлено
маааленькое дополнение |
|||
Строка 41:
Простейшее связывание ти́повых переменных называется их [[квантификация|квантификацией]]. Выделяются два случая:
* Действие переменной типа распространяется на '''''всё''''' определение типа:<br /><code>['a, 'b] 'a -> 'b -> 'a</code><br /><!-- стилистическое решение, которое в данном случае лучше - <source> ломает табуляцию, что для перечисления нежелательно; с другой - необходимо наглядное сопоставление сигнатур типов -->Математически такой тип записывается через [[Квантор всеобщности|универсальный квантор]] — «<math>\forall a. ~\forall b. ~a \rightarrow
▲Математически такой тип записывается через [[Квантор всеобщности|универсальный квантор]] — «<math>\forall a. a \rightarrow a~list </math>» — поэтому такая переменная типа называется «[[Квантор всеобщности|универсально квантифицированной]]», а весь тип — «универсально полиморфным».
{{викиучебник|:en:Haskell/Existentially_quantified_types|Экзистенциально квантифицированные типы в Хаскеле {{ref-en}}}}
* Действие переменной типа распространяется только на '''''часть''''' определения типа:<br /><code>['a] 'a -> (['b] b -> a)</code><br />Математически такой тип записывается через [[Квантор существования|экзистенциальный квантор]] — «<math>\
▲Математически такой тип записывается через [[Квантор существования|экзистенциальный квантор]] — «<math>\exists a. a \rightarrow a~list </math>» — поэтому такая переменная называется «[[Квантор существования|экзистенциально квантифицированной]]», а весь тип — «экзистенциальным». Далеко не во всех случаях «превращение» универсально полиморфного типа в экзистенциальный даёт применимый на практике тип или заметные отличия от универсального полиморфизма, но в определённых случаях использование [[экзистенциальный тип|экзистенциальных типов]] поднимает [[параметрический полиморфизм]] на [[объект первого класса|первоклассный]] уровень, т.е. позволяет передавать полиморфные функции без связывания в качестве параметров другим функциям (см. [[полиморфизм первого класса]]). Классическим примером является реализация гетерогенного списка (см. викиучебник). {{iw|Явная типизация|Явное аннотирование типов|en|Manifest typing}} в этом случае становится обязательным, т.к. [[выведение типов]] для полиморфизма выше ранга 2 [[алгоритмическая разрешимость|алгоритмически неразрешимо]].{{sfn|haskell_existentials}}
На практике, универсально полиморфные типы дают [[полиморфизм типов|обобщённость типа данных]], а экзистенциальные — [[абстрактный тип данных|абстрактность типа данных]]{{sfn|Cardelli, Wegner - On Understanding Types}}.
| |||