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

Поскольку 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+))
Это невозможно, потому что проблема остановки неразрешима?


haskell monads maybe fixpoint-combinators halting-problem
person Dannyu NDos    schedule 13.07.2018    source источник
comment
Вам также может понравиться Почему mfix не является полным в MaybeT, хотя этот вопрос фокусируется на (недостижимом) вызове ошибки, а не на бесконечные циклы.   -  person Daniel Wagner    schedule 13.07.2018

Ответы (1)


arrow_upward
8
arrow_downward

Один из 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. Мы можем аппроксимировать эту функцию различными способами, но в конечном итоге все они будут далеки от совершенства в этом отношении.

person Daniel Wagner    schedule 13.07.2018