Функциональные зависимости в Haskell
Я пытаюсь обернуть голову вокруг функциональных зависимостей, но я ничуть не ухожу. В статье "Monad Transformers Step by Step" автор дает эти два определения типов:
class (Monad m) => MonadError e m | m -> e where
throwError :: e -> m a
catchError :: m a -> (e -> m a) -> m a
class (Monad m) => MonadReader r m | m -> r where
ask :: m r
local :: (r -> r) -> m a -> m a
Из моего понимания некоторых материалов, которые я нашел в Интернете, это означает, что переменная типа e
определяется m
. Я просто не понимаю, что это значит. Как это определяется? Может ли кто-нибудь пролить некоторый свет с минимальной теорией вначале, а затем связать более тяжелые вещи теории?
Спасибо
Ответы
Ответ 1
Когда у вас есть многопараметрическое typeclass, по умолчанию переменные типа рассматриваются независимо. Поэтому, когда тип inferencer пытается выяснить, какой экземпляр
class Foo a b
он должен определить a
и b
независимо, затем перейдите посмотреть проверку, чтобы увидеть, существует ли экземпляр. С функциональными зависимостями мы можем сократить этот поиск. Когда мы делаем что-то вроде
class Foo a b | a -> b
Мы говорим: "Посмотрите, если вы определили, что такое a
, тогда существует уникальная b
, поэтому существует Foo a b
, поэтому не пытайтесь сделать вывод b
, просто найдите экземпляр и typecheck, что". Это позволяет типу inferencer намного эффективнее и помогает выводить в ряде мест.
Это особенно полезно при полиморфизме типа возврата, например
class Foo a b c where
bar :: a -> b -> c
Теперь нет способа сделать вывод
bar (bar "foo" 'c') 1
Потому что мы не можем определить c
. Даже если мы написали только один экземпляр для String
и Char
, мы должны предположить, что кто-то может/придет и добавит еще один экземпляр позже. Без fundeps мы должны были бы указать тип возврата, что раздражает. Однако мы могли бы написать
class Foo a b c | a b -> c where
bar :: a -> b -> c
И теперь легко видеть, что возвращаемый тип bar "foo" 'c'
является уникальным и, следовательно, выводимым.
Ответ 2
Когда Haskell пытается разрешить MonadError e m
, он по умолчанию проверяет параметры e
и m
вместе, ища любую пару, которая имеет экземпляр. Это особенно сложно, если у нас нет e
, отображаемого где угодно в сигнатуре типа вне самого ограничения
unitError :: MonadError e m => m ()
unitError = return ()
Функциональная зависимость говорит, что как только мы разрешили m
, может работать только один e
. Это позволяет компиляции вышеуказанного фрагмента, поскольку он убеждает Haskell в том, что там имеется достаточно информации, чтобы он имел не двусмысленный тип.
Без функциональной зависимости Haskell жалуется, что unitError
неоднозначно, потому что он может быть действительным для любого типа e
, и мы не имеем никакого способа узнать, что это за тип: информация каким-то образом испарилась в тонкую воздух.
Для MonadError
функциональная зависимость обычно означает, что сама монада параметризуется по типу ошибки. Например, здесь экземпляр
instance MonadError e (Either e) where
thowError = Left
catchError (Left e) f = f e
catchError (Right a) _ = Right a
Где e ~ e
и m ~ Either e
, и мы видим, что m
действительно однозначно идентифицирует один e
, который может быть действительным.
Функциональные зависимости "почти" эквивалентны типам семейств. Тип Семьи иногда немного легче переваривать. Например, здесь класс MonadError
, тип TypeFamilies
{-# LANGUAGE TypeFamilies #-}
class MonadError m where
type Err m
throwError :: Err m -> m a
catchError :: m a -> (Err m -> m a) -> m a
instance MonadError (Either e) where
type Err (Either e) = e
throwError = Left
catchError (Left e) f = f e
catchError (Right a) _ = Right a
Здесь Err
- это функция типа, которая принимает m
к ее конкретному типу ошибок e
, и понятие, если ровно один e
, равный Err m
для любого m
, естественно возникает из наше понимание функций.
Ответ 3
Это означает, что система типов всегда сможет определить тип (e
или r
) из типа m
.
Давайте сделаем наш собственный пример:
class KnowsA a b | b -> a where
known :: b -> a
Мы всегда должны иметь возможность определить a
из b
data Example1 = Example1 deriving (Show)
instance KnowsA Int Example1 where
known = const 1
Система типов знает, что для этого instnace, когда он имеет Example1
, его тип a
будет Int
. Как это знать? Это не позволяет нам иметь другой экземпляр с другим типом.
Если мы добавим
instance KnowsA [Char] Example1 where
known = const "one"
Мы получаем сообщение об ошибке:
Functional dependencies conflict between instance declarations:
instance KnowsA Int Example1
instance KnowsA [Char] Example1
Но мы можем добавить еще один экземпляр с другим типом для a
, если у нас есть другой тип для b
data Example2 = Example2 deriving (Show)
instance KnowsA [Char] Example2 where
known = const "two"
main = do
print . known $ Example1
print . known $ Example2
Это прогнозирует вывод
1
"two"