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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Сейбел:Как размышления над типом данных соотносятся с кодированием? Набросав типы, вы можете приниматься за код? Или, наоборот, написание кода помогает в понимании типов?

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

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

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

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