Что пределы типа проверяют и системы типов?

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

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

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

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

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

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

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

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

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

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

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

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

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

Вот простой пример (на 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.
         #

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

Чтобы ответить на ваш прямой вопрос, на чьей вы стороне: Программист А или Программист Б?

An interesting example is This Paper, which is probably the only apples-to-apples comparison ever done on static vs dynamic typing. They implemented self (a language like smalltalk, but with prototypes instead of classes,) with both type inference (static), and type feedback (dynamic).

The most interesting result is that the type inference engine had a lot of trouble resolving between machine integers and arbitrary precision integers -- They auto-promoted in vanilla self, and hence could not be told apart by the type system, which meant that the compiler had to include code to promote to BigInt on every integer operation.

They ran up against a limit of their type system: It could not examine the actual value of integers.

I think that there are no theoretical limits to type systems in general, but any given type checker can only deal with a specific, limited type system, and there will be programs where it cannot determine what is going on. Since the self type inferencer allowed for sets of types, it simply compiled both paths. A type checker that required convergence on a single type would have to reject the program. (Though it would probably have special code for this case.)

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

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

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

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

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

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

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

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

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

Это правильная программа на 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 или строку. Теперь, если бы мы ввели программу проверки типов (но не любую; проверка типов Scala просто скажет "signum is int->Any" !), эта программа была бы отвергнута... однако, она корректна и никогда не завершится с несоответствием строковому типу в качестве причины сбоя.

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

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

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

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

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

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

Каковы границы проверки типов и систем типов?

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

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

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