Алгоритм Хиндли-Милнера:использование типов для обеспечения применения привязок

Question

Я реализую алгоритм вывода типа Хиндли-Милнера, следуя учебникам Марк Джонс и Олег Киселёв.Оба из них имеют операцию «применить привязки» типа примерно такого вида

applyBindings :: TyEnv -> Type -> Type

который применяет tyvar -> ty привязки в TyEnv к данному Type.Я обнаружил, что в моем коде распространенной ошибкой является забывание вызвать applyBindings, и я не получаю никакой помощи от системы типов Haskell, поскольку ty имеет тот же тип, что и applyBindings tyenv ty.Я ищу способ обеспечить соблюдение следующего инварианта в системе типов:

при выполнении вывода типа привязки должны применяться до возврата «окончательного» результата

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

-- | Types not containing unification variables
type Type = ...          -- (Fix TypeF) in wren's package

-- | Types possibly containing unification variables
type MutType = ...       -- (MutTerm IntVar TypeF) in wren's package

и дать applyBindings тип

-- | Apply all bindings, returning Nothing if there are still free variables
-- otherwise just
applyBindings :: TyEnv -> MutType -> Maybe Type

(эта функция на самом деле freeze . applyBindings в унификации-fd).Это обеспечивает соблюдение нашего инварианта — если мы забудем applyBindings, то мы получим ошибку типа.

Это то решение, которое я ищу, но для объектных языков с полиморфизмом.Вышеупомянутый подход в его нынешнем виде неприменим, поскольку наши типы объектного языка могут иметь переменные типа - действительно, если после применения привязок есть свободные переменные, мы не хотим возвращать Nothing, но мы хотим обобщить эти переменные.

Есть ли решение в соответствии с тем, что я описываю, т.е.тот, который дает applyBindings другой тип от const id?Используют ли настоящие компиляторы те же каламбуры (между унификационными переменными и переменными типа объектного языка), что и в руководствах Марка и Олега?

Answer 1

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

• Ваша программа проверки типов должна иметь другой представления для переменные типа объединения и переменные типа объектного языка.

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