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

How to view higher-order functions and IO-actions from a mathematical perspective?

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

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

现在进入肮脏的现实世界。与它的交互并不纯粹,但没有它,就没有智能程序。在我上面的简化心智模型中,将程序的纯部分和不纯部分分开意味着每个功能程序的基础是一层命令式语句,这些语句从现实世界获取数据,对其应用纯函数(do table lookup),然后将结果写回现实世界(磁盘、屏幕、网络等)。

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

从数学上讲,采用或 return 其他函数的函数完全没有问题。从集合 S 到集合 T 的函数的标准集合论定义只是:

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

  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'.

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

所以写作 S → T 只是表示一个特定的集合,因此 (A → B) → CA → (B → C) 又只是特定的集合。

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

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

一位数学家可能喜欢将 IO 动作定义为一个归纳集,类似于:

  • 如果x :: a,则pure x :: IO a
  • 如果f :: a -> b,则fmap f :: IO a -> IO b
  • 如果x :: IO af :: 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
    • (还有一个读起来有点复杂的,只是说 >>= 是关联的)

在定义程序的含义方面,这足以指定 "values" IO 类型家族可以容纳的内容。您可能会从定义自然数的标准方式中认出这种定义方式:

  • 是自然数。
  • n为自然数,则Succ(n)[​​=82=]为自然数

当然,这种定义事物的方式有些地方不是很令人满意。比如:任何特定的 IO 操作 意味着什么 ?这个定义中没有任何内容说明这一点。 (虽然请参阅 "Tackling the Awkward Squad" 以了解如何说明 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 对这种定义到底做了什么变得更加困难。

...或者您可以采用 GHC 定义,在这种情况下,如果您深入挖掘,IO a 秘密地是 a。但是,嘘!!,不要告诉那些只想转义 IO 并编写 IO a -> a 函数的没有经验的程序员,因为他们还不知道如何使用 IO 接口进行编程!

IO是一种数据结构。例如。这是 IO:

的一个非常简单的模型
data IO a = Return a | GetLine (String -> IO a) | PutStr String (IO a)

真正的IO可以看作是这样,但是有更多的构造函数(我更愿意将base中的所有IO "primitives"视为这样的构造函数)。 Haskell 程序的 main 值就是这个数据结构的一个值。运行时(从 "external" 到 Haskell)计算 main 到第一个 IO 构造函数,然后 "executes" 它以某种方式传递任何值 return ed 作为包含函数的参数返回,然后递归地执行生成的 IO 操作,在 Return () 处停止。而已。 IO 与函数没有任何奇怪的交互,它实际上不是 "impure",因为 nothing in Haskell 是不纯的(除非它不安全) .在您的程序之外只有一个实体将其解释为有效的东西。

将函数视为输入和输出表非常好。在数学中,这被称为函数的 graph,例如在集合论中,它通常首先被视为函数的定义。 return IO 动作的函数正好适合这个模型。它们只是 return 数据结构的值 IO;没什么奇怪的。例如。 putStrLn 可能是这样定义的(我不认为它实际上是,但是......):

putStrLn s = PutStr (s ++ "\n") (Return ())

readLn可能是

-- this is actually read <$> getLine; real readLn throws exceptions instead of returning bottoms
readLn = GetLine (\s -> Return (read s))

在将函数视为图形时,两者都有非常合理的解释。

你的另一个问题,关于如何解释高阶函数,不会让你走得太远。函数是值,周期。将它们建模为图形是思考它们的好方法,在这种情况下,高阶函数看起来像在输入或输出列中包含图形的图形。没有 "simplifying view" 可以将接受函数的函数或 returning 函数变成只接受值的函数,而 returns 只是值。这样的过程定义不明确,没有必要。

(注:有些人可能会试图告诉你,IO可以看作是一个函数,以"real world"为输入,输出一个新版本的世界,这可真不好考虑它的方式,部分原因是它混淆了评估和执行。这是一种使 实施 Haskell 更简单的技巧,但它使 使用 [=48] =]而且想想语言有点乱。这个数据结构模型IMO比较好处理。)

returns函数是什么函数?

你快到了:

Composing functions thus amounts to building higher-dimensional lookup tables.

这是一个小例子,在 Haskell:

infixr 2 ||

(||)           :: Bool -> (Bool -> Bool)
True  || True  =  True
True  || False =  True
False || True  =  True
False || False =  False

您的查找 table 将采用 case-expression:

的形式
x || y =  case (x, y) of (True, True)   -> True
                         (True, False)  -> True
                         (False, True)  -> True
                         (False, False) -> False

而不是使用元组:

x || y =  case x of True  -> (case y of True  -> True
                                        False -> True)

                    False -> (case y of True  -> True
                                        False -> False)

如果我们现在将参数 y 移动到新的局部函数中:

(||) x =  case x of True  -> let f y =  case y of True  -> True
                                                  False -> True
                             in f

                    False -> let g y =  case y of True  -> True
                                                  False -> False
                             in g

那么对应的map-of-maps就是:

+-------+-----------------------+
| x     | (||) x                |
+-------+-----------------------+
| True  |                       |
|       |   +-------+-------+   |
|       |   | y     | f y   |   |
|       |   +-------+-------+   |
|       |   | True  | True  |   |
|       |   +-------+-------+   |
|       |   | False | True  |   |
|       |   +-------+-------+   |
|       |                       |
+-------+-----------------------+
| False |                       |
|       |   +-------+-------+   |
|       |   | y     | g y   |   |
|       |   +-------+-------+   |
|       |   | True  | True  |   |
|       |   +-------+-------+   |
|       |   | False | False |   |
|       |   +-------+-------+   |
|       |                       |
+-------+-----------------------+

因此您的抽象模型可以扩展为 higher-order 函数 - 它们只是从某个域映射到由其他映射组成的 co-domain。


returns 一个 I/O 动作(如 Haskell 的 IO 类型)的函数是什么?

让我们回答更简单的问题:

什么是 I/O 动作(如 Haskell 的 IO 类型)[从数学角度]?

...从数学的角度?这是一个具有讽刺意味的问题,考虑到数学本身是抽象的:

In a preliminary sense, mathematics is abstract because it is studied using highly general and formal resources.

The Applicability of Mathematics (The Internet Encyclopedia of Philosophy).

...这包括从充满 I/O 设备的外部环境及其对效果的依赖中抽象出来。这使得像 Haskell 这样努力尽可能紧密地基于数学的语言陷入了困境:

  • How must interactions between a program and an external environment (consisting of, e.g., input/output-devices, file systems, ...) be described in a programming language that abstracts from the existence of an outside world?

    Claus Reinke.

  • One useful property of expressions is referential transparency. In essence this means that if we wish to find the value of an expression which contains a sub-expression, the only thing we need to know about the sub-expression is its value. Any other features of the sub-expression, such as its internal structure, the number and nature of its components, the order in which they are evaluated or the colour of the ink in which they are written, are irrelevant to the value of the main expression.

    Christopher Strachey.

    (我强调的。)

所以现在(2022 年 2 月)没有 practical 从数学角度看待 I/O 本身的方法,因为数学没有。

I/O: 是缺少的 Millennium problem...