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

Question

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

Chris Smith claims:

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

и

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

Не могли бы вы рассказать, какие интересные программы могут быть такими? Где доказано, что контролеры типов имеют консервативный характер?

И более общий: Каковы пределы систем проверки типов и типов?

Answer 1

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

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

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

Answer 2

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

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

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

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

Answer 3

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

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

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

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

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

Answer 4

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

Answer 5

Вот простой пример (в 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's happy. The company shows off A's 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's house and either talk him into changing 
     # his patented type system or BEAT HIM WITH MY LAPTOP until he agrees. 
     # 

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

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

Answer 6

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

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

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

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

Answer 7

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

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

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

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

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

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

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

Answer 8

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

Это правильная программа 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))) 

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

Answer 9

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

Answer 10

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

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

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

Answer 11

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

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

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

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

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

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

Answer 12

Если вы посмотрите на Mitchell's book Concepts in Programming Languages с.134, вы найдете подробную информацию о так называемой «консервативности проверки времени компиляции». Проблема в том, что некоторые «интересные» функции, такие как обратные вызовы для массивов, не могут быть проверены статически, так как они потребуют оценки программы/каждого возможного прогона программы. Стандартный результат неразрешимости говорит, что вам придется решить проблему с остановкой, чтобы действительно проверить доступ к КАЖДОМУ массиву.

Answer 13

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