Доказательства
В этом сообщении в блоге Tekmo заявляет, что мы можем доказать, что ExitSuccess
завершает работу, потому что (я полагаю) он похож на функтор Const
для этого конструктора (он не несет x
, поэтому fmap
ведет себя как Const
).
С операционным пакетом Tekmo TeletypeF
может быть переведено примерно так:
data TeletypeI a where
PutStrLn :: String -> TeletypeI ()
GetLine :: TeletypeI String
ExitSuccess :: TeletypeI ()
Я читал, что операция изоморфна свободной монаде, но можем ли мы доказать, что ExitSuccess
выходит? Мне кажется, что он испытывает ту же проблему, что и exitSuccess :: IO ()
, и, в частности, если мы должны были написать для него интерпретатор, нам нужно было бы написать его так, как будто он не вышел:
eval (ExitSuccess :>>= _) = exitSuccess
Сравните со свободной версией монады, которая не содержит шаблона шаблона:
run (Free ExitSuccess) = exitSuccess
Лень
В учебном пособии Практическое пособие по Монаде apfelmus упоминает недостаток:
Государственная монада, представленная в виде s → (a, s), может справиться с некоторой бесконечной такие программы, как
evalState (sequence . repeat . state $ \s -> (s,s+1)) 0
тогда как список инструкций не имеет никакой надежды когда-либо обрабатывать что, поскольку только последняя команда Return может возвращать значения.
Это верно и для свободных монадов?