Haskell：之前的返回被之后的单子取消。如何？

Question

我如何理解该声明return 1 getLine？它通过了类型检查，并且看起来与1. getLine和如何return相互“抵消”？这对我来说根本没有意义。

Prelude> :t return 1
return 1 :: (Monad m, Num a) => m a

Prelude> :t return 1 getLine            -- why is it not a type error?
return 1 getLine :: Num t => t          

Prelude> return 1 getLine               
1                                       -- whatever happened to getLine?

另外，为什么最终产品是“纯”的，即使它涉及一个getLine？

Answer 1

如果你写return 1 getLine，这意味着它return 1应该是一个以参数为参数的函数getLine。

\n

我们很幸运，因为有一个带有函数[src]的实例Monad((->) r)。的确：

\n

\n

-- | @since 2.01\ninstance Applicative ((->) r) where\n    pure = const\n    (<*>) f g x = f x (g x)\n    liftA2 q f g x = q (f x) (g x)\n\n-- | @since 2.01\ninstance Monad ((->) r) where\n    f >>= k = \\ r -> k (f r) r\n

\n

\n

(->) r是 的更规范的形式r -> \xe2\x80\xa6。因此，它是一个具有作为参数类型的函数r，如果应用于a例如类型参数，则((->) r) a相当于r -> a。

\n

对于 的这个实例Monad，与具有return相同的实现。这意味着：pureconst

\n

return 1 getLine\n

\n

相当于：

\n

   const 1 getLine\n→ (\\_ -> 1) getLine\n→ 1

\n

Answer 2

我如何理解该声明return 1 getLine？

首先注意到这return 1 getLine实际上是。(return 1)getLine

这意味着这return 1是一个函数，因为它接受一个附加参数，并且函数也是一元值（这就是为什么它不是类型错误）。

因此我们必须统一

return   ::  Monad m   => a  -> m  a
return 1 :: (Monad m, Num a) => m  a
return 1 ::           Num a  => r -> a     -- Monad (r ->)

so that m a ~ r -> aand such m ~ (->) r（这是正确的书写方式(r ->)，其本身是无效的语法）。

对于函数，return = const所以我们有

return 1 getline 
= const 1 getline 
= const 1 undefined
= 1

因为const被定义为

const :: a -> b -> a
const    x    y =  x

（这就是getLine被忽略的方式）。

一般来说，函数 Monad 实例的定义是这样的

do { a <- f ; b <- foo a ; return (bar a b) } x

是相同的

let { a = f x ; b = foo a x } in bar a b  -- const (bar a b) x

return这就是被定义为 的原因const。

这意味着return和getLine不会“相互抵消” 。return这只是通过应用于第二个参数而完成的，无论它是什么，即使是undefined。

因此，正如您在问题中所写的那样，getLine属于“monad”是无关紧要的。Haskell 中的一切都是一个值，也只是另一个值。这是一个纯粹的价值；它只是描述了一个“不纯”的 I/O 操作，但它本身只是另一个值，在这里简单地用作参数。只有当出现在适当的位置（或在 main 中递归出现的其他代码中）时，它才“运行”，即它所描述的计算实际上被执行。但这里的情况并非如此。IOgetLinegetLinemain

这里发挥作用的 monad 是函数 monad，它return属于它。

至于纯度问题，单子本身并不纯或不纯。实现 Monad 的类型可以是纯类型，也可以是非纯类型。函数恰好是纯函数。

Monad 的作用是 将纯粹的与潜在不纯粹的分开。

但这实际上也是 Functor 所做的。具体来说，单子允许纯-->不纯-->纯-->不纯-->....位的混合链接，同时保持它们的分离（同样，“不纯”位实际上可以是纯的）他们自己也是如此；重要的是两个“世界”之间的分离）。