Почему программа проверки типов GHC принимает этот трюк UndecidableInstance?
GHC принимает следующий код.
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE UndecidableInstances #-}
class Blib b where
blib :: b
class Blob b where
blob :: b
instance Blib b => Blob b where
blob = blib
instance Blob b => Blib b where
blib = blob
bad :: ()
bad = blib () 4 'a' -- I can add any number of arguments of any type, it still compiles
main ::IO ()
main = return bad
Еще любопытство:
- когда я запускаю исполняемый файл, он почему-то работает "отлично"
- когда я загружаю его в GHCi и просто набираю
bad, GHCi зависает. - если я удалю объявление для
blibиblobследующим образом, код больше не зависает GHCi:
instance Blib b => Blob b where
-- blob = blib
instance Blob b => Blib b where
-- blib = blob
Что происходит ?
Обратите внимание, что любая функция, тип которой forall a . ...... -> a (включая forall a . SomeConstraint a => a, например blib/blob), может принимать «любое количество аргументов», поскольку можно создать экземпляр a с b1 -> b2 -> ..., заставляя больше аргументов появляться из ничего. Например. id id id id id id id True работает, даже если id выглядит так, будто принимает только один аргумент.
Ответы 1
На самом деле это не имеет ничего общего с UndecidableInstances. Единственное, что делает это расширение, — это позволяет компилировать объявления вашего экземпляра:
instance Blib b => Blob b where
Когда вы накладываете ограничение на экземпляр, ограниченный тип должен быть «меньше», чем заголовок экземпляра. Например:
instance Foo a => Foo [a]
Это ограничение распространяется только на a, который является частью заголовка экземпляра [a]. Это всегда разрешено. Но ваши определения имеют ограничение на тот же тип, что и заголовок экземпляра. Без UndecidableInstances это запрещено.
Но все остальное поведение, которое вы наблюдаете, не связано с этим. Вы получите точно такие же результаты, выполнив что-то вроде:
blib :: b
blib = blob
blob :: b
blob = blib
bad :: ()
bad = blib () 4 'a'
main ::IO ()
main = return bad
blib принимает любое количество аргументов, потому что это буквально любой тип (типа Type). В этом случае вывод (и установка числового литерала по умолчанию на Integer, поскольку ничто не указывает его) определяет его тип как () -> Integer -> Char -> (). Объявленный тип b унифицируется с ним, поэтому ошибки типа нет.
Скомпилированная программа работает нормально, потому что она никогда не вычисляет bad. Скомпилированная программа запускает действие ввода-вывода main и игнорирует значение, создаваемое этим вводом-выводом. Поскольку запуск ввода-вывода никогда не оценивается bad, все это сводится к нулю.
Напротив, ghci работает вечно, потому что вычисление bad для его печати приводит к бесконечной взаимной рекурсии.
Для справки: ghci делает несколько вещей с использованием простых выражений. Стоит иметь в виду, что он пытается выполнить эти действия в следующем порядке:
- Если выведенный тип выражения объединяется с
IO (), оно запускает действие ввода-вывода и ничего не печатает. - Если выведенный тип выражения объединяется с
Show a => IO a, оно запускает действие ввода-вывода и печатает результат. - Если выведенный тип выражения объединяется с
IO a, оно запускает действие ввода-вывода и ничего не печатает. - Он обрабатывает ввод так, как если бы он был
print <expr>для любого введенного вами выражения, и действует так же, как в случае 1 выше.
Предположительно, исполняемый файл выигрывает от оптимизации бесполезных
()вычислений. Что касается произвольных аргументов, это также работает дляundefinedили чего-либо с типомforall a. a, поскольку вы всегда можете объединить их с другими типами функций.