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

Question

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

• 什么是返回函数的函数？
• 什么是返回 IO 操作的函数（如 Haskell 的 IO 类型）？

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

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

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

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

Answer 1

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

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

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

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

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

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

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 定义，在这种情况下，IO a 秘密地是 a，如果您深入挖掘的话。但是，嘘！！，不要告诉那些只是想逃避IO并写一个IO a -> a函数的没有经验的程序员，因为他们还不了解如何使用IO接口进行编程！

Answer 2

IO 是一个数据结构。例如。这是IO的一个非常简单的模型：

data IO a = Return a | GetLine (String -> IO a) | PutStr String (IO a)

真正的IO 可以看作是this，但具有更多构造函数（我更愿意将base 中的所有IO“原语”视为此类构造函数）。 Haskell 程序的main 值就是这个数据结构的一个值。运行时（它是 Haskell 的“外部”）将 main 评估为第一个 IO 构造函数，然后以某种方式“执行”它，将返回的任何值作为参数传递回包含的函数，然后执行生成的 IO递归操作，停在Return ()。而已。 IO 与函数没有任何奇怪的交互，它实际上并不是“不纯的”，因为 Haskell 中的 nothing 是不纯的（除非它不安全）。在你的程序之外只有一个实体将它解释为有效的东西。

将函数视为输入和输出表是非常好的。在数学中，这被称为函数的 graph，例如在集合论中，它通常首先被视为函数的定义。返回IO 动作的函数非常适合这个模型。它们只是返回数据结构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))

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

你的另一个问题，关于如何解释高阶函数，不会让你走得太远。函数是值，周期。将它们建模为图形是一种思考它们的好方法，在这种情况下，高阶函数看起来就像在其输入或输出列中包含图形的图形。没有“简化视图”可以将接受函数或返回函数的函数转换为只接受值并只返回值的函数。这样的过程没有明确定义，也没有必要。

(注意：有些人可能会告诉你IO可以看作是一个以“现实世界”为输入并输出新版本世界的函数。这真的不是一个好的思考方式, 部分是因为它将评估和执行混为一谈。这是一种使 实现 Haskell 更简单的 hack，但它使 使用 和思考该语言有点混乱。这些数据结构模型更容易处理。）

Answer 3

什么是返回函数的函数？

你快到了：

因此，组合函数相当于构建更高维的查找表。

这是一个小例子，在 Haskell 中：

infixr 2 ||

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

然后您的查找表将采用 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 |   |
|       |   +-------+-------+   |
|       |                       |
+-------+-----------------------+

因此，您的抽象模型可以扩展到高阶函数 - 它们只是从某个域映射到由其他映射组成的共同域。

---

什么是返回 I/O 动作的函数（如 Haskell 的 IO 类型）？

这是一个有趣的事实：部分应用的函数类型：

forall a . (->) a

是一元的：

unit     :: a -> (d -> a)
unit x   =  \ u -> x

bind     :: (d -> a) -> (a -> (d -> b)) -> (d -> b)
bind m k =  \ u -> let x = m u in k x u

instance Monad ((->) a) where
    return = unit
    (>>=)  = bind

这多么简单！要是IO 类型能这么容易定义就好了……

当然不可能完全相同 - 涉及外部交互 - 但我们能接近多远？

好吧，I/O 通常需要以某种预定义的顺序发生才能发挥作用（例如，抓住房子钥匙然后离开锁定的房子），因此需要一种机制来按顺序对 @ 的评估进行排序987654337@ 表达式 - bang patterns 怎么样？

unit     :: a -> (d -> a)
unit x   =  \ u -> x

bind     :: (d -> a) -> (a -> (d -> b)) -> (d -> b)
bind m k =  \ u -> let !x = m u in k x u

几乎不引人注意 - 很好！作为奖励，我们现在还可以为(>>) 提供一个有用的定义：

next     :: (d -> a) -> (d -> b) -> (d -> b)
next m w =  \ u -> let !_ = m u in w u

instance Monad ((->) a) where
       .
       .
       .
    (>>)   = next

让我们考虑以下小型 Haskell 2010 程序：

main :: IO ()
main =  putStr "ha" >> putStr "ha" >> putStr "!\n"

这可以改写为：

main = let x = putStr "ha" in x >> x >> putStr "!\n"

假设适当的定义：

puts :: String -> (d -> ())
putc :: Char -> (d -> ())

我们也可以重写吗：

main' :: d -> ()
main' =  puts "ha" >> puts "ha" >> puts "!\n"

作为：

main' = let x = puts "ha" in x >> x >> puts "!\n"

否 - 引用 Philip Wadler 的 How to Declare an Imperative：

[...] 笑点在我们身上：程序只打印一个 "ha"，此时变量 x 被绑定。在存在副作用的情况下，最简单形式的equational reasoning 将失效。

（第 5 页第 2.2 节。）

为什么？让我们看看发生了什么变化：

let x = puts "ha" in x >> x

如果(>>) 被替换为它的定义：

let x = puts "ha" in \ u -> let !_ = x u in x u

原因已揭示 - 虽然 x u 被使用了两次，但它只被评估一次，因为 Haskell 是 nonstrict - 第二次使用 x u 只是检索第一个结果。

这是一个合法的转换，例如：

testme n = n^2 + n^2 + n

和：

testme n = let x = n^2 in x + x + n

和优化像 GHC 这样的 Haskell 实现依赖于它和许多其他转换来完成他们的目标 - 将 I/O 视为一些特殊情况很可能是完全徒劳的练习......让我们修改代码让它赢'最终不会被重写。

一种简单的方法是让所有对puts 或putc 的调用都是唯一的，基于F. Warren Burton 在Nondeterminism with Referential Transparency in Functional Programming Languages 中描述的技术：

let x = puts "ha" in \ u -> let !u1:u2:_ = ... in
                            let !_ = x u1 in x u2

因此：

bind     :: (d -> a) -> (a -> (d -> b)) -> (d -> b)
bind m k =  \ u -> let !u1:u2:_ = ... in
                   let !x       = m u1 in
                   k x u2

next     :: (d -> a) -> (d -> b) -> (d -> b)
next m w =  \ u -> let !u1:u2:_ = ... in
                   let !_       = m u1 in
                   w u2

但是，这还不够：

let x = puts "ha" in \ u -> let !u1:u2:_ = ... in
                            let !_ = x u1 in x u

我们可以从 Clean 获得提示并添加唯一性类型，但已经进行了一项重大更改（爆炸模式扩展） - 我们真的要添加另一个扩展吗什么时候遇到新问题？

我们不妨做一个completely-new programming language...

继续，让我们重命名所有烦人的d 类型变量，以及puts 和putc：

data OI
putstr   :: String -> OI -> ()
putchar  :: Char -> OI -> ()

嗯...所有输出，没有输入：

getchar  :: OI -> Char

其他定义呢？让我们试试吧：

next     :: (OI -> a) -> (IO -> b) -> OI -> b
next m w =  \ u -> let !u1:u2:_ = ... in
                   let !_       = m u1 in
                   w u2

所以u、u1和u2具有相同的类型；它们是相关的：

next     :: (OI -> a) -> (IO -> b) -> OI -> b
next m w =  \ u -> let !u1:u2:_ = parts u in
                   let !_       = m u1 in
                   w u2

像parts 这样的名字相当通用：

class Partible a where
    parts :: a -> [a]

partsOI :: OI -> [OI]

instance Partible OI where
    parts = partsOI

我们现在可以为putstr 提供定义：

putstr s =  \ u -> foldr (\!_ -> id) () $ zipWith putchar s $ parts u

并完成bind的：

bind     :: (OI -> a) -> (a -> OI -> b) -> OI -> b
bind m k =  \ u -> let !u1:u2:_ = parts u in
                   let !x       = m u1 in
                   k x u2

unit的那个定义：

unit     :: a -> OI -> a
unit x   =  \ u -> x

不使用它的参数u，所以：

let x = puts "ha" in \ u -> let !u1:u2:_ = ... in
                            let !_ = x u1 in unit () u

是可能的 - 这怎么比：

let x = puts "ha" in \ u -> let !u1:u2:_ = ... in
                            let !_ = x u1 in x u

unit 也应该打电话给parts吗？

unit x   =  \ u -> let !_:_ = parts u in x

现在unit、bind 和next 执行的第一项任务涉及partsOI 的（间接）应用...如果OI 值被破坏 partsOI 首次使用时，无法重复使用？

否：不只是partsOI，还有putchar 和getchar - 那么这三个都可以使用一个共同的检查和破坏 机制;然后可以将 OI 参数的重用视为无效，例如通过抛出异常或引发错误（就像现在在 Haskell 中处理除零一样）。

现在，要么是那个，要么是唯一性类型......

在评估期间破坏 OI 值会排除惯用的 Haskell 类型声明。就像Int 或Char 一样，OI 需要预先定义；与partsOI、putchar和getchar一起构成抽象数据类型。

一些观察：

• partsOI 返回一个不定长度的列表；一个更简单的选择是在 Haskell 中定义这样一个列表（语法要好得多:-)

• 在bind 和next 中，仅使用parts 返回的列表的前两个成员 - 一对OI 值就足够了。

返回一对 OI 值很简单：

part u  :: Partible a => a -> (a, a)
part u  =  let !u1:u2:_ = parts u in (u1, u2)

这很有趣：

parts u =  let !(u1, u2) = part u in u1 : part u

这表明：

class Partible a where
    part  :: a -> (a, a)
    parts :: a -> [a]

     -- Minimal complete definition: part or parts
    part u  =  let !u1:u2:_ = parts u in (u1, u2)
    parts u =  let !(u1, u2) = part u in u1 : part u

partOI :: OI -> (OI, OI)

instance Partible OI where
    part = partOI

还有：

unit     :: a -> OI -> a
unit x   =  \ u -> let !(_, _) = part u in x

bind     :: (OI -> a) -> (a -> OI -> b) -> OI -> b
bind m k =  \ u -> let !(u1, u2) = part u in
                   let !x        = m u1 in
                   k x u2

next     :: (OI -> a) -> (IO -> b) -> OI -> b
next m w =  \ u -> let !(u1, u2) = part u in
                   let !_        = m u1 in
                   w u2

效果很好！还有一个细节：main main' - 当它被调用时会发生什么？

这一切都在类型签名中：

main' :: OI -> ()

一个实现会将main' 的应用评估为一个新的OI 值，然后丢弃结果； OI 值是通过类似于 partOI 用于生成它返回的 OI 值的机制获得的。

是时候把所有东西放在一起了：

 -- the OI ADT:
data OI                      
putchar  :: Char -> OI -> ()
getchar  :: OI -> Char
partOI   :: OI -> (OI, OI)


class Partible a where
    part  :: a -> (a, a)
    parts :: a -> [a]

     -- Minimal complete definition: part or parts
    part u  =  let !u1:u2:_ = parts u in (u1, u2)
    parts u =  let !(u1, u2) = part u in u1 : part u

instance Partible OI where
    part = partOI


putstr   :: String -> OI -> ()
putstr s =  \ u -> foldr (\!_ -> id) () $ zipWith putchar s $ parts u

unit     :: a -> OI -> a
unit x   =  \ u -> let !(_, _) = part u in x

bind     :: (OI -> a) -> (a -> OI -> b) -> OI -> b
bind m k =  \ u -> let !(u1, u2) = part u in
                   let !x        = m u1 in
                   k x u2

next     :: (OI -> a) -> (IO -> b) -> OI -> b
next m w =  \ u -> let !(u1, u2) = part u in
                   let !_        = m u1 in
                   w u2

instance Monad ((->) OI) where
    return = unit
    (>>=)  = bind
    (>>)   = next


{- main' :: OI -> () -}

那么...问题是什么？

什么是返回 I/O 操作的函数（如 Haskell 的 IO 类型）？

我只回答简单的问题：

什么是 I/O 操作（如 Haskell 的 IO 类型）？

在我看来，I/O 操作（Haskell 中的 IO 值）是一个抽象实体，它承载着函数类型，其域是特定于目的的可分割类型外部互动。

---

P.S：如果你想知道我为什么不使用 I/O 的 pass-the-planet 模型：

newtype IO' a    =  IO' (FauxWorld -> (FauxWorld, a))

data FauxWorld   =  FW OI

instance Monad IO' where
    return x    =  IO' $ \ s@(FW _) -> (s, x) 
    IO' m >>= k =  IO' $ \ s@(FW _) -> let !(s', x) =  m s in
                                       let !(IO' w) =  k x in
                                       w s'

putChar'         :: Char -> IO' ()
putChar' c       =  IO' $ \ (FW u) -> let !(u1, u2) =  part u in
                                      let !_        =  putchar c u1 in
                                      (FW u2, ())

putStr'          :: String -> IO' ()
putStr' s        =  IO' $ \ (FW u) -> let !(u1, u2) =  part u in
                                      let !_        =  putstr s u1 in
                                      (FW u2, ())

getChar'         :: IO' Char
getChar'         =  IO' $ \ (FW u) -> let !(u1, u2) =  part u in
                                      let !c        =  getchar u1 in
                                      (FW u2, c)