Наши партнеры

UnixForum

Библиотека сайта rus-linux.net

Компилятор Glasgow Haskell

Глава 5 из книги "Архитектура приложений с открытым исходным кодом", том 2.

Оригинал: The Glasgow Haskell Compiler
Авторы: Simon Marlow и Simon Peyton-Jones
Перевод: Н.Ромоданов

5.3. Ключевые проектные решения

В этом разделе мы сосредоточимся на нескольких проектных решений, которые оказались особенно эффективными в компиляторе GHC.

Промежуточный язык

>

Выражения

 

t,e,u

::=

x

Переменные

 

|

K

Конструкторы данных

 

|

k

Литералы

 

|

λ x:σ.e|e u

Абстракция значений и приложения

 

|

Λ a:η.e |e φ

Абстракция типов и приложения

 

|

let x:τ = e in u

Локальное связывание

 

|

case e of p→u

Выражения типа case

 

|

e ▷ γ

Приведения типов

 

|

⌊ γ ⌋

Ограничения

p

::=

K c:η x:τ

Шаблоны

Рис.5.3: Синтаксис языка Core

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

Промежуточный язык, используемый в компиляторе GHC, называется Core (когда рассматриваем реализацию) или системой FC (когда мы имеем дело с теорией). Его синтаксис приведен на рисунке 5.3. Точные детали здесь не важны, более подробную информацию заинтересованный читатель может найти в [SCPD07]. Однако, для наших целей ключевыми являются следующие моменты:

  • Язык Haskell является языком с очень большим исходным кодом. Тип данных, представляющий его синтаксическое дерево, имеет буквально сотни конструкторов.

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

  • Язык Haskell является языком с неявно типизированным исходным кодом. В программе может быть мало или совсем нет быть аннотации типов; вместо этого в ней используется алгоритм вывода типов для того, чтобы выяснить тип каждого компонента и подвыражения. Этот алгоритм вывода типов сложный и иногда опирается на на проектные компромиссы, которые есть в каждом настоящем языке программирования.

    Язык Core, наоборот, является языком с явной типизацией. Для каждого компонента явно указывается его тип, а в термах (конструктах языка — прим.пер) явно указывается типы и правила использования. В языке Core используется очень простой, быстрый алгоритм проверки типов, который проверяет, что программа является правильной с точки зрения использования типов. Алгоритм достаточно очевиден; специальные компромиссы отсутствуют.

Весь анализ и оптимизация, которые выполняются компилятором GHC, переносятся в язык Core. Это очень удобно: поскольку Core является таким крошечным языком, есть всего несколько вариантов оптимизации. Хотя язык Core небольшой, он крайне выразителен, система F, в конце концов, изначально разрабатывалась как фундаментальное исчисление для типизированных расчетов. Когда к языку, на котором пишется исходный код, добавляются новые возможности (что иногда происходит), изменения, как правило, ограничены только внешним языком; неизменным остается язык Core, и, следовательно, большая часть компилятора.

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

Тем не менее, наличие явно типизированного промежуточного языка стало огромной победой по следующим нескольким причинам:

  • Запуск программы проверки типов в Core (назовем ее Lint) является очень мощным средством целостности данных в самом компиляторе. Представьте себе, что вы пишете «оптимизацию», случайно создающую код, который трактует целое значение как функцию, и пытается ее вызвать. Есть вероятность того, что в программе произойдет ошибка сегментации, либо во время выполнения программы причудливым образом возникнет ошибка. Трассировка ошибки сегментации вернет программу обратно на соответствующий этап оптимизации, из-за которой программа была выведена из строя.

    А теперь представьте, что вместо этого мы запускаем проверку типов Lint после каждого прохода оптимизации (и мы делаем это, если вы используете флаг -dcore-lint): она сразу после неправильной оптимизации точно сообщит о том, где находится ошибка. Хвала всевышнему.

    Конечно, устойчивость типов не то же самое, что и корректность: Lint не будет сигнализировать об ошибке, если вы «оптимизировали» выражение (х * 1) до 1 вместо х. Но если программа проходит проверку Lint, то это будет гарантировать, что она будет работать без ошибок сегментации, и, кроме того, на практике мы обнаружили, что это удивительно трудно случайно написать оптимизацию, при которой сохраняется правильность типов, но нарушается семантическая корректность.

  • Алгоритм вывода типов для языка Haskell очень большой и очень сложный: взгляд на рисунок 5.1 подтверждает, что контроль типов на сегодняшний день является самым большим компонентом компилятора GHC. Большой размер и сложность означают то, что могут быть ошибки. Но Lint выступает в роли 100%-й независимой проверки типов в движке вывода типов; если движок вывода типов принимает программу, которая, на самом деле, не является корректной с точки зрения типов, то Lint отвергнет ее. Поэтому Lint выступает в роли мощного аудитора движка вывода типов.
  • Наличие языка Core также оказалось важной проверкой на вменяемость конструкций исходного языка. Наши пользователи постоянно предлагают новые функции, которые они хотели бы видеть в языке. Иногда эти функции являются явным «синтаксическим сахаром», т. е. удобным новым синтаксисом для чего-то, что вы можете уже делать. Но иногда они могут более глубокими, и, возможно, сразу трудно сказать, как далеко будет простираться эта функция.

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

На практике язык Core оказался невероятно стабильным: в течение 20-летнего периода мы добавили в Core ровно одну новую основную возможность (а именно, coercions и связанные с ней приведения типов). За тот же период, исходный язык был расширен весьма существенно. Мы объясняем эту стабильность не нашими собственными достижениями, а, скорее всего, тем, что Core базируется на фундаментальной математике: браво Жерар!

Продолжение статьи: Проверка типов исходного языка