Является ли mfix для "Возможно, невозможно быть нетривиальным"?

Question

Поскольку Nothing >>= f = Nothing для каждого fследующее тривиальное определение подходит для mfix:

mfix _ = Nothing

Но это не имеет практического применения, поэтому у нас есть следующее нетитальное определение:

mfix f = let a = f (unJust a) in a where
    unJust (Just x) = x
    unJust Nothing = errorWithoutStackTrace "mfix Maybe: Nothing" 

Было бы хорошо, если mfix f возвращенный Nothing если это let-Клауз не остановится. (Например, f = Just . (1+))
Разве это невозможно, потому что проблема остановки неразрешима?

Answer 1

Один из MonadFix Законы говорят, что монадическая точка фиксации должна совпадать с чистой точкой фиксации, когда монадическое действие чисто:

mfix (return . f) = return (fix f)

Из-за этого требуется следующее:

mfix (Just . (1+)) = mfix (return . (1+))
                   = return (fix (1+))
                   = Just (fix (1+))

А также fix (1+) действительно дно. Таким образом, для вашей предложенной функции, законы точно определяют, как mfix должен вести себя (и он ведет себя так).

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

mfix' (Just . (1+)) = Nothing
mfix' (Just . const 1) = Just 1

Это невозможно осуществить именно по той причине, о которой вы говорите: проблема остановки говорит нам, что невозможно точно знать, fix f будет зацикливаться или заканчиваться произвольно f, Мы можем аппроксимировать эту функцию различными способами, но в конечном итоге все в этом отношении не будут доведены до совершенства.