强函数式编程
✍ dations ◷ 2025-06-20 05:32:32 #强函数式编程
强函数式编程(也称为全函数式编程),与之相对的是普通的或者说弱函数式编程。是一种编程范式,它将程序的范围限制为可证明停机的程序。
在满足下列限制的条件时,程序一定会终止:
这些限制意味着强函数式编程不是图灵完备的。但是,我们仍然可以使用很多算法。例如,任何可以计算渐近上限的算法(仅使用 Walther 递归的程序)都可以将上限作为额外的参数,从而在每次递归中递减该参数,使其变为子结构递归的形式。
例如,通常的快速排序并不是以子结构递归的形式编写的,但它的递归深度不会超过数组的长度(最坏情况时间复杂度O(2))。下面是用Haskell实现的一个不满足子结构递归的快速排序:
import Data.List (partition)qsort = qsort = qsort (a:as) = let (lesser, greater) = partition (<a) as in qsort lesser ++ ++ qsort greater
利用数组的长度信息来限制函数,我们可以将其改写为子结构递归的形式:
import Data.List (partition)qsort x = qsortSub x x-- 数组为空的情况qsortSub as = as -- 返回本身-- 数组非空的情况qsortSub (l:ls) = -- 空数组,不需要递归qsortSub (l:ls) = -- 只有一个元素,不需要递归qsortSub (l:ls) (a:as) = let (lesser, greater) = partition (<a) as -- 发生递归,但是每次递归的参数中,as都是ls的子集 in qsortSub ls lesser ++ ++ qsortSub ls greater
有一些算法没有理论上的上限,但可以设定一个实际的上限(例如,一些基于启发式的算法可以在多次递归后“放弃”,从而确保终止)。
强函数式编程会导致立刻求值和懒惰求值的行为在理论上是一致的。当然,二者实际执行时由于性能原因还是有一定的差别的,有时仍然需要选择其中一个。
在强函数式编程中,数据和辅助数据是有区别的——前者是有限的,而后者可能是无限的。无限的数据可以表示诸如I/O这样的资源,而使用这些辅助数据则需要诸如共递归之类的操作。但是,具有依赖类型的强函数式语言也可以在没有辅助数据的情况下来操作I/O。
Epigram和Charity都可以被认为是强函数式编程语言,即使它们的工式与特纳在他的论文中指定的那样不同。这样的语言可以直接在系统F、直觉类理论或构造演算中进行编程。