Haskell 是一门拥有惰性赋值特性的函数式编程语言,Normal Form是表达惰性求值的重要概念, seqdeepseq 用于将表达式求值到不同等级的 Normal Form。

Normal Form

  • Normal Form

NF是指已经被完全求值,不能再规约的表达式。对于一个求值能结束的表达式,non-strict语义可以 保证一个表达式中存在多个可规约项时,不同求值顺序最终将其规约到同样的Normal Form。

  • Weak Head Normal Form

WHNF指将表达式求值到最外层构造器或者函数抽象或者一个部分调用的内建函数。惰性求值(Lazy Evaluation)就是将一个表达式求值到WHNF。

  • Head Normal Form

对于 Head Normal Form的解释:

A term describing a lambda expression whose top level is either a variable, a data value, a built-in function applied to too few arguments, or a lambda abstraction whose body is not reducible. I.e. the top level is neither a redex nor a lambda abstraction with a reducible body.

An expression in HNF may contain redexes in argument postions whereas a normal form may not.

具体来说,相当于HNF的函数体不可规约,但参数中可以可规约项。

这三者之间的关系,可以表述为HNF是WNHF的真子集,NF是HFN的真子集。

seq

seq 函数用于 strict evaluation:

The seq function is the most basic method of introducing strictness to a Haskell program. seq :: a -> b -> b takes two arguments of any type, and returns the second. However, it also has the important property that it is magically strict in its first argument.

seq 的原理并不是直接对第一个参数求值,而是引入数据依赖,当 seq 函数的结果,也 就是第二个参数被严格求值时,保证第一个参数一定会被求值。因此也就不难理解,seq x xx 是等价的。seqstrictness annotationsBangPatterns 一样,都 用在程序的语义解释阶段,用于表达严格求值。

例如:

f !x !y = z

的语义等价于

f x y
    | x `seq` y `seq` False = undefined
    | otherwise             = z

GHC 的惰性求值通过 thunks 来实现,seq 可以被用于累积参数以确保不会形成过大的 thunks 导致程序运行时内存压力过大。例如,fold函数就可以通过严格求值来提高效率。

foldl' :: (a -> b -> a) -> a -> [b] -> a
foldl' _ z [] = z
foldl' f z (x:xs) = let z' = f z x in z' `seq` foldl' f z' xs

这个例子中,seq 函数保证了每次 z' 都会被严格求值。

$ 运算符表示将函数应用到参数上,求值。$! 是 Call-by-value 的函数应用运算符,使用 $! 时,参数会先被求值到 WHNF(Weak head normal form,弱首范式),然后再调用函数。 可以使用 seq 函数来定义 $! 运算符(实际实现是使用 strictness annotations,与 seq在语义上等价):

($!) :: (a -> b) -> a -> b
f $! x = x `seq` f x

-- f $! x = let !vx = x in f vx

seq is the only way to force evaluation of a value with a function type (except by applying it, which is liable to cause other problems).

对于函数来说,seq会将函数求值到lambda表达式的形式,也就是ready for application的 形式。例子:

-- ok, lambda is outermost
Prelude> seq (\x -> undefined) 'a'
'a'

-- not ok.  Because of the inner seq, `undefined` must be evaluated before
-- the lambda is showing
Prelude> seq (seq undefined (\x -> x)) 'b'
*** Exception: Prelude.undefined

GHC中,case...of对于参数也是严格求值,因此可以认为:

seq a b = case a of
                _ -> b

deepseq 和 NFData

deepseq 将表达式求值到NF。函数类型声明:

deepseq :: NFData a => a -> b -> b

deepseqseq 的区别在于deepseq会将参数彻底严格求值,而不仅仅是seq那样只 在顶层求值。deepseq可以被用于强制抛出异常、减少内存消耗和严格求值IO操作等,以及用于 连接并行计算策略。

deepseq对参数的求值是并行求值,不保证参数各部分的求值顺序

There is no guarantee about the ordering of evaluation. The implementation may evaluate the components of the structure in any order or in parallel. To impose an actual order on evaluation, use pseq from Control.Parallel in the parallel package.

同时,deepseq包中还包含了两个常用的函数:$!!force

  • $!!

$!!$$!类似,区别在于$!!首先将参数求值到NF而不是WHNF。

($!!) :: (NFData a) => (a -> b) -> a -> b
f $!! x = x `deepseq` f x
  • force

force函数对参数进行严格求值,并返回结果:

force :: (NFData a) => a -> a
force x = x `deepseq` x

deepseq包中定义了数据类型NFData用于表达可以被彻底地严格求值的数据类型。数据类型 Int, Float, Bool 以及 List 等都是NFData类型类的实例类型。deepseq包中的函数rnf 可以对一个NFData的实例类型的表达式进行严格求值,将其规约到NF(rnf: reduce to normal form)。

rnf :: (NFData a) -> a -> ()

rnf should reduce its argument to normal form (that is, fully evaluate all sub-components), and then return ().

seq is bad, and why?

Polymorphic seq 可能会破坏一些变换的等价性。例如在Haskell中,以下等式成立:

map g (f xs) = f (map g xs)

其中,fgxs 的类型声明分别为:

f :: [a] -> [b]
g :: a -> b
xs :: [a]

fg和分别取值:

f (x:y:_) = [seq x y]
g True = True

如果xs的值为xs = [False, True],那么:

map g (f xs) = map g (f [False, True]) = map g [True] = True
f (map g [False, True]) = f [undefined, True] = [undefined]

等式两边的值不一样,破坏了等式的性质。之所以会出现这个问题,愿意就在于seq会将List xs 中不同位置的两个值建立起依赖。更深层次的探讨,这一问题与Free Theorem有关, Free Theorems in the Presence of seq 以及 Philip Wadler 的论文 Theorems for free! 就在讨论这一问题,此外,Improvements for Free 一文看上去也很有 意思。

Polymorphic seq 在特定情况下会产生一些问题,但是其他的可选方案同样不是非常理想。如果 为seq添加一个类型类作为依赖,在使用seq时可能就需要很多的类型约束。同时,已经明确很多 内存占用过大的问题可以通过seq来解决,因此,seq也不可能被去除。

StackOverflow上另一个问题 A simple example showing that IO doesn’t satisfy the monad laws? 也很有意思,答案是使用 seq !!! 事实上,将sequndefined组合 会破坏Monad Laws,因此,所有的 Monad 都会失效。

对于一个Monad,有:

(Monad m) => m >>= return  = m

然而:

Prelude> seq ( undefined >>= return :: IO () ) "hello, world"
"hello, world"

Prelude> seq ( undefined :: IO () ) "hello, world"
*** Exception: Prelude.undefined

在这个例子中:undefined >>= returnundefined 的值不相等。使用 unsafePerformIO也会产生类似的效果。

另一个使得 Maybe 不满足 Monad Laws 的例子:

Prelude> seq ( undefined >>= return :: Maybe () ) "hello, world"
*** Exception: Prelude.undefined

Prelude> seq ( undefined :: Maybe () ) "hello, world"
*** Exception: Prelude.undefined

引用一段证明如下:

In the Kleisli category the monad gives rise to, return is the identity morphism and (<=<) is composition. So return must be an identity for (<=<):

return <=< x = x

Using seq even Identity and Maybe fail to be monads:

seq (return <=< undefined :: a -> Identity b) () = ()
seq (undefined            :: a -> Identity b) () = undefined

seq (return <=< undefined :: a -> Maybe b) () = ()
seq (undefined            :: a -> Maybe b) () = undefined

参考

最后一部分内容关于 seq is bad 的内容参考了 Jan Christiansen 在 StackOverflow 上的问题 Why is seq bad? 下的 回答