bod*_*ydo 164 monads haskell functional-programming
任何人都可以给出一些指针,说明为什么Haskell中的不纯计算被建模为monad？
我的意思是monad只是一个有4个操作的界面,那么建模副作用的原因是什么呢？
ken*_*ytm 286
假设一个函数有副作用.如果我们将它产生的所有效果作为输入和输出参数,那么该函数对于外部世界是纯粹的.
所以对于一个不纯的功能
f' :: Int -> Int
我们将RealWorld添加到考虑范围内
f :: Int -> RealWorld -> (Int, RealWorld)
-- input some states of the whole world,
-- modify the whole world because of the side effects,
-- then return the new world.
然后又f是纯洁的.我们定义了一个参数化数据类型IO a = RealWorld -> (a, RealWorld),因此我们不需要多次输入RealWorld
f :: Int -> IO Int
对于程序员来说,直接处理RealWorld太危险了 - 特别是如果程序员得到RealWorld类型的值,他们可能会尝试复制它,这基本上是不可能的.(想想尝试复制整个文件系统,例如.你会把它放在哪里？)因此,我们对IO的定义也包含了整个世界的状态.
如果我们不能将它们链接在一起,这些不纯的功能就毫无用处.考虑
getLine :: IO String = RealWorld -> (String, RealWorld)
getContents :: String -> IO String = String -> RealWorld -> (String, RealWorld)
putStrLn :: String -> IO () = String -> RealWorld -> ((), RealWorld)
我们想从控制台获取文件名,读取该文件,然后打印出内容.如果我们能够进入现实世界的状态,我们该怎么做？
printFile :: RealWorld -> ((), RealWorld)
printFile world0 = let (filename, world1) = getLine world0
(contents, world2) = (getContents filename) world1
in (putStrLn contents) world2 -- results in ((), world3)
我们在这里看到一个模式:函数被调用如下:
...
(<result-of-f>, worldY) = f worldX
(<result-of-g>, worldZ) = g <result-of-f> worldY
...
所以我们可以定义一个运算符~~~来绑定它们:
(~~~) :: (IO b) -> (b -> IO c) -> IO c
(~~~) :: (RealWorld -> (b, RealWorld))
-> (b -> RealWorld -> (c, RealWorld))
-> RealWorld -> (c, RealWorld)
(f ~~~ g) worldX = let (resF, worldY) = f worldX in
g resF worldY
然后我们可以简单地写
printFile = getLine ~~~ getContents ~~~ putStrLn
没有触及现实世界.
现在假设我们也希望将文件内容设为大写.大写是一种纯粹的功能
upperCase :: String -> String
但为了使它进入现实世界,它必须返回一个IO String.提升这样的功能很容易:
impureUpperCase :: String -> RealWorld -> (String, RealWorld)
impureUpperCase str world = (upperCase str, world)
这可以概括为:
impurify :: a -> IO a
impurify :: a -> RealWorld -> (a, RealWorld)
impurify a world = (a, world)
所以impureUpperCase = impurify . upperCase,我们可以写
printUpperCaseFile =
getLine ~~~ getContents ~~~ (impurify . upperCase) ~~~ putStrLn
(注意:通常我们写getLine ~~~ getContents ~~~ (putStrLn . upperCase))
现在让我们看看我们做了什么:
(~~~) :: IO b -> (b -> IO c) -> IO c将两个不纯函数链接在一起的运算符impurify :: a -> IO a将纯值转换为不纯的函数.现在我们做的鉴定(>>=) = (~~~)和return = impurify,并看到了吗？我们有一个monad.
(要检查它是否真的是一个单子,应该满足几个公理:
(1) return a >>= f = f a
impurify a = (\world -> (a, world))
(impurify a ~~~ f) worldX = let (resF, worldY) = (\world -> (a, world)) worldX
in f resF worldY
= let (resF, worldY) = (a, worldX))
in f resF worldY
= f a worldX
(2) f >>= return = f
(f ~~~ impurify) a worldX = let (resF, worldY) = impuify a worldX
in f resF worldY
= let (resF, worldY) = (a, worldX)
in f resF worldY
= f a worldX
(3) f >>= (\x -> g x >>= h) = (f >>= g) >>= h
行使.)
Con*_*nal 43
任何人都可以给出一些指针,说明为什么Haskell中的无法计算被建模为monad？
这个问题包含了广泛的误解.杂质和Monad是独立的概念.杂质不是由Monad建模的.相反,有一些数据类型,例如IO代表命令式计算.对于其中一些类型,其界面的一小部分对应于称为"Monad"的界面模式.此外,没有已知的纯/功能/外延的解释IO(并且不太可能有一个,考虑到"sin bin"的目的IO),尽管有一个常见的故事是关于World -> (a, World)它的含义IO a.这个故事不能如实描述IO,因为它IO支持并发性和非确定性.当确定性计算允许中间计算与世界交互时,这个故事甚至都不起作用.
有关更多说明,请参阅此答案.
编辑:在重新阅读问题时,我认为我的答案并未完全按计划进行.正如问题所说,命令式计算的模型经常变成monad.提问者可能不会真正假设monadness以任何方式启用命令式计算的建模.
Pau*_*son 13
据我了解,有人称Eugenio Moggi首先注意到一个名为"monad"的先前模糊的数学结构可用于模拟计算机语言中的副作用,因此使用Lambda演算来指定它们的语义.当Haskell被开发出来时,有各种方式对不纯的计算进行建模(有关详细信息,请参阅Simon Peyton Jones的"头发衬衫"论文),但当Phil Wadler介绍monad时,很快就会发现这是答案.剩下的就是历史.
任何人都可以给出一些指针,说明为什么Haskell中的无法计算被建模为monad？
好吧,因为Haskell是纯粹的.你需要一个数学概念区别开来unpure计算和纯净的人的类型,级别和模型PROGRAMM流量分别.
这意味着你必须得到一些IO a模拟不合理计算的类型.然后你需要知道组合这些计算的方法,这些计算适用于sequence(>>=)和提升值(return)是最明显和最基本的.
有了这两个,你已经定义了一个monad(甚至没有想到它);)
此外,单子提供非常笼统,抽象厉害,这么多种类的控制流可以方便地推广在一元函数一样sequence,liftM或特殊的语法,使得unpureness没有这样一个特例.
有关更多信息,请参阅函数式编程和唯一性类型中的monads(我知道的唯一替代方法).
如你所说,Monad是一个非常简单的结构.答案的一半是:Monad是我们可能给副作用函数提供的最简单的结构,并且能够使用它们.随着Monad我们可以做两件事情:我们可以把一个纯粹的价值作为一个副作用的值(return),我们可以应用副作用的功能,一个副作用的价值得到新的副作用的值(>>=).失去做这些事情的能力将是瘫痪,所以我们的副作用类型需要"至少" Monad,并且事实证明Monad足以实现我们迄今为止所需的一切.
另一半是:我们可以给"可能的副作用"最详细的结构是什么？我们当然可以将所有可能的副作用空间视为一组(唯一需要的是会员资格).我们可以通过一个接一个地做两个副作用来组合,这会产生不同的副作用(或者可能是同一个 - 如果第一个是"关闭计算机"而第二个是"写文件",那么结果编写这些只是"关机计算机").
好的,那么我们能说些什么呢？它是联想的; 也就是说,如果我们结合三个副作用,我们在哪个顺序组合就没关系.如果我们这样做(写文件然后读取套接字)然后关闭计算机,那就像写文件那样(读取套接字然后关闭)电脑).但它不是可交换的:("写文件"然后"删除文件")是一种不同的副作用("删除文件",然后是"写文件").我们有一个身份:特殊的副作用"无副作用"有效("无副作用",然后"删除文件"与"删除文件"的副作用相同)此时任何数学家都在想"群组!" 但群体反转,一般情况下无法反转副作用; "删除文件"是不可逆转的.所以我们留下的结构是一个monoid,这意味着我们的副作用函数应该是monad.
是否有更复杂的结构？当然!我们可以将可能的副作用分为基于文件系统的效果,基于网络的效果等等,我们可以提出更精细的构图规则来保留这些细节.但它又归结为:Monad非常简单,但足以表达我们关心的大部分属性.(特别是,关联性和其他公理让我们以小块的形式测试我们的应用,确信组合应用的副作用将与片的副作用的组合相同).