将A => M [B]转换为M [A => B]

问题描述 投票:40回答:4

对于单声道M,是否可以将A => M[B]转换为M[A => B]

我尝试遵循这些类型均无济于事,这使我认为这是不可能的,但是我仍然想问一下。另外,在Hoogle中搜索a -> m b -> m (a -> b)也没有返回任何内容,因此我运气不高。

scala haskell types monads scalaz
4个回答
57
投票

实践中

不,至少不能以有意义的方式完成。

考虑此Haskell代码

action :: Int -> IO String
action n = print n >> getLine

首先获取n,进行打印(在此处执行IO),然后从用户那里读取一行。

假设我们有一个假设transform :: (a -> IO b) -> IO (a -> b)。然后,作为一项心理实验,请考虑:

action' :: IO (Int -> String)
action' = transform action

上面必须先做所有的IO,然后才知道n,然后返回一个纯函数。这不能等同于上面的代码。

为了强调这一点,请在下面考虑以下废话代码:

test :: IO ()
test = do f <- action'
          putStr "enter n"
          n <- readLn
          putStrLn (f n)

魔术地,action'应该预先知道用户接下来要输入什么!会话看起来像

42     (printed by action')
hello  (typed by the user when getLine runs)
enter n
42     (typed by the user when readLn runs)
hello  (printed by test)

这需要一台时间机器,因此无法完成。

理论上

不,无法完成。参数类似于the one I gave to a similar question

存在矛盾transform :: forall m a b. Monad m => (a -> m b) -> m (a -> b)。将m专用于延续monad ((_ -> r) -> r)(我省略了新类型包装器)。

transform :: forall a b r. (a -> (b -> r) -> r) -> ((a -> b) -> r) -> r

专门r=a

transform :: forall a b. (a -> (b -> a) -> a) -> ((a -> b) -> a) -> a

应用:

transform const :: forall a b. ((a -> b) -> a) -> a

通过Curry-Howard同构,以下是直觉重言式

((A -> B) -> A) -> A

但这是皮尔斯定律,这在直觉逻辑中无法得到证明。矛盾。


4
投票

其他答复很好地说明了,对于任何单子a -> m b,通常都不可能实现从m (a -> b)m的功能。但是,在某些特定的monad中,很可能实现此功能。阅读器monad就是一个例子:

data Reader r a = R { unR :: r -> a }

commute :: (a -> Reader r b) -> Reader r (a -> b)
commute f = R $ \r a -> unR (f a) r

3
投票

编号

例如,Option是单子,但是功能(A => Option[B]) => Option[A => B]没有有意义的实现:

def transform[A, B](a: A => Option[B]): Option[A => B] = ???

您放什么而不是???SomeSome接下来呢?还是None


0
投票

只需完成@svenningsson的答案。其中一个特别有用的示例是在QuickCheck中生成随机函数。此处的生成器定义为:

newtype Gen a = MkGen {
  unGen :: QCGen -> Int -> a
}

并且它具有一个Monad实例,该实例在某种意义上是Reader,但其中bind总是为所有子计算分配随机生成器。

这意味着我们可以将作用在生成器上的函数定义为函数的生成器!

promote :: (a -> Gen b) -> Gen (a -> b)
promote f = MkGen $ \gen n -> \a -> let MkGen h = f a in h gen n

并且在library中甚至更通用。

现在的问题是如何首先获得作用于生成器的函数,但这是另一个很好解释的问题here

© www.soinside.com 2019 - 2024. All rights reserved.