Showing posts with label системы типов. Show all posts
Showing posts with label системы типов. Show all posts

Tuesday, August 14, 2007

Cтатическая и динамическая системы типов: распространенные заблуждения

В продолжение предыдущего поста. В основном, по мотивам этого эссе

Для начала факты:

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

А теперь несколько самых распространенных заблуждений о системах статической и динамической типизации:

1. Статическая типизация подразумевает объявления типов

Дело в том, что Java, Pascal, C++ и C не просто языки со статической типизацией — это языки с явным объявлением типов. Многим не нравится тратить кучу времени на описание типов функций и переменных, и они не любят статически типизированные языки именно по этой причине. Это зря, потому как, скажем в ML и Haskell типы объявлять в большинстве случаев не нужно, при этом они являются на 100% языками с развитой системой статической проверки типов. Вот и в C# (и C++) сейчас видны подвижки в сторону включения в язык неявного вывода типов в некоторых случаях.

2. Динамическая типизация = "слабая" типизация

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

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

А все дело в том, что в динамических языках сам подход другой, главным образом это быстрое написание кода и интенсивное тестирование потом. В динамических языках есть отличные средства для быстрого и четкого отлова рантайм ошибок, с диагностикой, которая покажет вам, почему именно ошибка произошла (см. идеологию "Let it crash" в Erlang.)

3. Статическая типизация не сочетается с итеративными/agile  процессами разработки, заставляет разрабатывать архитектуру целиком и полностью до кодирования, и вообще предполагает водопадную модель.

Некоторые статически типизированные языки и правда устроены так, чтобы стимулировать определенный подход к процессу разработки. Пример этого — требование объявлять все переменные заранее в Паскале, заголовочные файлы в C++ (хотя там это отчасти продиктовано практическими соображениями).

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

4. Языки с динамической типизацией не предоставляют средств для поиска багов на этапе разработки

Распространенный аргумент против динамических языков — это то, что ошибки вылезают у пользователя, а не у разработчика. Однако, в реальности это происходит очень редко, так что аргумент хреновый — программы на динамических языках в среднем содержат не особенно больше ошибок чем на языках вроде C++ и Java. Если это вообще можно измерить.

5.  Статическая типизация ведет к более объемным исходникам

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

Красивый пример из Haskell: есть функция lookup, которая ищет в Map (ассоциативном массиве) значение по ключу. Тип у нее такой:

lookup :: (Monad m, Ord k) => k -> Map k a -> m a

Если кто с хаскелем не знаком — у функции два аргумента, ключ типа k и ассоциативный массив с типом ключа k и типом значений a. Возвращает функция значение типа a, завернутое в монаду m.

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

case (lookup bobBarker employees) of
    Nothing -> hire bobBarker
    Just salary -> pay bobBarker salary

Как Хаскель узнал что мы хотим именно первый вариант, получать значение Nothing в случае ошибки? Он увидел что мы сравниваем результат с Nothing, и вывел соответствующий конкретный тип для монады m. Если б мы не написали этого куска кода, обрабатывающего ошибки сразу, а воткнули бы обработчик ошибок где-нибудь несколькими уровнями выше по стеку — Хаскель тоже правильно вывел бы тип, и можно было б вызывать lookup несколько раз, не заботясь о том, что ключа может не оказаться.

Оригинал: "What To Know Before Debating Type Systems"

 


Monday, August 13, 2007

Типы: микроFAQ/ликбез

В основном это вольный перевод избранных мест из "What To Know Before Debating About Type Systems" и статьи L. Cardelli "Type Systems".

Итак,

Определение

Одного простого и общепринятого определения понятия "тип" или "система типов", как ни странно, нету. Основное назначение системы типов это обнаружение ошибок, которые могут возникнуть при выполнении программы. Весьма известный деятель в области computer science, лауреат премии Тьюринга Лука Карделли приводит такое несложное определение:

Тип переменной -- это множество значений которые может принимать переменная во время выполнения программы.

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

Если хотите чего-нибудь более философского, то можно обратиться к книжке Б. Пирса "Types and Programming Languages", где он дает более хитрое определение для системы типов:

Система типов — это способ доказать за конечное время, основываясь на синтаксисе и классификации фраз программы по видам вычисляемых ими значений, что программа не ведет себя определенным образом.

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

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

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

Строгая типизация

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

Статическая vs Динамическая система типов

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

Если такие операции приводят к каким-то непредсказуемым в общем случае последствиям, можно смело говорить что типов нету вообще. Товарищ Карделли вот называет это untyped unsafe languages, и приводит в пример ассемблер.

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

Карделли вот вообще осознанно не использует термин "динамическая типизация" — вместо этого у него "динамические проверка [значений]", а подобные языки называет untyped safe languages. Это он не потому что считает, что динамические языки это не тру, а потому что путаница получается серьезная.

 Продолжение следует