Условие согласованности функциональных зависимостей Haskell: нужно ли это? Это используется? - PullRequest
Новая
       32

Условие согласованности функциональных зависимостей Haskell: нужно ли это? Это используется?

0 голосов
/ 02 июля 2018

Условие согласованности FunDep встречается во всей литературе, относящейся к статье Mark P Jones 2000. И это унаследовано от происхождения теории баз данных FunDeps.

Но FunDeps на Haskell не очень похожи на базы данных: FunDep -> означает: в любом случае для этого класса я обещаю дать алгоритм перехода от параметров класса слева к параметрам справа. (В экземпляре decl этот алгоритм может пройти через свои ограничения - тогда вам нужно UndecidableInstances.)

Достаточно хорошо известно, что реализация условия согласованности в GHC является фиктивной - см. этот ответ, например . И это хорошо, так что я могу написать 

class TypeEq a a' (b :: Bool) | a a' -> b  where ...
instance TypeEq a a True  where ...
instance (b ~ False) => TypeEq a a' b  where ...

(для этого нужны OverlappingInstances или прагмы, а также Undecidable.)

Заявления в документах, в том числе в документе FunDeps через документ CHRs 2006, заключаются в том, что условие согласованности необходимо для обеспечения вывода типа слияния. И есть правило вывода, что если у вас есть TypeEq alpha1 alpha2 beta1 и TypeEq alpha1 alpha2 beta2, вы можете заключить beta1 == beta2, в котором == является идентификатором типа, а не просто ~ унифицируемостью.

Но я не вижу доказательств того, что GHC когда-либо применял это правило. И такое ограничение работает просто отлично ( РЕДАКТИРОВАТЬ: моя первая подпись здесь была слишком неприличной даже для GHC, исправлено): 

f :: (TypeEq a a' True, TypeEq a' a False) => a -> a' -> ()
f _ _ = ()

f 'c' 'd'         -- produces `()` happily

Сопоставимая функция, использующая семейства типов, может быть определена, но не может использоваться 

g :: ((a == b) ~ False, (b == a) ~ True) => a -> b -> ()

(необходимо TypeOperators, import Data.Type.Equality) Для g 'c' 'd' или g 'c' "d" GHC жалуется Couldn't match type 'True with 'False.

Тогда условие согласованности - это что-то, кроме неприятности? (На Trac есть несколько билетов, в которых получается очень странное поведение.)

Кто-нибудь на это полагается? Или использовать его для проверки своих экземпляров в случае неловких совпадений?

ADDIT: Вы можете подумать, что подпись для f обманывает, переключая параметры типа params. Эта подпись (мой первоначальный пост) 

f :: (TypeEq a a' True, TypeEq a a' False) => a -> a' -> ()

Получает отклонено Couldn't match type 'False with 'True. Похоже, что GHC применяет правило вывода вызовов с одинаковыми аргументами.

Но с аргументами non-flip все в порядке (потому что две сигнатуры слишком отдаленные?) 

f1 :: (TypeEq a a' False) => a -> a' -> [()]
f1 _ _ = [()]
f2 :: (TypeEq a a' True) => a -> a' -> [()]
f2 _ _ = [()]
-- f3 :: (TypeEq a a' f2', TypeEq a a' f1') => a -> a' -> [()]  
f3 x y = f1 x y ++ f2 x y

То есть, все в порядке, если я не ставлю подпись для f3. (И независимо от того, какую подпись я использую для f3, отклоняет Overlapping instances for TypeEq a b 'True arising from a use of ‘f2’; среди других сообщений.)

...