Как преобразовать неудавшееся вычисление в успешное и наоборот

_{Это вполне может быть решением, ищущим проблему... если это так, я прошу вашего снисхождения!}

Возможная реализация:

class Switch' f where
  switch :: f a -> f ()

instance Switch' [] where
  switch []     = [()]
  switch (_:_)  = []

instance Switch' Maybe where
  switch Nothing   = Just ()
  switch (Just _)  = Nothing

Интерпретация будет: при успешном вычислении сделать ее неудачной; учитывая неудачное вычисление, сделайте его успешным. Я не уверен, но похоже, что это может быть что-то вроде противоположности MonadPlus... если вы сильно усмехнулись.???

Существует ли стандартная модель или другая реализация для этой концепции? Что бы выглядела нижележащая математика, если таковая имеется (т.е. Это полугруппа, цикл и т.д.)?

Ответы

Ответ 1

switch :: (Alternative f, Eq (f a)) => f a -> f ()
switch x | x == empty = pure ()
         | otherwise = empty

или

switch :: (MonadPlus m, Eq (m a)) => m a -> m ()
switch x | x == mzero = return ()
         | otherwise = mzero

Ответ 2

У меня есть общее решение, но оно может работать только для экземпляров MonadPlus, которые подчиняются закону left catch (и что, вероятно, только необходимое условие, недостаточно):

isZero :: (MonadPlus m) => m a -> m Bool
isZero x = (x >> return False) `mplus` return True

switch :: (MonadPlus m) => m a -> m ()
switch x = isZero x >>= \r -> if r then return () else mzero

Он работает для STM.

(Для списков он всегда возвращает [()], хотя я бы сказал, что это определение не будет работать ни на что, что удовлетворяет левому распределению.)

Невозможно определить его таким образом для Applicative s, потому что switch проверяет значение isZero, и аппликаторы не могут этого сделать. (И, MonadPlus экземпляры, которые удовлетворяют правилу левого лова редко удовлетворяют законам Applicative.)

Во всяком случае, было бы интересно узнать, подходит ли для этого определения switch . (switch :: m () -> m ()) = id.

Ответ 3

Я нашел совершенно другой ответ, и это LogicT monad transformer. Он имеет lnot, определяемый как:

lnot :: MonadLogic m => m a -> m ()
Инвертирует логическое вычисление. Если m преуспевает с хотя бы одним значением, lnot m терпит неудачу. Если m не работает, то lnot m получает значение ().

Я считаю, что это именно то, что вы хотели.