Как вывод типа работает при наличии функциональных зависимостей
Рассмотрим код ниже:
{-# LANGUAGE MultiParamTypeClasses,FlexibleInstances,FunctionalDependencies,UndecidableInstances,FlexibleContexts #-}
class Foo a c | a -> c
instance Foo Int Float
f :: (Foo Int a) => Int -> a
f = undefined
Теперь, когда я вижу предполагаемый тип F в GHCI
> :t f
> f :: Int -> Float
Теперь, если я добавлю следующий код
g :: Int -> Float
g = undefined
h :: (Foo Int a) => Int -> a
h = g
Я получаю ошибку
Could not deduce (a ~ Float)
Я не могу понять, что здесь произошло? ОграничениеFoo Int a
должен был ограничить типh
вInt -> Float
как показано в предполагаемом типе.f
Это потому, что объединение типов происходит перед разрешением экземпляров?
[Обновить]
Объяснение, данное Дэном Доэлом в списке рассылки кафе
Я считаю, что ответ заключается в том, что различие между реализацией fundep и семействами типов заключается в информации о локальных ограничениях. Фундепс не имеет локального распространения.
Итак, в вашем первом определении вымы предоставляем локальноInt -> a
, что является приемлемым для GHC. Затем он вычисляет внешне функцию, которая(Foo Int a) => Int -> a
на самом деле .Int -> Float
Во втором определении выпытаемся датьInt -> Float
, но GHC знает только локально, что вы должны предоставить ''Int -> a
с ограничением ''Foo Int a
что этоне будет использовать, чтобы определить это.a ~ Float
Это не присуще fundeps. Можно создать версию fundeps, которая имеет локальные правила ограничения (легко сделать это путем перевода на новый тип семейств типов). Но различие также является причиной того, что перекрывающиеся экземпляры поддерживаются для fundeps, а не для семейств типов. Но я выигралпрямо сейчас.
Я до сих пор нене понимаю, что это значит. Поэтому все еще ищем более понятный ответ.