如何从数学角度查看高阶函数和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 和两个条件成立:

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 ::字符串->IO()
• forkIO :: IO a->IO ThreadId
• ...以及其他一千种基本情况.
• 我们在一些平等上取商:
  • fmap id = id
  • fmap f.fmap g = fmap(f .g)
  • 纯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 并写一个 IO a->函数，因为他们还不了解如何使用 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屋！