Вывод типа

Вывод типа , иногда называемый реконструкцией типа , относится к автоматическому определению типа выражения на формальном языке . К ним относятся языки программирования и системы математических типов , а также естественные языки в некоторых областях информатики и лингвистики .

Нетехническое объяснение

Типы в самом общем виде могут быть связаны с назначенным использованием, предполагающим и ограничивающим действия, возможные для объекта этого типа. Многие существительные в языке определяют такое использование. Например, слово « поводок» указывает на другое использование, чем слово « линия» . Назвать что-то столом означает другое обозначение, чем называть это дровами , хотя по сути это может быть одно и то же. Хотя их материальные свойства позволяют использовать вещи для определенных целей, они также подлежат особым обозначениям. Это особенно актуально в абстрактных областях, а именно в математике и информатике, где материал в конечном итоге представляет собой лишь биты или формулы.

Чтобы исключить нежелательное, но материально возможное использование, концепция типов определяется и применяется во многих вариациях. В математике парадокс Рассела положил начало появлению первых версий теории типов. В языках программирования типичными примерами являются «ошибки типа», например, команда компьютеру суммировать значения, которые не являются числами. Хотя это возможно с материальной точки зрения, результат больше не будет иметь смысла и, возможно, будет катастрофическим для всего процесса.

При типизации выражение противопоставляется типу. Например, $4$, $2+2$, и $2\cdot 2$ все это отдельные термины с типом $\mathrm {nat}$для натуральных чисел . Традиционно за выражением следует двоеточие и его тип, например: $2:\mathrm {nat}$. Это означает, что значение $2$ имеет тип $\mathrm {nat}$. Эта форма также используется для объявления новых имен, например $n:\mathrm {nat}$, очень похоже на введение в сцену нового персонажа словами «детектив Декер».

В отличие от истории, в которой обозначения разворачиваются медленно, объекты в формальных языках часто приходится с самого начала определять по их типу. Кроме того, если выражения неоднозначны, могут потребоваться типы, чтобы явно указать предполагаемое использование. Например, выражение $2$ может иметь тип $\mathrm {nat}$ но его также можно читать как рациональное или действительное число или даже как простой текст .

Как следствие, программы или доказательства могут настолько перегрузиться типами, что их желательно выводить из контекста. Это может быть возможно путем сбора данных об использовании нетипизированных выражений (включая неопределенные имена). еще неопределенное имя n Если, например, в выражении используется $n+2$, можно заключить, что n — это как минимум число. Процесс вывода типа из выражения и его контекста — это вывод типа .

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

Проверка типов против вывода типов

При типизации выражение E противопоставляется типу T, формально записываемому как E : T. Обычно типизация имеет смысл только в некотором контексте, который здесь опущен.

В этой ситуации особый интерес представляют следующие вопросы:

1. Э: Т? В этом случае заданы как выражение E, так и тип T. Итак, действительно ли E — это T? Этот сценарий известен как проверка типов .
2. Э: _? Здесь известно только выражение. Если есть способ получить тип для E, то мы выполнили вывод типа .
3. _ : Т? Наоборот. Учитывая только тип, есть ли для него какое-либо выражение или тип не имеет значений? Есть ли пример буквы Т? Это известно как тип проживания .

Для простого лямбда-исчисления все три вопроса разрешимы . Ситуация не столь комфортна, когда более выразительные допускаются типы.

Типы в языках программирования

Типы — это функция, присутствующая в некоторых строго статически типизированных языках. Это часто характерно для функциональных языков программирования в целом. Некоторые языки, которые включают вывод типа, включают C23 , С++11 , C# (начиная с версии 3.0), Chapel , Clean , Crystal , D , F# , FreeBASIC , Go , Haskell , Java (начиная с версии 10), Julia , Котлин , ML , Nim , OCaml , Opa , Q#, RPython , Rust , Скала , Быстрый , TypeScript , Налейте , Дарт , и Visual Basic (начиная с версии 9.0). Большинство из них используют простую форму вывода типа; система типов Хиндли -Милнера может обеспечить более полный вывод типов. Возможность автоматического вывода типов упрощает многие задачи программирования, позволяя программисту пропускать аннотации типов, но при этом разрешая проверку типов.

В некоторых языках программирования все значения имеют тип данных, явно объявленный во время компиляции , что ограничивает значения, которые конкретное выражение может принимать во время выполнения . Все чаще компиляция «точно в срок» стирает различие между временем выполнения и временем компиляции. Однако исторически сложилось так, что если тип значения известен только во время выполнения, эти языки являются динамически типизированными . В других языках тип выражения известен только во время компиляции ; эти языки статически типизированы . В большинстве статически типизированных языков входные и выходные типы функций и локальных переменных обычно должны быть явно указаны с помощью аннотаций типов. Например, в ANSI C :

int   add_one  (  int   x  )   { 
     int   result  ;    /* объявляем целочисленный результат */ 

     result   =   x   +   1  ; 
      вернуть   результат  ; 
  } 

Подпись , этого определения функции int add_one(int x), заявляет, что add_one — это функция, которая принимает один аргумент, целое число , и возвращает целое число. int result; объявляет, что локальная переменная resultявляется целым числом. В гипотетическом языке, поддерживающем вывод типов, код мог бы быть написан следующим образом:

add_one  (  x  )   { 
     вар   результат  ;     /* переменная выведенного типа result */ 
     var   result2  ;    /* переменная выведенного типа result #2 */ 

     result   =   x   +   1  ; 
      результат2   =   х   +   1,0  ;     /* эта строка не будет работать (на предложенном языке) */ 
     return   result  ; 
  } 

Это идентично написанию кода на языке Dart , за исключением того, что на него налагаются некоторые дополнительные ограничения, описанные ниже. Можно было бы определить типы всех переменных во время компиляции. В приведенном выше примере компилятор сделает вывод, что result и x иметь целочисленный тип, поскольку константа 1 является целочисленным типом, и, следовательно, что add_one это функция int -> int. Переменная result2 не используется юридически, поэтому у него не будет типа.

На воображаемом языке, на котором написан последний пример, компилятор предположил бы, что в отсутствие информации об обратном +принимает два целых числа и возвращает одно целое число. (Вот как это работает, например, в OCaml .) Из этого средство вывода типа может сделать вывод, что тип x + 1 является целым числом, что означает result является целым числом и, следовательно, возвращаемым значением add_oneявляется целым числом. Аналогично, поскольку + требует, чтобы оба его аргумента были одного типа, x должно быть целым числом, и, следовательно, add_one принимает одно целое число в качестве аргумента.

Однако в следующей строке result2 вычисляется путем добавления десятичной дроби. 1.0 с арифметикой с плавающей запятой , вызывая конфликт при использовании xкак для целочисленных выражений, так и для выражений с плавающей запятой. Правильный алгоритм вывода типа для такой ситуации известен с 1958 года и известен как правильный с 1982 года. Он пересматривает предыдущие выводы и с самого начала использует наиболее общий тип: в данном случае с плавающей запятой. Однако это может иметь пагубные последствия: например, использование чисел с плавающей запятой с самого начала может привести к проблемам с точностью, которых не было бы при использовании целочисленного типа.

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

Алгоритм промежуточной общности неявно объявляет result2 как переменную с плавающей запятой, а сложение неявно преобразует xдо плавающей точки. Это может быть правильно, если контексты вызова никогда не предоставляют аргумент с плавающей запятой. Такая ситуация показывает разницу между выводом типа , который не предполагает преобразование типа , и неявным преобразованием типа , которое принудительно приводит данные к другому типу данных, часто без ограничений.

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

Недавнее появление JIT-компиляции позволяет использовать гибридные подходы, при которых тип аргументов, предоставляемых различным контекстом вызова, известен во время компиляции и может генерировать большое количество скомпилированных версий одной и той же функции. Каждую скомпилированную версию затем можно оптимизировать для другого набора типов. Например, JIT-компиляция позволяет иметь как минимум две скомпилированные версии add_one :

Версия, которая принимает целочисленные входные данные и использует неявное преобразование типов.

Версия, которая принимает в качестве входных данных число с плавающей запятой и повсюду использует инструкции с плавающей запятой.

Техническое описание

Вывод типа — это возможность автоматически определять, частично или полностью, тип выражения во время компиляции. Компилятор часто может определить тип переменной или сигнатуру типа функции без явных аннотаций типа. Во многих случаях можно полностью исключить аннотации типов из программы, если система вывода типов достаточно надежна или программа или язык достаточно просты.

Чтобы получить информацию, необходимую для вывода типа выражения, компилятор либо собирает эту информацию в виде совокупности и последующего сокращения аннотаций типов, заданных для его подвыражений, либо посредством неявного понимания типа различных атомарных значений (например, true: Логическое значение; 42: Целое число; 3,14159: Действительное и т. д.). Именно благодаря распознаванию возможного сведения выражений к неявно типизированным атомарным значениям компилятор языка вывода типов может скомпилировать программу полностью без аннотаций типов.

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

Некоторые методы вывода типа основаны на удовлетворении ограничений. или теории выполнимости по модулю .

Пример

Например, Haskell функция map применяет функцию к каждому элементу списка и может быть определена как:

карта   f   []   =   [] 
 карта   f   (  первый  :  отдых  )   =   f   первый   :   карта   f   отдых 

Введите вывод на map функция происходит следующим образом. map является функцией двух аргументов, поэтому ее тип ограничен формой a → b → c. В Haskell шаблоны [] и (first:rest) всегда соответствуют спискам, поэтому второй аргумент должен быть типом списка: b = [d] для какого-то типа d. Его первый аргумент f применяется к аргументу first, который должен иметь тип d, что соответствует типу в аргументе списка, поэтому f :: d → e ( :: означает «имеет тип») для некоторого типа e. Возвращаемое значение map f, наконец, список чего угодно f производит, поэтому [e].

Соединение частей вместе приводит к map :: (d → e) → [d] → [e]. В переменных типа нет ничего особенного, поэтому их можно переименовать как

карта   ::   (  а   →   б  )   →   [  а  ]   →   [  б  ] 

Оказывается, это также самый общий тип, поскольку никаких дополнительных ограничений не применяется. В качестве предполагаемого типа map , параметрически полиморфен тип аргументов и результатов f не выводятся, а оставляются как переменные типа, и поэтому map может применяться к функциям и спискам различных типов, при условии, что фактические типы совпадают при каждом вызове.

Хиндли-

Основная статья: система типов Хиндли – Милнера

Алгоритм, впервые использованный для вывода типа, теперь неофициально называется алгоритмом Хиндли-Милнера, хотя по праву этот алгоритм следует приписать Дамасу и Милнеру. Ее также традиционно называют реконструкцией типа . Если термин правильно типизирован в соответствии с правилами типизации Хиндли-Милнера, то эти правила генерируют основную типизацию для этого термина. Процесс обнаружения этой основной типизации — это процесс «реконструкции».

Происхождением этого алгоритма является алгоритм вывода типа для просто типизированного лямбда-исчисления , который был разработан Хаскеллом Карри и Робертом Фейсом в 1958 году. В 1969 году Дж. Роджер Хиндли расширил эту работу и доказал, что их алгоритм всегда выводит наиболее общий тип. В 1978 году Робин Милнер независимо от работы Хиндли предоставил эквивалентный алгоритм, алгоритм W. В 1982 году Луис Дамас наконец доказал, что алгоритм Милнера является полным, и расширил его для поддержки систем с полиморфными ссылками.

Побочные эффекты использования самого общего типа

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

• плавающая запятая рассматривается как общий тип целого числа, тогда как плавающая запятая создаст проблемы с точностью
• вариантные/динамические типы рассматриваются как общий тип других типов, что вводит правила приведения и сравнения, которые могут быть разными, например, такие типы используют оператор «+» как для числового сложения, так и для конкатенации строк, но какая операция выполняется: определяется динамически, а не статически

Вывод типов для естественных языков

Алгоритмы вывода типов использовались для анализа естественных языков , а также языков программирования. Алгоритмы вывода типа также используются в некоторых грамматических индукциях. и грамматические системы на основе ограничений для естественных языков.

Внешние ссылки

• Архивное электронное письмо Роджера Хиндли, объясняющее историю вывода типов.
• Вывод полиморфного типа Майкла Шварцбаха дает обзор вывода полиморфного типа.
• Базовая статья Луки Карделли по проверке типов, описывает алгоритм и включает реализацию в Modula-2.
• Реализация вывода типа Хиндли-Милнера в Scala , Эндрю Форрест (получено 30 июля 2009 г.)
• Реализация Хиндли-Милнера в Perl 5, Никита Борисов из Wayback Machine (архивировано 18 февраля 2007 г.)
• Что такое Хиндли-Милнер? (и почему это круто?) Объясняет Хиндли-Милнер, примеры на Scala