haskell 为什么IO不是State的示例化?

hi3rlvi2  于 2023-03-08  发布在  其他
关注(0)|答案(2)|浏览(187)

当我们有RealWorld时,为什么IO不是(严格的)State单子的示例化,就像Control.Monad.ST中提供的那样?我认为RealWorld应该是一个表示现实本身的魔法类型。
我的意思是,回想一下State单子的“run”函数:

runState :: (s -> (a, s)) -> s -> a

将其示例化为RealWorld,我们得到:

runIO :: (RealWorld -> (a, RealWorld)) -> RealWorld -> a

由于我们无法构造RealWorld * 的值 *,因此这不应该像unsafePerformIO那样充当后门。
原因是因为这种解释会启用定义为StateT RealWorld的单子转换器IOT吗?

watbbzwu

watbbzwu1#

1.暴露IO中的RealWorld仍然会给你getUnsafePerformIO :: IO (IO a -> a),这和unsafePerformIO一样糟糕。

  1. IO使用未提升的类型(RealWorld#(#,#))来避免不必要的分配,因此无论如何它并不完全匹配State
    1.它确实与ST匹配,但是IO的直接定义可以在您查看Core或需要做一些低级黑客时将噪音降到最低(这比使用ST(也涉及IO)要常见得多)。
    1.我认为RealWorld应该是一个代表现实本身的魔法类型。
    RealWorld是一个可爱的名字,但主要是混淆的来源。它实际上不代表任何东西。最好忘记RealWorld的含义,只从操作语义的Angular 考虑IO的定义。
vof42yt1

vof42yt12#

IO的目的是在Haskell值的纯宇宙中仔细地定义一个模型,这样你可以用这个模型做的每一件事都与真实的宇宙的实际行为相匹配,然后我们可以将模型中的特定API与真实世界的观察和效果挂钩。
如果IO仅仅是type IO a = State RealWorld,它就不会做这样的工作,即使我们不能构造RealWorld,我们仍然可以用这个接口做一些对真实的宇宙的行为没有任何意义的事情。

main = do
  backup <- get
  fireMissiles
  tears <- checkForRegrets
  if tears
    then put backup
    else pure ()

因此,Haskell的纯IO模型的一个关键部分是IO类型是 abstract,它没有直接可见的属性,* 除了 * 它实现了Monad类和提供的原语操作。
你当然可以在心里将IO建模为“它就像一个状态单子,其中被线程化的状态代表了整个宇宙”,在这种理解下,组合IO操作就是安排“宇宙”以正确的顺序被线程化。
许多 haskell 人(包括我自己)更喜欢IO a是对不纯行为的纯描述的心理模型;类似于“一个声称运行它将产生a的程序“。基于这种理解,组合IO操作是将后面的程序作为延续运行与前面的程序产生的结果挂钩。
但这两个模型都不是IO在引擎盖下“真正工作”的方式。IO "像“这两个东西,但主要是因为一个未知抽象单子的API像这两个东西,并且“它是一个单子”实际上是IO的公共API所具有的唯一声明性信息。你可以用任何一种对你最有帮助的方式来思考它(我有一个得意的理论,即来自“传统”命令式编程的人发现状态单子类比更容易,并且对延续传递风格感到舒服的人发现“动作的描述”更有吸引力)。但是不管您怎么想,类型检查器和模块系统都将强制执行真正重要的属性(除非您特意导入和使用不安全的东西)。
IO实现中有一些看起来像是世界传递的东西;这就是您注意到的RealWorld类型的使用位置,它本质上是一种实现技术,有助于确保编译器不会意外地决定重新排序IO操作;它的工作原理是使所需的操作顺序出现(对编译器来说)有一个需要这种顺序的数据依赖。但是如果你有权访问那个级别,你就 * 不 * 限于编写实际上与真实的世界中IO操作行为方式相对应的合理代码,所以这个世界通行证不是IO公共API的一部分。s作为实现细节并不意味着您必须或者甚至应该将IO视为状态单子,就像你需要把MapSet看作一棵树一样。
一些其他的语言(我知道的是Clean和Mercury)确实更明确地使用了世界传递,并且实际上提供了对世界令牌的直接访问。要做到这一点并保持这样的属性,即你在IO的纯模型中所能做的任何事情实际上都对应于我们在单一真实的宇宙中所能做的事情,需要一种不同的限制。Clean和Mercury使用唯一性类型;本质上,给定的World有一个类型级标记,确保它必须被使用 * 恰好 * 一次(注意,在Clean和Mercury中,世界标记 * 本身 * 仍然是完全抽象的;world token的 existence 是API的一部分,但是除了将它们传递给下一个IO操作之外,您仍然无法查看它们的内部或对它们做任何事情)。这防止了我之前写的那种“备份宇宙”的废话。如果Haskell真的想用world传递来建模IO,它可以,但它还需要使用诸如唯一性类型之类的东西。所以它仍然不能使用普通的State单子。

相关问题