Каковы пределы проверки типов и систем типов? - PullRequest
Новая
       100

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

18 голосов
/ 09 августа 2009

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

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

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

и

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

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

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

Ответы [ 13 ]

0 голосов
/ 13 июля 2010

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

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

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

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

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

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

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

0 голосов
/ 14 августа 2009

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

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

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

0 голосов
/ 09 августа 2009

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

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

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

Страница:
...