Алгоритм Хиндли-Милнера: использование типов для обеспечения применения привязок
Я реализую алгоритм вывода типа Хиндли-Милнера, следуя руководствам Марка Джонсаи Олега Киселёва. Оба они имеют операцию «применить привязки» с типом примерно в форме
applyBindings :: TyEnv -> Type -> Type
, которая применяет привязки tyvar -> tyв TyEnvк данному Type. Я обнаружил, что распространенной ошибкой в моем коде является забывание вызвать applyBindings, и я не получаю помощи от системы типов Haskell, поскольку tyимеет тот же тип, что и applyBindings tyenv ты.Я ищу способ реализовать следующий инвариант в системе типов:
при выводе типа привязки должны применяться до возврата «окончательного» результата
При выводе типа для мономорфного объектного языка существует естественный способ реализовать это, реализованный в пакете unification-fd wren ng thornton : мы определяем два типа данных для Types:
-- | 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
(эта функция на самом деле заморозка . applyBindingsв unification-fd). Это применяет наш инвариант — если мы забудем applyBindings, то получим ошибку типа.
Это то решение, которое я ищу, но для объектных языков с полиморфизмом. Приведенный выше подход в его нынешнем виде неприменим, поскольку наши типы объектного языка могут иметь переменные типа — действительно, если переменные свободны после применения привязок, мы не хотим возвращать Nothing, но мы хотим обобщить эти переменные.
Существует ли решение, подобное описанному мной, т. е. такое, которое дает applyBindingsтип, отличный от const id? Используют ли настоящие компиляторы те же каламбуры (между унифицирующими переменными и переменными типа объектного языка), что и в учебниках Марка и Олега?