Экзистенциальные типы и монадные трансформаторы - PullRequest
Новая
       23

Экзистенциальные типы и монадные трансформаторы

7 голосов
/ 22 декабря 2011

Контекст: я пытаюсь создать монаду об ошибке, которая также отслеживает список предупреждений, что-то вроде этого: 

data Dangerous a = forall e w. (Error e, Show e, Show w) =>
    Dangerous (ErrorT e (State [w]) a)

т.е. Dangerous a - это операция, результатом которой является (Either e a, [w]), гдеe - это отображаемая ошибка, а w - отображаемая.

Проблема в том, что мне кажется, что на самом деле я не могу управлять этим, в основном потому, что не очень хорошо понимаю экзистенциальные типы.Заметьте: 

runDangerous :: forall a e w. (Error e, Show e, Show w) =>
    Dangerous a -> (Either e a, [w])
runDangerous (Dangerous f) = runState (runErrorT f) []

Это не компилируется, потому что: 

Could not deduce (w1 ~ w)
from the context (Error e, Show e, Show w)
...
`w1' is a rigidtype variable bound by
    a pattern with constructor
    Dangerous :: forall a e w.
                 (Error e, Show e, Show w) =>
                 ErrorT e (State [w]) a -> Dangerous a
...
`w' is a rigid type variable bound by
    the type signature for
    runDangerous :: (Error e, Show e, Show w) =>
                    Dangerous a -> (Either e a, [w])

Я потерян.Что за w1?Почему мы не можем сделать вывод, что это ~ w?

Ответы [ 2 ]

12 голосов
/ 22 декабря 2011

Экзистенция, вероятно, не то, что вы хотите здесь; нет никакого способа «наблюдать» фактические типы, привязанные к e или w в значении Dangerous a, поэтому вы полностью ограничены операциями, данными вам Error и Show.

Другими словами, единственное, что вы знаете о w, это то, что вы можете превратить его в String, так что это может быть просто String (игнорируя приоритет для упрощения вещей), и единственный Что вы знаете о e, так это то, что вы можете превратить его в String, вы можете превратить в него String s, и у вас есть выдающееся значение этого (noMsg). Невозможно утверждать или проверять, что эти типы такие же, как и любые другие, поэтому после помещения их в Dangerous невозможно восстановить какую-либо специальную структуру, которая может иметь эти типы.

Сообщение об ошибке говорит о том, что, по сути, ваш тип для runDangerous утверждает, что вы можете превратить Dangerous в (Either e a, [w]) для любого e и w, которые есть соответствующие случаи. Это явно не так: вы можете превратить Dangerous в этот тип только для один выбор из e и w: тот, с которым он был создан. w1 только потому, что ваш тип Dangerous определен с переменной типа w, как и runDangerous, поэтому GHC переименовывает одну из них, чтобы избежать конфликта имен.

Тип, который вам нужно дать runDangerous выглядит следующим образом: 

runDangerous
  :: (forall e w. (Error e, Show e, Show w) => (Either e a, [w]) -> r)
  -> Dangerous a -> r

, что, учитывая функцию, которая будет принимать значение типа (Either e a, [w]) для любого вариантов e и w, если у них есть заданные экземпляры, и Dangerous a, производит результат этой функции. Это довольно сложно обдумать!

Реализация так же просто, как 

runDangerous f (Dangerous m) = f $ runState (runErrorT m) []

, что является тривиальным изменением вашей версии. Если это работает для вас, отлично; но я сомневаюсь, что экзистенциальный - это правильный способ достичь того, что вы пытаетесь сделать.

Обратите внимание, что вам понадобится {-# LANGUAGE RankNTypes #-} для выражения типа runDangerous. Кроме того, вы можете определить другой экзистенциальный для вашего типа результата: 

data DangerousResult a = forall e w. (Error e, Show e, Show w) =>
   DangerousResult (Either e a, [w])

runDangerous :: Dangerous a -> DangerousResult a
runDangerous (Dangerous m) = DangerousResult $ runState (runErrorT m) []

и извлеките результат с помощью case, но вам нужно быть осторожным, иначе GHC начнет жаловаться на то, что вы позволили e или w бежать - что эквивалентно попытке пройти недостаточно полиморфная функция к другой форме runDangerous; то есть тот, который требует больше ограничений на то, что e и w выходит за рамки того, что гарантирует тип runDangerous.

1 голос
/ 23 декабря 2011

Хорошо, я думаю, что понял, что я колеблюсь после: 

data Failure = forall e. (Error e, Show e) => Failure e

data Warning = forall w. (Show w) => Warning w

class (Monad m) => Errorable m where
    warn :: (Show w) => w -> m ()
    throw :: (Error e, Show e) => e -> m ()

instance Errorable Dangerous where
    warn w = Dangerous (Right (), [Warning w])
    throw e = Dangerous (Left $ Failure e, [])

(instance Monad Dangerous и data DangerousT справка тоже.)

Это позволяет вам иметь следующеекод: 

foo :: Dangerous Int
foo = do
    when (badThings) (warn $ BadThings with some context)
    when (worseThings) (throw $ BarError with other context)

data FooWarning = BadThings FilePath Int String
instance Show FooWarning where
...

, а затем в главном модуле вы можете определить пользовательские экземпляры Show Failure, Error Failure и Show Warning и иметь централизованный способ форматирования сообщений об ошибках, например 

instance Show Warning where show (Warning s) = "WARNING: " ++ show s
instance Show Failure where ...

let (result, warnings) = runDangerous function
in ...

Это, на мой взгляд, довольно крутой способ обработки ошибок и предупреждений.У меня есть рабочий модуль, похожий на этот, теперь я собираюсь его отшлифовать и, возможно, взломать.Предложения приветствуются.

...