Кодеры за работой. Размышления о ремесле программиста - Сейбел Питер

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

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

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

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

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

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

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

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

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

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

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

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

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

Сейбел: Что-то вроде контрактного программирования в Eiffel?

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

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

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

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

Сейчас за это отвечает довольно сложный фрагмент кода. Но недавно я понял, что задача раскладывается на две части: 1) преобразование в диалект С--, позволяющий делать вызовы процедур, когда внутри одной процедуры можно вызвать другую, и 2) преобразование этого в подъязык без всяких вызовов, кроме хвостовых.

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

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

Многие споры шли на уровне типов. Норман говорил: «Вот API», — показывая сигнатуру типов, а я в ответ: «Зачем так сложно?» Он объяснял зачем, а я говорил: «Может быть, вот так будет проще». Так что мы довольно долго бились над описанием типов.

Но много времени уходило не на собственно программирование, а на определение самой идеи. Что мы хотим сделать с анализом потока данных? Надо было дать четкий ответ: что подразумевает такой-то шаг программы. Так что немало времени мы потратили на уточнение того, что у нас на входе и что на выходе, и какие у них типы данных. И всего лишь определив эти типы данных, мы довольно подробно описали работу программы. Даже удивительно, насколько подробно.