Подтвердить что ты не робот

Почему GHC typecheck перед десурацией?

Есть ли веская причина для запуска typechecker? Казалось бы, typechecker был бы намного проще, если бы он работал с меньшим синтаксисом, особенно потому, что с текущей системой каждое расширение синтаксиса должно касаться typechecker. Этот вопрос применим, в частности, к синтаксису стрелок, определение типов, которое как описано в комментариях здесь, является фиктивным.

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

4b9b3361

Ответ 1

В разделе статьи GHC содержится раздел по этому вопросу, который содержится в томе 2 книги "Архитектура приложения с открытым исходным кодом":

Тип Проверка исходного языка

Одно интересное дизайнерское решение следует ли проверять тип проверки до или после десурагирования. компромиссы таковы:

  • Проверка типа перед десурацией означает, что контролер типа должен иметь дело непосредственно с очень сильным синтаксисом Haskell, поэтому проверка типа многие случаи для рассмотрения. Если мы отвлечемся (нетипизированный вариант) Во-первых, можно надеяться, что средство проверки типов станет много меньше.

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

  • Скорее всего, тип проверки десугасированной программы сделает это гораздо сложнее сообщить об ошибках, связанных с исходным текстом программы, а не его (иногда сложной) версии.

Большинство тестов типов компиляторов после desugaring, но для GHC мы сделали противоположный выбор: мы печатаем полный исходный синтаксис Haskell, а затем результат. Похоже, что добавление новой синтаксической конструкции может быть но (после французской школы) мы структурировали так что это упрощает процесс ввода вывода. Вывод типа разделены на две части:

  • Генерация ограничений: пройдите по дереву синтаксиса источника, создав набор ограничений типа. Этот шаг касается полного синтаксиса из Haskell, но это очень простой код, и его легко добавить новые случаи.

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

В целом, выбор типа-check-before-desugar был большим выиграть. Да, он добавляет строки кода в средство проверки типов, но они простые линии. Это позволяет избежать двух противоположных ролей для одних и тех же данных тип и делает механизм вывода типа менее сложным и проще изменить. Более того, сообщения об ошибках типа GHC довольно хороши.