Каковы пределы проверки типов и систем типов?

Question

Системы типов часто подвергаются критике за ограниченность, то есть ограничение языков программирования и запрещение программистам писать интересные программы.

Крис Смит утверждает :

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

и

Кроме того, существует железное математическое доказательство того, что средство проверки типов любого интереса всегда консервативно. Создание средства проверки типов, которое не отклоняет правильные программы, не просто сложно; это невозможно.

Не могли бы вы рассказать, какие это интересные программы? Где доказано, что шашки типа должны быть консервативными?

И более общий: каковы ограничения проверки типов и систем типов?

Answer 1

Я думаю, что первое утверждение технически неверно, хотя на практике верно.

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

Проблема в том, что для мощной логики вывод типа больше не работает, и вы должны предоставить доказательства как часть программы, чтобы средство проверки типов могло выполнять свою работу. Конкретным примером являются пруверы более высокого порядка, такие как Coq. Coq использует чрезвычайно мощную логику, но также очень утомительно делать что-либо в Coq, потому что вы должны предоставить доказательства в мельчайших деталях.

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

Что касается второго утверждения, он может ссылаться на теорему Гёделса о неполноте. В нем говорится, что для любой данной системы доказательств существуют истинные утверждения арифметики (логика сложения и умножения натуральных чисел), которые не могут быть доказаны в системе доказательств. В переводе на статические системы типов у вас будет программа, которая не делает ничего плохого, но статическая система типов не может этого доказать.

Эти контрпримеры строятся путем обращения к определению системы доказательств, говоря, по сути, «я не могу быть доказан» в переводе на арифметику, что не очень интересно. ИМХО программа, построенная аналогично, тоже не будет интересна.

Answer 2

Интересным примером является Эта статья , которая, вероятно, является единственным сравнением яблок с яблоками, когда-либо проводимым при статической и динамической типизации. Они реализовали self (язык, подобный smalltalk, но с прототипами вместо классов) как с выводом типа (статический), так и с обратной связью типа (динамический).

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

Они столкнулись с пределом их системы типов: он не мог проверить действительное значение целых чисел.

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

Answer 3

Вы можете выразить все как на статическом, так и на динамическом языке.Доказательство == вы можете написать любой языковой компилятор на любом тьюринговом языке.Итак, каким бы ни был язык, вы можете создать статический язык, который выполняет X.

Что может быть интересным в динамической типизации? ... При достаточно хорошей типизации утки вы можете взаимодействовать с объектами по сети, даже не зная ихвведите и передайте их результаты (неизвестного вам типа) в качестве параметров локальным функциям, которые на самом деле могут сделать что-то полезное.

Статический ответ на эту проблему будет заключаться в переносе всего в «экспортируемый интерфейс» с предоставлением .call () и .provides? () работает над текстовым именем, но это будет определенно сложнее.

Это самый «ограничивающий» случай, который я знаю, и он действительно немного растягивает (только действительно полезен для ложных объектов?),Что касается теоретических ограничений, то их нет - вам просто нужен дополнительный код для преодоления практических проблем.

Answer 4

Я думаю, что есть недоразумение. Это правда, что любая система типов отклонит правильную программу (я не помню точное имя результата, поэтому я не могу найти его прямо сейчас, извините). В то же время верно, что любой полный язык Тьюринга может делать то же самое, что и любой другой, поэтому неверно, что есть некоторые программы на динамически типизированных языках, которые вы не можете воспроизвести, скажем, на Haskell.

Загвоздка в том, что тот факт, что система типов отклонит программу, не означает, что она отклонит все эквивалентные ей программы. Поэтому некоторые программы будут отклонены, но вы можете заменить их другими эквивалентными программами. В качестве примера возьмем следующую программу Scala

def foo: Int =
  if (1 > 0) 15 else "never happens"

Средство проверки типов отклонит его, поскольку выражение if (1 > 0) 15 else "never happens" формально имеет тип Any. Когда вы запустите его, он обязательно вернет целое число, но без оценки 1 > 0 вы не можете быть уверены, что он не вернет строку. Вы можете написать на Python

def foo():
  if 1 > 0:
    return 15
  else:
    return "never happens"

и компилятору Python все равно.

Конечно, есть программы, эквивалентные этой, которые вы можете написать в Scala, самое простое из которых

def foo: Int = 15

Answer 5

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

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

Вот одна цитата, которая предлагает окно в обмен:

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

и в работающем примере показан случай, когда статически типизированная программа запрещает полезное / интересное поведение по своей природе.

Answer 6

Я думаю, eval-функция иногда может быть удобной, но не обязательной (это редко встречается в статически типизированном языке, см. Объяснение по ссылке).

Answer 7

Если вы посмотрите на книгу Митчелла «Концепции в языках программирования» стр.134, вы найдете некоторые подробности о том, что называется «консервативностью проверки во время компиляции». Проблема заключается в том, что некоторые «интересные» функции, такие как доступ за пределы массива, не могут быть проверены статически, поскольку они потребуют оценки программы / каждого возможного запуска программы. Стандартный результат undecidability сообщает, что вам нужно решить проблему Halting, чтобы действительно проверить КАЖДЫЙ доступ к массиву.

Answer 8

Каковы пределы проверки типов и систем типов?

Я собираюсь предположить, что «системы типов» подразумевают статически типизированный язык программирования.

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

Answer 9

Spec # имеет систему типов с ненулевыми типами и является статически безопасным. (http://research.microsoft.com/en-us/projects/specsharp/)

Answer 10

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

Это правильная программа на python, которая отвечает на вопрос, каковы абсолютные значения 5 и -5.

def abs(x):
    def signum(f):
        if f > 0:
            return 1
        else:
            return "non-positive"
    if signum(x) == 1:
        return x
    else:
        return -x

print("abs(5) = %r and abs(-5) = %r" % (abs(5), abs(-5)))

Очевидно, что abs и signum принимают int как параметр; abs всегда возвращает int, но signum может возвращать int или string. Теперь, если мы введем средство проверки типов (но не средство проверки типов; средство проверки типов в scala просто скажет «signum is int->Any»!), Эта программа будет отклонена ... но она верна и никогда не завершится с несоответствие типов как причина сбоя.