Вывод типов


Вывод типов
Типизация данных

Типобезопасность
Вывод типов
Динамическая типизация
Статическая типизация
Строгая типизация
Мягкая типизация
Зависимые типы
Утиная типизация

Вывод типа (англ. Type inference) — в программировании возможность компилятора самому логически вывести тип значения из выражения. Первоначально было распространено в функциональных языках, но в последнее время эта возможность появляется и в объектно-ориентированных ЯП (C#, D, Visual Basic .NET, C++11, Vala). Например:

var s = "Hello, world!";  // Тип переменной s (string) выведен из инициализатора

Содержание

Алгоритмы

Модель типизации Хиндли — Милнера

Модель типизации Хи́ндли — Ми́лнера — механизм вывода типов выражений, который реализован в некоторых строго типизированных языках программирования. Обычно этот механизм реализуется в рамках функциональной парадигмы программирования, хотя и не ограничен только ей. Примеры языков, которые используют модель типизации Хиндли — Милнера: Haskell, ML, OCaml, Scala, Nemerle, Fortress и Boo.

Механизм вывода типов основан на возможности автоматически полностью или частично выводить тип выражения, полученного при помощи вычисления некоторого выражения. Так как этот процесс систематически производится во время трансляции программы, транслятор часто может вывести тип переменной или функции без явного указания типов этих объектов. Во многих случаях можно опускать явные декларации типов — это можно делать для достаточно простых объектов, либо для языков с простым синтаксисом. Например, в языке Haskell реализован достаточно мощный механизм вывода типов, поэтому указание типов функций в этом языке программирования не требуется. Программист может указать тип функции явно для того, чтобы ограничить её использование только для конкретных типов данных, либо для более структурированного оформления исходного кода.

Для того, чтобы получить информацию для корректного вывода типа выражения в условиях отсутствия явной декларации типа этого выражения, транслятор либо собирает такую информацию из явных деклараций типов подвыражений (переменных, функций), входящих в изучаемое выражение, либо использует неявную информацию о типах атомарных значений. Такой алгоритм не всегда помогает определить тип выражения, особенно в случаях использования функций высших порядков и параметрического полиморфизма достаточно сложной природы. Поэтому в сложных случаях, когда есть необходимость избежать неоднозначностей, рекомендуется явно указывать тип выражений.

Сама модель типизации основана на алгоритме вывода типов выражений, который имеет своим источником механизм получения типов выражений, используемый в типизированном λ-исчислении, который был предложен в 1958 г. Х. Карри и Р. Фейсом. Далее уже́ Роджер Хиндли в 1969 г. расширил сам алгоритм и доказал, что он выводит наиболее общий тип выражения. В 1978 г. Робин Милнер независимо от Р. Хиндли доказал свойства эквивалентного алгоритма. И, наконец, в 1985 г. Луис Дамас окончательно показал, что алгоритм Милнера является законченным и может использоваться для полиморфных типов. В связи с этим алгоритм Хиндли — Милнера иногда называют также и алгоритмом Дамаса — Милнера.

Система типов определяется в модели Хиндли — Милнера следующим образом:

  1. Примитивные типы v являются типами выражений.
  2. Параметрические переменные типов α являются типами выражений.
  3. Если \sigma_{1} и \sigma_{2} — типы выражений, то тип \sigma_{1} \rightarrow \sigma_{2} является типом выражений.
  4. Символ \bot является типом выражений.

Выражения, типы которых вычисляются, определяются довольно стандартным образом:

  1. Константы являются выражениями.
  2. Переменные являются выражениями.
  3. Если e_{1} и e_{2} — выражения, то (e_{1} e_{2}) — выражение.
  4. Если v — переменная, а e — выражение, то \lambda v.e — выражение.

Говорят, что тип \sigma_{1} является экземпляром типа \sigma_{2}, когда имеется некое преобразование \rho такое, что:

\sigma_{1} = \rho(\sigma_{2})

При этом обычно полагается, что на преобразования типов \rho накладываются ограничения, заключающиеся в том, что:

  1. \rho(\sigma_{1} \rightarrow \sigma_{2}) = \rho(\sigma_{1}) \rightarrow \rho(\sigma_{2})
  2. \rho(v) = v

Сам алгоритм вывода типов состоит из двух шагов — генерация системы уравнений и последующее решение этих уравнений.

Построение системы уравнений

Построение системы уравнений основано на следующих правилах:

  1. f \Gamma v = \tau — в том случае, если связывание v : \tau находится в \Gamma.
  2. f \Gamma (e f) = \tau — в том случае, если \tau_{1} = \tau_{2} \rightarrow \tau, где \tau_{1} = f \Gamma e и \tau_{2} = f \Gamma f.
  3. f \Gamma (\lambda v.e) = \tau \rightarrow \tau_{e} — в том случае, если \tau_{e} = f \Gamma' e и \Gamma' является расширением \Gamma связыванием v : \tau.

В этих правилах под символом \Gamma понимается набор связываний переменных с их типами:

\Gamma = v_{1} : A_{1}, v_{2} : A_{2}, \ldots, v_{n} : A_{n}

Решение системы уравнений

Решение построенной системы уравнений основано на алгоритме унификации. Это достаточно простой алгоритм. Имеется некоторая функция u, которая принимает на вход уравнение типов и возвращает некоторую подстановку. Подстановка — это просто проекция переменных типов на сами типы. Такие подстановки могут вычисляться различными способами, которые зависят от конкретной реализации алгоритма Хиндли — Милнера.

См. также

Ссылки


Wikimedia Foundation. 2010.

Смотреть что такое "Вывод типов" в других словарях:

  • ВЫВОД ЛОГИЧЕСКИЙ —     ВЫВОД ЛОГИЧЕСКИЙ рассуждение, в котором     осуществляется переход по правилам от высказывания или системы высказываний к высказыванию или системе высказываний. К логическому выводу обычно предъявляются (совместно или по отдельности)… …   Философская энциклопедия

  • вывод логический —         ВЫВОД ЛОГИЧЕСКИЙ рассуждение, в котором по определенным правилам осуществляется переход от высказываний или системы высказываний к высказыванию или системе высказываний. К В. л. обычно предъявляются (разом или по отдельности) следующие… …   Энциклопедия эпистемологии и философии науки

  • Ввод/вывод — С информатике, ввод/вывод (в англ. языке часто используется сокращение I/O  input/output) означает взаимодействие между обработчиком информации (например, компьютер) и внешним миром, который может представлять как человек, так и любая другая …   Википедия

  • Ввод-вывод — В информатике, ввод/вывод (в англ. языке часто используется сокращение I/O) означает взаимодействие между обработчиком информации (например, компьютер) и внешним миром, который может представлять как человек, так и любая другая система обработки… …   Википедия

  • Сравнение языков программирования — Эту статью следует викифицировать. Пожалуйста, оформите её согласно правилам оформления статей.  Условные обозначения  …   Википедия

  • C++ — У этого термина существуют и другие значения, см. C. См. также: Си (язык программирования) C++ Семантика: мультипарадигмальный: объектно ориентированное, обобщённое, процедурное, метапрограммирование Тип исполнения: компилируемый Появился в …   Википедия

  • Coq — (фр. coq  петух)  интерактивное программное средство доказательства теорем, использующее собственный язык функционального программирования (Gallina) с зависимыми типами. Позволяет записывать математические теоремы и их… …   Википедия

  • C++11 — C++11[1][2] или ISO/IEC 14882:2011[3] (в процессе работы над стандартом носил условное наименование C++0x[4][5])  новая версия стандарта языка C++, вместо ранее действовавшего ISO/IEC 14882:2003. Новый стандарт включает дополнения в ядре… …   Википедия

  • C++0x — C++0x  будущая версия стандарта языка C++, вместо ныне существующего ISO/IEC 14882:2003. Новый стандарт будет включать дополнения в ядре языка и расширение STL, включая большую часть TR1  кроме, вероятно, библиотеки специальных… …   Википедия

  • Nemerle — Семантика: мультипарадигменный, объектно ориентированный, функциональный, императивный Тип исполнения: компилируемый Появился в: 0.9.3 16 мая …   Википедия

Книги

Другие книги по запросу «Вывод типов» >>


Поделиться ссылкой на выделенное

Прямая ссылка:
Нажмите правой клавишей мыши и выберите «Копировать ссылку»

We are using cookies for the best presentation of our site. Continuing to use this site, you agree with this.