Проблема с уравнением для тика в Wadler, «Монады для функционального программирования», раздел 3 - PullRequest
Новая
       55

Проблема с уравнением для тика в Wadler, «Монады для функционального программирования», раздел 3

1 голос
/ 06 февраля 2020

В Wadler's Монады для функционального программирования Я смотрю на уравнение

галочка ✭ λ (). m = m ✭ λ (). галочка

в разделе 3 (в контексте государственной монады). Утверждается, что он

сохраняется до тех пор, пока тик является единственным действием над состоянием в пределах m .

I не понимаю, как это может быть. Разве левый термин не имеет типа m , в то время как правый термин имеет тип tick : M ()? Более того, если тип m не M (), типы операндов ✭ не совпадают с правой стороны.

Я посмотрел вокруг, но не смог найти никаких ошибок, и то же самое уравнение появляется в пересмотренной версии документа от 2001 года, так что должно быть что-то, что я упускаю…

1 Ответ

2 голосов
/ 06 февраля 2020

Синтаксис Haskell, 

tick x  =  ((), x+1)
unitState a x  =  (a, x)
bindState m k  =  uncurry k . m    -- StarOp for State

bindState tick (\() -> m) =
     = uncurry (\() -> m) . (\x -> ((), x+1))
     = (\y -> uncurry (\() -> m) ( (\x -> ((), x+1)) y))
     = (\y -> uncurry (\() -> m)          ((), y+1)    )
     = (\y ->         (\() -> m)           () (y+1)    )
     = (\y ->                 m               (y+1)    )

bindState m (\() -> tick) =
     = uncurry (\() -> tick) . m
     = uncurry (\() -> (\x -> ((), x+1))) . m
     = uncurry (\() x -> ((), x+1)) . m
     = (\y -> uncurry (\() x -> ((), x+1)) (m y))
     = (\y -> let ((),z) = m y in ((), z+1))

Эти два значения будут одинаковыми, только если m y возвращает ((),z), так что m (y+1) возвращает ((),z+1) (т.е. m y добавляет только некоторые фиксированная сумма до начального состояния y, которая не зависит от y).

Так что я не вижу проблемы с типами, но это Engli sh Значение фразы также ускользает от меня.

Кстати, предложенный в статье способ добавления "количества выполнений" к своему монадическому c оценщику путем замены этого unitState на unitState a x = (a, x+1), по сути, сделает его недопустимым монада, потому что этот новый unitState не будет тождеством.

Типы: 

tick :: M ()
bindState :: M a -> (a -> M b) -> M b
(\() -> tick) :: () -> M () 

bindState (tick :: M ()) ((\() -> m) :: () -> M b ) :: M b
bindState (m :: M ()) ((\() -> tick) :: () -> M ()) :: M ()

Так что единственное, что с типами это то, что m должно быть m :: M () не общее M b, как мы уже видели с расширениями выше.

...