Адаптация статьи What do types mean for programmers? (Ville Tirronen)

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

Основное значение слова «Тип»

Что имеют в виду учёные-информатики или программисты, когда используют слово «тип»? В обычном смысле слово «тип» используется в таких предложениях, как «не люблю этот тип людей» или «есть разные типы лыж». Его синонимы включают такие слова, как «вид», «род», «класс», «семейство» и т.п. (забавно, что эти слова в английском языке также являются ключевыми в некоторых языках программирования: kind, sort, class, …). Мы используем это слово, чтобы выразить мысль, что некоторые вещи отличаются от других, обычно по какому-то фундаментальному признаку. И именно это, я считаю, также объясняет происхождение данного термина в программировании.

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

Почему именно программисты говорят о типах?

Возможно, вы уже знаете, что всё, что обрабатывается компьютером, представляется в виде последовательностей нулей или единиц. Это дает основное представление о том, что происходит внутри компьютера. Вот конкретный пример: число 1 часто представляется в виде последовательности битов 00000001, число 2 – в виде 00000010, число 3 – в виде 00000011 и так далее. Аналогичным образом буква a часто кодируется как 01100001, а b – как 01100010.

Таким образом, чтобы правильно произвести обработку, необходимо знать, как интерпретировать данные битовые последовательности. Если вы проявите небрежность и прочитаете 01100001 как число, вы получите 97 вместо a. Это разные типы.

Однако с тех пор, как перфокарты вышли из моды (главным образом из-за того, что их использование было тем еще испытанием для нервов), программисты на самом деле не работают непосредственно с битами. Вместо этого мы немедленно переходим к разговору о разных видах чисел, адресов памяти и строках символов (все они автоматически конвертируются в биты компьютером и для компьютера). Думать о вещах в памяти компьютера как о различных типах, таких как числа или символы, гораздо эффективнее, чем думать о битах. Как минимум, типы позволяют нам обсуждать реализацию программ – вы можете сказать своему соседу: «Эта программа работает с числами и ее нельзя использовать с текстом».

ArnoldReinhold, CC BY-SA 3.0 https://creativecommons.org/licenses/by-sa/3.0, via Wikimedia Commons

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

Типы и проверка типов

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

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

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

Динамический подход

Динамическая типизация возникла из идеи о том, что использовать одну и ту же последовательность битов для обозначения двух разных вещей несколько неразумно. По смыслу этой концепции мы могли бы закодировать символ a как 00 01100001, а число 97 как 01 01100001 вместо того, чтобы представлять их оба в виде последовательности 01100001 и создавать двусмысленность. Поступая таким образом, мы даем компьютеру возможность проверить первые два бита до исполнения программы. Если эти биты 00, то у нас буква, а если 01 – то число. А в случае, если типы перепутают, компьютер может предотвратить катастрофу, безопасно остановив обработку.

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

Статический подход

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

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

Плюсы и минусы динамической типизации

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

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

Однако динамическая типизация имеет свои преимущества. Самое очевидное – она может быть значительно более гибкой, чем статический подход. Статическая проверка, будучи более сложной задачей, ограничивает программиста написанием только таких программ, правильность которых можно доказать. Это также может потребовать дополнительных действий, например, написания аннотаций для тайпчекера. У динамической типизации таких ограничений нет – засчитывается любая ваша программа, если только она не приводит к дикому смешению типов. Кроме того, динамические системы обычно более устойчивы к определенным изменениям. Если не все, то многие динамические языки следуют принципу «утиной (неявной) типизации»: вы можете свободно менять типы данных, которыми манипулируете в программе, если новые типы поддерживают такие же операции, что и предыдущие.

Плюсы и минусы статической типизации

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

Динамическая типизация с тестированием кажется практически аналогичной по безопасности и, возможно, более эргономичной, разве не так? Однако в чем тогда преимущества статической типизации? Не углубляясь в сложные случаи использования статических типов, можно назвать следующие. Во-первых, они действительно лучше гарантируют выполнение некоторых простых условий, чем динамические типы. Если программа проверяет соответствие типов, мы без тестирования узнаем, что некоторые вещи выполняются для всех входных данных. Во-вторых, видится некоторое когнитивное преимущество в том, чтобы заставлять программистов четко писать, о чем (о каких типах вещей) они говорят.

Однако что лучше?

А теперь мы попадаем на спорную территорию! И статические и динамические системы имеют ярых приверженцев, которым, по-видимому, нравится спорить в интернете по поводу типов. По их словам, «не использовать статическую типизацию – неэтично» или «статическая типизация – удел слабоумных». «Почему нужно ждать выполнения программы, чтобы убедиться, что она работает неправильно?», «Почему нужно тратить кучу времени, пытаясь убедить тайпчекер в том, что программа работает корректно?». Но мы здесь собрались не ради споров.

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

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

Незатейливая связь между статическими и динамическими типами

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

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

Таким же образом мы зачастую можем определить типы, представляющие концепцию «одного из нескольких вариантов». К примеру, счет заказчика может быть либо «действующим», либо «просроченным», либо «аннулированным (в определенный день)». Все эти варианты можно представить одним типом. Аналогичным образом программа может возвращать «ошибку в виде текста» или «результат в виде числа», а мы используем один тип, чтобы это смоделировать. Для таких типов существуют некоторые метаданные среды выполнения, которые позволяют компьютеру определить, какой конкретный случай они представляют. Типы, которые могут быть «либо этим, либо тем», иногда называются типами-суммами.

Так вышло, что типы-суммы позволяют получить интересное представление о связи между статическими и динамическими типами. По сути, они позволяют системам со статической типизацией демонстрировать поведение динамической типизации! Например, если мы хотим создать программу, которая может принимать либо тип Заказчик, либо тип Адрес, мы можем просто создать тип-сумму, содержащий оба этих типа и заставить нашу программу принять этот новый тип. Для этого нам не нужна динамическая типизация.

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

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

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

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

Но что же такое статические типы?

До сих пор мы говорили о типе как об атрибуте данных. То есть существует некоторая последовательность нулей и единиц, в которой заключается «суть типа». Эта последовательность 01100001 является «Числом». Однако когда мы начинали разговор о проверке статических типов, мы неожиданно сказали, что мы проводим проверку типов, не выполняя программу и даже не имея никаких данных. Если типы являются свойством данных, то что мы здесь проверяем? Явно не типы, так как если данных нет, то и типа быть не может!

Конечно, можно заявить, что мы делаем проверку на наличие возможных проблем, которые могут проявиться как несоответствие типов в процессе выполнения программы. То есть можно представить, как мы говорим о типах в том смысле, что «когда программа будет исполняться, список заказчики будет содержать данные типа Заказчик». Однако это выглядит как умственная гимнастика и уж точно не похоже на то, как мы говорим о проверке типов. Вместо этого мы прямо говорим, что заказчики – это список, содержащий значения типа Заказчик. Вместо этого мы говорим о символах на экране. «Видишь вот это выражение, которое имеет тип Int?».

Таким образом, на профессиональном сленге статической типизации вещи, которые имеют типы, фактически являются не данными, а фрагментами программного кода. Выражение 1 + 1, а не битовая последовательность 0000010 в памяти компьютера, как раз имеет тип Int. Фактически существуют вещи с типами, которые никогда не хранятся в памяти компьютера. Например, константные выражения, такие как 1+1, зачастую исключаются перед выполнением программы. Более того, учитывая достаточно богатую систему типов, мы можем определять такие типы, как Void (как в Haskell), которые вообще никак не могут быть представлены во время выполнения, однако помогают нам выражать что-то в нашем коде.

Таким образом, на практике динамическая типизация и статическая типизация говорят о неявно – или довольно явно – различающихся вещах.

Математика и статические типы

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

Математики на несколько сотен лет опередили учёных-информатиков с концепцией типа (статического). На заре 20 века математики начали заниматься теориями, которые могли бы служить надежной основой для математики. К этим исследованиям относится, по-видимому, первое упоминание типов, которое соответствует взгляду программистов на эту тему в современной статической типизации.

Бертран Рассел

Есть интересная история о том, как это произошло. Бертран Рассел, один из математиков, занимающихся фундаментальными исследованиями, случайно обнаружил ошибку или парадокс в основе этих исследований. Математическое множество представляет собой объект, который может содержать или не содержать какие-то другие объекты. У вас может быть множество основных цветов ({красный, зеленый, синий}) или даже множество всех множеств. Вы также можете случайно изобрести множество всех множеств, которые не содержат самих себя. Однако если данное множество включает само себя, то этого не должно быть и наоборот. Парадокс!

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

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

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

Alonzo Church @ University of Berkeley

Типы Рассела не имеют практически ничего общего с программированием, в отличие от еще одной концепции типов, изобретенной в середине прошлого века. Логик Алонзо Чёрч случайно обнаружил минимальную вычислительную систему, которая, по-видимому, была способна выразить все вообразимые вычисления. Эта система также имела аналогичные парадоксы, что делало ее непригодной для использования в качестве математической основы (сегодня программисты назвали бы их всего лишь бесконечными циклами или бесконечной рекурсией). Решение было таким же – определить тип для каждого выражения в формуле, а затем проверить его (в текстовом виде) и исходя из этого определить, имеет ли система «смысл».

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

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

Заключение

Когда читаешь споры о динамической и статической типизации в интернете, порою кажется, что находишься на территории абсурда. Одна сторона говорит о типах как о свойствах некоторых выражений в текстовом редакторе, а другая сторона говорит о типах как о свойствах данных. Некоторые проводят математические расчеты. Неудивительно, что возникают споры! И эти споры усугубляются обоснованными подозрениями, что статический и динамический способы проверки типов различаются слишком сильно, чтобы их можно было сравнивать. Например, я могу написать код на Python с динамической проверкой типов без особых проблем. Но я сомневаюсь, что смогу написать какой-либо код на Haskell без статической проверки типов. Нет смысла сравнивать динамические и статические языки в надежде понять, какая типизация – статическая или динамическая – лучше.

И конечно, здесь говорилось не обо всем, что связано с типами в языках программирования! В F# есть «type providers», которые выходят за рамки простой проверки программного кода и извлекают информацию о типах из внешних источников, таких как база данных. Например, можно сказать: «Эй, компилятор, найди-ка все возможные значения для поля Х в базе данных и назови это множество типом T». Есть постепенная типизация, направленная на построение системы, где динамические и статические типы образуют гладкий континуум, в котором разработчики могут переходить с одного типа на другой в зависимости от потребностей. Существуют такие языки, как Isabel, где вы программируете доказательства математических теорий, и такие как Idris, где вы создаете доказательства правильности своих программ. Типы приобретают всевозможные неожиданные формы и используются повсеместно.