线性类型场景下高阶函数Lowering变换可行性技术问询

你提到的这个变换是完全可行的，仅在具备线性类型约束的环境下合法，无类型约束的普通场景确实无法实现该逻辑。

合法性解释 #

• 普通场景下不合法的原因：常规高阶函数不存在调用次数约束，你无法保证传入的高阶函数会恰好调用一次你提供的a -> b回调：可能不调用导致没有a值产生，也可能调用多次产生多个a值，根本无法安全地将唯一的a从闭包中取出返回。
• 线性类型下合法的核心依据：
  • 签名中高阶函数参数((a %1-> b) %1-> r)本身是线性修饰的，必须被恰好调用一次
  • 你传入给高阶函数的a %1-> b回调也是线性类型，高阶函数拿到该回调后必须恰好消耗（调用）一次，因此必然会产生且仅产生一个a类型的值
  • 你可以通过单次写入的线性容器暂存回调被调用时传入的a，待高阶函数执行完成拿到返回值r后，即可安全取出暂存的a，和r配对作为最终结果返回

参考实现（基于GHC Linear Haskell扩展） #

import Control.Monad.ST.Linear (runST, newEmptyRef, writeRef, readRef)
import Prelude.Linear (lseq)

lower :: ((a %1-> b) %1-> r) %1-> b %1-> (r, a)
lower hof b = runST $ do
  -- 分配仅可写入一次的线性引用
  ref <- newEmptyRef
  -- 构造传给高阶函数的回调：写入a后直接返回传入的b
  let callback :: a %1-> b
      callback a = writeRef ref a `lseq` b
  -- 调用高阶函数拿到r
  let r = hof callback
  -- 安全读取唯一写入的a
  a <- readRef ref
  pure (r, a)

注意事项 #

该实现完全依赖线性类型的调用次数约束，没有线性检查的场景下该逻辑会存在空值、重复赋值等安全隐患，完全不符合类型安全要求。

内容的提问来源于stack exchange，提问作者OllieB