Кодеры за работой

Сейбел: Когда сторонники динамической и статической типизации начинают препираться, первые говорят: «Очень много программ, где статическая типизация мешает мне написать то, что я хочу». А вторые отвечают: «Да, такие программы есть, но на практике это не составляет проблемы». Что вы думаете по этому поводу?

Пейтон-Джонс: Это отчасти зависит от привычки. Я, например, говорю, что так и не привык писать на C++. С другой стороны, вы не будете страдать от отсутствия ленивых вычислений, если вообще ими не пользовались, а я буду, потому что пользуюсь ими постоянно. Возможно, динамическая типизация — похожий случай. Мое ощущение — насколько оно может быть ценным с моим специфическим опытом — таково, что крупные программные блоки вполне могут иметь статическую типизацию, особенно в таких богатых системах типизации. И там, где такая типизация возможна, она очень полезна по неоднократно приводившимся причинам.

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

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

Еще одно: статическая типизация для меня отчасти объясняет, что именно делает программа. Это такой не очень развитый язык, на котором я могу сказать что-то по поводу действий программы. Меня часто спрашивают: «Где в функциональном языке аналог UML-схем?» Думаю, лучший ответ — «система типизации». Там, где объектно-ориентированный программист будет рисовать картинки, я стану создавать сигнатуры типов. Они, конечно, не схемы, но поскольку мы в формальном языке, то они есть неотъемлемая часть текста программы и статически проверяются в коде, который я пишу. Поэтому у них масса достоинств. Это почти архитектурное представление того, что делает программа.

Сейбел:

А вам приходилось писать такие программы, про которые известно, что они корректны, но по каким-то причинам выходят за границы проверки типов?

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

Сейчас есть целая мини-индустрия, которая исследует возможности применения типизации в программах с обобщенными типами. Это очень увлекательно. Но проще взять язык динамического типа. Я пытаюсь убедить Джона Хьюза написать статью для «Journal of Functional Programming» о том, чем плоха статическая типизация. Думаю, это будет интересная статья, если Джон — сторонник строгой типизации, изощренный прикладной функциональный программист, который сейчас пишет много на нетипизированном Erlang, — объяснит, чем плоха статическая типизация. Полагаю, статья будет полна интересных размышлений. Не знаю, чем все это закончится.

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

Сторонники зависимых типов сказали бы: «В конце концов, система типизации сможет выражать абсолютно все». Но система типизации — это забавная штука, нечто вроде компактного языка спецификации. Она говорит кое-что о функции, но не настолько много, чтобы это не поместилось в вашей голове. Поэтому важна четкость. Система типизации на двух страницах перестает передавать нужную информацию.

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

Сейбел:

Что-то вроде контрактного программирования в Eiffel?

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

Сейбел: Как вы подходите к проектированию программ?

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