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

ssgvzors 于 2023-10-19 发布在其他

关注(0)|答案(1)|浏览(134)

{-# 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

haskell

来源：https://stackoverflow.com/questions/76905950/anything-wrong-with-this-simpler-bind-for-cont

1条答案

按热度按时间

c3frrgcw1#

修改后的定义工作正常（除了我不知道如何让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)

相比之下，你的二阶连续单子：

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'`

就这样
由于这种同构，对于某些a0 :: a，arr总是等于截面($ a0)，对于某些f :: a -> b，aCbrr总是等于\a' -> C ($ f a')，这意味着>>=的原始定义如下：

(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)

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

赞(0）回复(0）举报 2023-10-19

我来回答

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

1条答案

相关问题

热门标签

最新问答