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

Ответ 1

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

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

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

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

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

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

Ответ 2

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

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

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

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

Ответ 3

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

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

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

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

Ответ 4

Я думаю, что есть недоразумение. Это правда, что любая система типов отклонит правильную программу (я не помню точное имя результата, поэтому я не могу сейчас это посмотреть, извините). В то же время верно, что любой полный язык Turing может делать то же самое, что и любой другой, поэтому неверно, что есть некоторые программы на динамически типизированных языках, которые вы не можете воспроизвести, скажем, в 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

Ответ 5

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

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

Здесь одна цитата, которая предлагает окно в компромисс:

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

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

Ответ 6

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

Ответ 7

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

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

"Интересные" программы? Конечно. Легче записывать расширения с динамического языка. Кроме того, в распределенных системах может быть очень удобно иметь слабо типизированный пользовательский интерфейс и не создавать отдельные объекты передачи данных. Например, если у вас был внешний интерфейс JavaScript и базовый сервер С#, вы можете использовать LINQ на конце С# для создания анонимных классов и отправки их на ваш Javascript через JSON. С уровня JS вы можете просто использовать эти анонимные типы, как если бы они были первоклассными объектами и не нуждались в большем кодировании всех ваших контрактов данных явно.

Ответ 8

Вот простой пример (в Python, но полностью не связанный с его проблемами ввода):

# The company deals with rectangles. They have horizontal and vertical lengths
# that should not be mixed. Programmer A writes:

class Rectange:
    def __init__(self, width, height):
        enforce_type('horizontal', width)
        enforce_type('vertical', height)
        #
        # A: Hehe! I'm so smart! With my patented type system if I try to
        #    write "width * width" I'll have a loud error so I'll know I'm wrong.  
        #
        area = width * height
        enforce_type('square_meters', area)
        ...

# Everyone happy. The company shows off A type system on the conference.

...

# Much later, the clients request ability to specify square by entering only 
# one length. Programmer B writes:

class Square(Rectangle):
    def __init__(self, width):
         Rectange.__init__(self, width, width)
         # !!
         # Error happens! 'horizontal' is not 'vertical'!
         #
         # B: Dear Management, I would like to request a weeklong leave since I 
         #    have to track Programmer A house and either talk him into changing
         #    his patented type system or BEAT HIM WITH MY LAPTOP until he agrees.
         #

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

Чтобы ответить на ваш прямой вопрос, на чьей стороне вы находитесь: программист A или программист B?

Ответ 9

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

Некоторые интересные неприятности с очень строгим статическим анализом в системах алгебраических типов заключаются в том, что очень сложно иметь контейнер, содержащий смесь объектов разных типов.

Например, на большинстве основных языков вы можете иметь гетерогенную смесь типов в списке. Пример в python:

["a",1,"b",2]

Чтобы сделать это в строгой системе типов, вам нужно будет сделать унифицированный тип упаковки, а затем шаблон соответствовать всем возможным типам.

Но реальная интересная вещь, которая отсутствует на языках, - это мощная интроспекция, которую вы имеете на самом современном языке (например, С#, Java, Python, Ruby, Lisp).

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

Ответ 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"!) Эта программа будет отвергнута... однако, она правильная и никогда не будет сбой с несогласованностью в качестве причины сбоя.

Ответ 11

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

Ответ 12

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

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

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

Ответ 13

Если вы посмотрите Концепции книги Митчелла на языках программирования, вы найдете некоторые подробности о том, что называется "Консервативность" проверки времени компиляции ". Проблема в том, что некоторые" интересные" функции, такие как обратные вызовы для массивов, не могут быть проверены статически, так как они потребуют оценки программы/каждого возможного прогона программы. Стандартный результат неразрешимости говорит, что вам придется решить проблему с остановкой, чтобы действительно проверить доступ к КАЖДОМУ массиву.