Что такое язык с полным выводом типа? а ограничения такого языка?
Насколько я знаю, любой язык программирования, которому не требуется писать аннотации типов в исходном тексте при написании функции или модуля и если этот фрагмент кода является "корректным по типу", компилятор выведет типы и скомпилирует код. есть что-то еще?
Есть ли такой язык? если да, есть ли какие-либо ограничения на систему типов?
Обновление 1. Просто для ясности, я спрашиваю о статически типизированном языке программирования с полным выводом, а не о динамически типизированном языке программирования.
3 ответа
Ограничение полного вывода типа состоит в том, что он не работает со многими расширенными функциями системы типов. В качестве примера рассмотрим Haskell и OCaml. Оба этих языка почти полностью выведены из типа, но имеют некоторые особенности, которые могут мешать выводу типа.
В Haskell это классы типов в сочетании с полиморфными типами возвращаемых данных:
readAndPrint str = print (read "asd")
Вот read является функцией типа Read a => String -> a, что означает "для любого типа a который поддерживает класс типа Read функция read может взять String и вернуть a, Так что если f это метод, который принимает int, я могу написать f (read "123") и он преобразует "123" в Int 123 и вызовет f с этим. Он знает, что должен преобразовать строку в Int, потому что f занимает Int. Если бы f взял список целых, он попытался бы вместо этого преобразовать строку в список целых. Нет проблем.
Но для readAndPrint Функция выше этого подхода не работает. Проблема здесь в том, что print может принимать аргумент любого типа, который может быть напечатан (то есть любой тип, который поддерживает Show класс типов). Таким образом, у компилятора нет возможности узнать, хотите ли вы преобразовать строку в целое число, список целых чисел или что-либо еще, что может быть напечатано. Поэтому в таких случаях вам нужно добавить аннотации типов.
В OCaml проблемной особенностью являются полиморфные функции в классах: если вы определяете функцию, которая принимает объект в качестве аргумента и вызывает метод для этого объекта, компилятор выведет мономорфный тип для этого метода. Например:
let f obj = obj#meth 23 + obj#meth 42
Здесь компилятор выведет, что obj должен быть экземпляром класса, у которого есть метод с именем meth типа int -> intт.е. метод, который принимает Int и возвращает Int. Теперь вы можете определить группу классов, имеющих такой метод, и передавать экземпляры этого класса в качестве аргументов f, Нет проблем.
Проблема возникает, если вы определяете класс с методом типа 'a. 'a -> intт.е. метод, который может принимать аргумент любого типа и возвращать int. Вы не можете передать объект этого класса в качестве аргумента f потому что это не соответствует выведенному типу. Если ты хочешь f чтобы принять такой объект в качестве аргумента, единственный способ - добавить аннотацию типа f,
Таким образом, это были примеры языков, которые почти полностью выводятся из типов, и случаи, когда они не являются таковыми. Если вы удалите проблемные функции из этих языков, они будут полностью выведены из текста.
Следовательно, основные диалекты МЛ без таких продвинутых функций полностью выведены из типа Например, я предполагаю, что Caml Light полностью выведен из типа, поскольку в основном это OCaml без классов (однако я на самом деле не знаю язык, так что это всего лишь предположение).
Что такое вывод типа?
Исторически, вывод типа (или восстановление типа) означал, что все типы в программе могут быть получены без необходимости каких-либо явных аннотаций типов. Однако в последние годы в мейнстриме языка программирования стало модным обозначать даже самые тривиальные формы восходящего вывода типов как "вывод типа" (например, новый auto объявления C++11). Таким образом, люди начали добавлять "полный", чтобы ссылаться на "реальную" вещь.
Что такое полный тип вывода?
Существует широкий спектр того, в какой степени язык может выводить типы, и на практике почти ни один язык не поддерживает "полный" вывод типов в самом строгом смысле этого слова (основной пример ML - единственный пример). Но главный отличительный фактор заключается в том, могут ли типы быть получены для привязок, к которым не прикреплено "определение" - в частности, параметров функций. Если вы можете написать, скажем,
f(x) = x + 1
и система типов выясняет, что f например, имеет тип Int → Int, тогда имеет смысл вызывать этот тип вывода. Кроме того, мы говорим о выводе полиморфного типа, когда, например,
g(x) = x
присваивается общий тип ∀(t) t → t автоматически.
Вывод типа был изобретен в контексте лямбда-исчисления с простыми типами, а полиморфный вывод типа (он же вывод Хиндли / Милнера, изобретенный в 1970-х годах) является заявлением о славе языков семейства ML (Standard ML, OCaml и возможно Хаскель).
Каковы пределы полного вывода типа?
Core ML обладает роскошью "полного" вывода полиморфного типа. Но это зависит от определенных ограничений полиморфизма в его системе типов. В частности, только определения могут быть общими, а не аргументы функций. То есть,
id(x) = x;
id(5);
id(True)
работает нормально, потому что id может быть задан полиморфный тип, когда определение известно. Но
f(id) = (id(5); id(True))
не проверяет тип в ML, потому что id не может быть полиморфным в качестве аргумента функции. Другими словами, система типов допускает полиморфные типы, такие как ∀(t) t → t, но не так называемые полиморфные типы более высокого ранга, такие как (∀(t) t → t) → Bool, где полиморфные значения используются в первоклассным способом (который, чтобы быть ясным, даже очень немногие явно типизированные языки позволяют).
Полиморфное лямбда-исчисление (также называемое "Система F"), которое явно напечатано, допускает последнее. Но это стандартный результат в теории типов, что восстановление типа для полной Системы F неразрешимо. Хиндли / Милнер попадает в приятное место немного менее выразительной системы типов, для которой реконструкция типов все еще решаема.
Существуют более продвинутые функции системы типов, которые также делают неразрешимой полную реконструкцию типов. Есть и другие, которые делают его разрешимым, но все же делают его невозможным, например, наличие специальной перегрузки или подтипа, потому что это приводит к комбинаторному взрыву.
Еще одним ограничением являются типы с более высоким рейтингом. Например, следующая программа не выполняет проверку типов в языках с выводом типа стиля ML:
foo = let bar f = (f ['a', 'b', 'c'], f [1,2,3]) in bar reverse
Средство проверки типа может назначать типу [Char] -> [Char] или [Int] -> [Int], но не a.[A]->[a]. В ML, Ocaml и F# нет способа исправить это, поскольку вы даже не можете писать типы с более высоким рангом.
Но Haskell (через расширение GHC) и Frege поддерживают типы более высокого ранга. Но поскольку возможна только проверка типов с более высоким рангом (в отличие от вывода с более высоким рангом), программист должен предоставить аннотацию типа, хотя, например:
foo = let bar (f :: forall a.[a]->[a]) = (f ['a', 'b', 'c'], f [1,2,3]) in bar reverse