Я написал некоторый код Haskell, который нужно -XUndecidableInstances для компиляции. Я понимаю, почему это происходит, что есть определенное условие, которое нарушается, и поэтому GHC кричит.
Тем не менее, я никогда не сталкивался с ситуацией, когда средство проверки типов фактически зависало или заканчивалось в бесконечном цикле.
Что представляет собой определение без конечного экземпляра - можете ли вы привести пример?
Например:
{-# LANGUAGE UndecidableInstances #-}
class C a where
f :: a -> a
instance C [[a]] => C [a] where
f = id
g x = x + f [x]
Что происходит: при вводе f [x] компилятор должен гарантировать, что x :: C [a] для некоторого a. В объявлении экземпляра указано, что x может иметь тип C [a], только если он также имеет тип C [[a]]. Поэтому компилятор должен гарантировать, что x :: C [[a]] и т.д. И попадает в бесконечный цикл.
Там классический, несколько тревожный пример (с участием взаимодействия с функциональными зависимостями) в этот документ из HQ:
class Mul a b c | a b -> c where
mul :: a -> b -> c
instance Mul a b c => Mul a [b] [c] where
mul a = map (mul a)
f b x y = if b then mul x [y] else y
Нам нужно mul x [y] иметь тот же тип, что и y, поэтому, принимая x :: x и y :: y, нам нужно
instance Mul x [y] y
который, согласно данному экземпляру, может иметь. Разумеется, для некоторого z мы должны взять y ~ [z] такое, что
instance Mul x y z
то есть.
instance Mul x [z] z
и мы находимся в цикле.
Это вызывает беспокойство, поскольку этот экземпляр Mul выглядит так, что его рекурсия структурно уменьшается, в отличие от явно патологического примера в ответе Петра. Тем не менее, он делает цикл GHC (с порогом скуки, чтобы избежать зависания).
Проблема, поскольку я уверен, что я уже упоминал где-то, что идентификация y ~ [z] выполняется, несмотря на то, что z функционально зависит от y. Если бы мы использовали функциональную нотацию для функциональной зависимости, мы могли бы заметить, что ограничение говорит y ~ Mul x [y] и отклоняет подстановку как в случае нарушения проверки на наличие.
Заинтригованный, я думал, что дам это вихрем,
class Mul' a b where
type MulT a b
mul' :: a -> b -> MulT a b
instance Mul' a b => Mul' a [b] where
type MulT a [b] = [MulT a b]
mul' a = map (mul' a)
g b x y = if b then mul' x [y] else y
При включенном UndecidableInstances для цикла требуется довольно много времени. При отключенном UndecidableInstances экземпляр по-прежнему принимается, и typechecker все еще работает, но обрезание происходит намного быстрее.
Итак... смешной старый мир.