时间戳

首页 > 解决方案 > 如何从数学角度看待高阶函数和 IO 动作？

haskell - 如何从数学角度看待高阶函数和 IO 动作？

问题描述

我试图从第一原理理解函数式编程，但我被困在纯函数世界和具有状态和副作用的不纯现实世界之间的接口上。从数学的角度来看，

详细说明：在我的理解中，纯函数是从域到共域的映射。最终，它是从计算机内存中的某些值到内存中的某些其他值的映射。在函数式语言中，函数是声明式定义的；即，它们描述了映射，而不是需要对特定输入值执行的实际计算；后者由编译器派生。在具有备用内存的简化设置中，运行时不会进行计算；相反，编译器可以在编译时为每个函数创建一个查找表。执行纯程序相当于查表。因此，组合函数相当于构建更高维的查找表。当然，拥有计算机的全部意义在于设计方法来指定函数，而无需逐点查找表——但我发现心智模型有助于区分纯函数和效果。但是，我很难将这种心智模型用于高阶函数：

现在进入令人讨厌的现实世界。与它的交互并不纯粹，但没有它，就没有明智的程序。在我上面的简化心智模型中，分离程序的纯部分和不纯部分意味着每个函数式程序的基础是一层命令式语句，这些语句从现实世界中获取数据，对其应用纯函数（进行表查找），以及然后将结果写回现实世界（磁盘、屏幕、网络等）。

在 Haskell 中，这种与现实世界的命令式交互被抽象为IO 动作，编译器根据它们的数据依赖性对其进行排序。但是，我们不会将程序直接编写为命令式 IO 操作的序列。相反，有些函数会返回 IO 操作（类型为 的函数:: IO a）。但据我了解，这些不可能是真正的功能。这些是什么？如何根据上述心智模型最好地思考它们？

标签： haskellfunctional-programmingiohigher-order-functionspurely-functional

解决方案

从数学上讲，接受或返回其他函数的函数完全没有问题。从集合S到集合T的函数的标准集合论定义是：

f ∈ S → T意味着f ⊂ S ✕ T和两个条件成立：

  1. 如果s ∈ S，那么(s, t) ∈ f对于某个t，并且
  2. 如果(s, t) ∈ f和(s, t') ∈ f，则t = t'。

我们将f(s) = t写成(s, t) ∈ f 的一种方便的符号简写。

所以写S → T只是表示一个特定的集合，因此(A → B) → C和A → (B → C)再次只是特定的集合。

当然，为了提高效率，我们不会将内存中的函数内部表示为这样的输入-输出对集合，但这是一个不错的第一个近似值，如果您想要数学直觉，可以使用它。（第二个近似值需要做更多的工作才能正确设置，因为它使用您可能还没有体验过的结构以谨慎、有原则的方式处理惰性和递归。）

IO 操作有点棘手。您如何看待它们可能在某种程度上取决于您特定的数学倾向。

一位数学家可能希望将 IO 动作定义为归纳集，例如：

  • 如果x :: a，那么pure x :: IO a。
  • 如果f :: a -> b，那么fmap f :: IO a -> IO b。
  • 如果x :: IO a和f :: a -> IO b，那么x >>= f :: IO b。
  • putStrLn :: String -> IO ()
  • forkIO :: IO a -> IO ThreadId
  • ...以及一千个其他基本案例。
  • 我们对几个等式进行商：
    • fmap id = id
    • fmap f . fmap g = fmap (f . g)
    • pure x >>= f=f x
    • x >>= pure . f=fmap f x
    • （还有一个读起来有点复杂的，只是说它>>=是联想的）

就定义程序的含义而言，这足以指定 IO 系列类型可以容纳的“值”。您可能会从定义自然数的标准方式中认出这种定义方式：

  • 零是一个自然数。
  • 如果n是自然数，则Succ(n)是自然数。

当然，这种定义事物的方式有一些事情不是很令人满意。比如：任何特定的 IO 操作是什么意思？这个定义中没有任何内容说明这一点。（尽管请参阅“处理尴尬的小队”以阐明即使您采用这种类型的归纳定义，您如何说出 IO 操作的含义。）

另一种数学家可能更喜欢这种定义：

一个 IO 动作同构于代表宇宙当前状态的幻象标记上的有状态函数：

IO a ~= RealWorld -> (RealWorld, a)

这种定义也很有吸引力。但是，值得注意的是，要说出这种定义到底forkIO做了什么变得更加困难。

...或者您可以采用 GHC 定义，在这种情况下，如果您足够深入地了解，则 anIO a是秘密的。a但是，嘘！！，不要告诉没有经验的程序员，因为他们还不了解如何使用接口进行编程，所以他们只是想逃避IO并编写一个函数！IO a -> aIO

推荐阅读