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

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

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

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

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

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

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

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

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

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

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

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

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

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

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