如何从数学角度看待高阶函数和 IO 动作? [英] How to view higher-order functions and IO-actions from a mathematical perspective?

问题描述

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

I am trying to understand functional programming from first principles, yet I am stuck on the interface between the pure functional world and the impure real world that has state and side effects. From a mathematical perspective,

• 什么是返回函数的函数?
• 什么是返回 IO 操作的函数(如 Haskell 的 IO 类型)?

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

To elaborate: In my understanding, a pure function is a map from domain to co-domain. Ultimately, it is a map from some values in computer memory to some other values in memory. In a functional language, functions are defined declaratively; i.e., they describe the mapping but not the actual computation that needs to be performed on a specific input value; the latter is up to the compiler to derive. In a simplified setting with memory to spare, there would be no computation at runtime; instead, the compiler could create a lookup table for each function already at compile time. Executing a pure program would amount to table lookup. Composing functions thus amounts to building higher-dimensional lookup tables. Of course, the entire point in having computers is to devise ways to specify functions without the need for point-wise table lookup - but I find the mental model helpful to distinguish between pure functions and effects. However, I have difficulty adapting this mental model for higher-order functions:

• 对于将另一个函数作为参数的函数，将值映射到值的结果一阶函数是什么?是否有它的数学描述(我确定有，但我既不是数学家也不是计算机科学家).
• 返回函数的函数怎么样?我如何才能在心理上扁平化"这个构造以再次获得将值映射到值的一阶函数?

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

Now to the nasty real world. Interaction with it is not pure, yet without it, there are no sensible programs. In my simplified mental model above, separating pure and impure parts of a program means that the basis of each functional program is a layer of imperative statements that get data from the real world, apply a pure function to it (do table lookup), and then write the result back to the real world (to disk, to the screen, the network, etc.).

在 Haskell 中，这种与现实世界的命令式交互被抽象为 IO 操作，编译器根据它们的数据依赖性进行排序.但是，我们不会直接将程序编写为一系列命令式 IO 操作.相反，有些函数会返回 IO 操作(::IO a 类型的函数).但据我所知，这些不可能是真正的功能.这些是什么?如何根据上述心理模型来最好地思考它们?

In Haskell, this imperative interaction with the real world is abstracted as IO actions, which the compiler sequences according to their data dependency. However, we do not write a program directly as a sequence of imperative IO actions. Instead, there are functions that return IO actions (functions of type :: IO a). But to my understanding, these cannot be real functions. What are they? How to best think about them in terms of the mental model outlined above?

推荐答案

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

Mathematically, there's no problem at all with functions that take or return other functions. The standard set-theory definition of a function from set S to set T is just:

f ∈ S → T 表示 f ⊂ S ✕ T 和两个条件成立:

f ∈ S → T means that f ⊂ S ✕ T and two conditions hold:

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

1. If s ∈ S, then (s, t) ∈ f for some t, and
2. if both (s, t) ∈ f and (s, t') ∈ f, then t = t'.

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

We write f(s) = t as a convenient notational shorthand for (s, t) ∈ f.

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

So writing S → T just denotes a specific set, and therefore (A → B) → C and A → (B → C) are again just specific sets.

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

Of course, for efficiency, we do not represent functions internally in memory as the set of input-output pairs like this, but this is a decent first approximation that you can use if you want a mathematical intuition. (The second approximation takes a lot more work to set up properly, because it uses structures you probably haven't already experienced very much to deal with laziness and recursion in a careful, principled way.)

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

IO actions are a bit trickier. How you want to think of them may depend a bit on your particular mathematical bent.

数学家的一种劝说可能想将 IO 动作定义为归纳集，例如:

One persuasion of mathematician might like to define IO actions as an inductive set, something like:

• 如果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 线程 ID
• ...以及其他一千个基本案例.
• 我们对几个等式进行商数:
  • fmap id = id
  • fmap f .fmap g = fmap (f . g)
  • pure x >>= f = f x
  • x >>= pure .f = fmap f x
  • (还有一个稍微有点复杂，只是说 >>= 是关联的)
  • If x :: a, then pure x :: IO a.
  • If f :: a -> b, then fmap f :: IO a -> IO b.
  • If x :: IO a and f :: a -> IO b, then x >>= f :: IO b.
  • putStrLn :: String -> IO ()
  • forkIO :: IO a -> IO ThreadId
  • ...and a thousand other base cases.
  • We quotient over a few equalities:
    • fmap id = id
    • fmap f . fmap g = fmap (f . g)
    • pure x >>= f = f x
    • x >>= pure . f = fmap f x
    • (and a slightly complicated-to-read one that just says that >>= is associative)

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

    In terms of defining the meaning of a program, that's enough to specify what "values" the IO family of types can hold. You might recognize this style of definition from the standard way of defining natural numbers:

    • 零是一个自然数.
    • 如果 n 是自然数，则 Succ(n) 是自然数.
    • Zero is a natural number.
    • If n is a natural number, then Succ(n) is a natural number.

    当然，这种定义事物的方式也有一些不太令人满意的地方.比如:任何特定的 IO 操作意味着是什么?这个定义中没有任何说明.(尽管请参阅解决尴尬的小队"以阐明即使您采用这种类型的归纳定义，您也可以说出 IO 操作的含义.)

    Of course, there are some things about this way of defining things that aren't super satisfying. Like: what does any particular IO action mean? Nothing in this definition says anything about that. (Though see "Tackling the Awkward Squad" for an elucidation of how you could say what an IO action means even if you take this kind of inductive definition of the type.)

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

    Another kind of mathematician might like this kind of definition better:

    IO 操作同构于代表宇宙当前状态的幻象令牌上的有状态函数:

    An IO action is isomorphic to a stateful function on a phantom token representing the current state of the universe:

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

    这种定义也有其吸引力；但是，值得注意的是，要说明 forkIO 对这种定义做了什么要困难得多.

    There are attractions to this kind of definition, too; though, notably, it gets a lot harder to say what the heck forkIO does with that kind of definition.

    ...或者您可以采用 GHC 定义，在这种情况下，IO a 秘密地是 a，如果您在封面下挖掘得足够多.但是，嘘！！，不要告诉那些只想逃避IO并写一个IOa->的没有经验的程序员.一个函数，因为他们还不了解如何使用IO接口编程！

    ...or you could take the GHC definition, in which case an IO a is secretly an a if you dig under the covers enough. But, shhh!!, don't tell the inexperienced programmers who just want to escape IO and write an IO a -> a function because they don't understand how to program using the IO interface yet!

    这篇关于如何从数学角度看待高阶函数和 IO 动作?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！