这个更简单的 Cont 绑定有什么问题吗？

Question

{-# LANGUAGE RankNTypes #-}

newtype C a = C {runCont :: forall r. (a -> r) -> r} 

instance Functor C where  
  fmap f (C arr) = C $ \br -> arr $ br . f

instance Applicative C where
  pure a = C ($ a)
  (C abrr) <*> (C arr) = C $ \brr -> abrr ( \ab -> arr ( brr . ab ) )

instance Monad C where 
  -- (C arr) >>= aCbrr = C $ \br -> arr (\a -> runCont (aCbrr a) br) -- The usual
  (C arr) >>= aCbrr = arr aCbrr -- My simpler idea with the same result in this test

main :: IO ()
main = print $ flip runCont id $ do
  x <- pure (5::Int)
  y <- pure $ 2 * x
  z <- pure $ take y $ repeat 'a'
  pure z

根据Noughtmare的建议添加一些法律证明。我认为它们直观上是有意义的，但注释的步骤可能不太正式：

Left identity: pure a >>= h === h a

pure a >>= h
C (\k -> k a) >>= h
(\k -> k a) h
h a

Right identity: m >>= pure === m

m >>= pure
C arr >>= pure
arr pure
arr ( \a -> C (\k -> k a) )
C ( \k -> k (arr id) ) -- because arr knows nothing about r
C arr -- because arr::(a->r)->r so k::a->r
m

Associativity: 

(m >>= f) >>= g         ===    m >>= (\x -> f x >>= g)
((C arr) >>= f) >>= g   ===    (C arr) >>= (\x -> f x >>= g)
(arr f) >>= g          
f (arr id) >>= g
(pure.h) (arr id) >>= g ===    (C arr) >>= (\x -> (pure.h) x >>= g)
C (h (arr id)) >>= g    ===    arr ( \x -> (C (h x)) >>= g )
                        ===    C (h (arr id)) >>= g

Answer 1

您修改后的定义工作正常（除了我不知道您如何进行

flip runCont

进行类型检查 - 我认为您需要手动翻转参数）。然而，我也认为你会发现你的延续单子不是很有用。

通常的延续单子是 1 级类型：

newtype C' r a = C' { runCont' :: (a -> r) -> r }

并且它很有用，因为

C' r a

与

a

值“几乎同构”，除了类型

r

是已知的。这意味着您可以构造

C' Int Char

类型的一元值，表示纯

Char

:

C' (\f -> f 'A')   -- same as `pure 'A'`

但是你也可以构造一个相同类型的一元值C' Int Char

，用一个

Int

返回值来缩短计算：

C' (\f -> 42) 相比之下，你的 2 级延续单子：

newtype C a = C { runCont :: forall r. (a -> r) -> r }

与 a 类型同构。同构的一个方向由

pure

给出，另一个方向由：

 给出

unpure :: C a -> a
unpure (C f) = f id

所以，用你的

C Char

，你可以代表一个纯粹的

Char

:C (\f -> f 'A') -- equivalent to `pure 'A'`

就是这样。

由于这种同构，对于某些

arr

，您的

($ a0)

始终等于部分

a0 :: a

，对于某些

aCbrr

，您的

\a' -> C ($ f a')

始终等于

f :: a -> b

，这意味着原始定义

>>=

给出：

(C arr) >>= aCbrr 
-- by original definition of `>>=`
= C $ \br -> arr (\a -> runCont (aCbrr a) br)
-- by the above equivalencies
= C $ \br -> ($ a0) (\a -> runCont ((\a' -> C ($ f a')) a) br)
-- and simplify
= C $ \br -> ($ a0) (\a -> runCont (C ($ f a)) br)
= C $ \br -> (\a -> runCont (C ($ f a)) br) a0
= C $ \br -> runCont (C ($ f a0)) br
= C $ \br -> ($ f a0) br
= C ($ f a0)

而您对 

>>=

的修改定义给出了

(C arr) >>= aCbrr
-- by your definition of `>>=`
= arr aCbrr
-- by the above equivalencies
= ($ a0) (\a' -> C ($ f a'))
-- and simplify
= (\a' -> C ($ f a')) a0
= C ($ f a0)

所以这两个定义是等价的。