A strict function satisfies , where is the bottom value representing an undefined or nonterminating computation. This is a semantic implication: obtaining a defined result requires enough definedness of the argument. It does not prescribe an evaluation order or say that every component of a structured argument is evaluated.[ref]
For example, in Haskell,is strict, since every result is , but never needs to inspect its argument. Moreover, lazy evaluation may leave an entire application unevaluated when its result is unused. Strictness is therefore different from the operational statement that an argument is evaluated on every call.
f :: a -> b
f _ = undefinedThe list fold criterion is: there must be a value
z and a definable combining function c such thatThe last equality says that all information needed about the tail factors through f xs; the combining function receives no other access to xs. These conditions give f = foldr c z.Necessity follows from the defining equations of
foldr, including its case distinction on the input list. Sufficiency follows by structural induction for finite lists and finite partial-list approximations. For infinite or partial lazy lists, the usual continuous semantics of these definable functions extends equality from the approximations to their limit. The strictness condition matters: agreement only on finite total lists does not establish agreement at . This is the fold factorisation criterion.Use these structural recursion definitions in Haskell:The first definition returns a known outer constructor even when
tails :: [a] -> [[a]]
tails xs = xs : ptails xs
ptails :: [a] -> [[a]]
ptails [] = []
ptails (_:xs) = tails xs
ntails :: [a] -> [[a]]
ntails [] = []
ntails xs@(_:rest) = xs : ntails restxs is undefined, so null (tails undefined) is False, as required. The pattern in ntails must first determine whether the input is empty. Each suffix of a list is shared with the original list; on a finite input of length , constructing the outer lists takes work and additional outer-list space. No suffix is copied or measured repeatedly.tails is not a direct list fold. Every foldr c z is strict in its list argument, but tails undefined = undefined : undefined has a defined outer constructor. Applying null distinguishes this result from .ptails is not a direct list fold either. On a type with distinct values u and v,A fold step given the same new head x and these equal folded tails must return the same result. However,Thus the tail information needed by the next step does not factor through ptails; this violates the fold factorisation criterion even on finite total lists.ntails is a direct list fold:ntailsFold :: [a] -> [[a]]
ntailsFold = foldr step []
where
step x yss = (x : original yss) : yss
original [] = []
original (ys:_) = ys[]. Hence original (ntailsFold xs) = xs. The inner case distinction is delayed beneath constructors, so the definition also preserves the required behaviour on partial and infinite lazy lists. Building a suffix head does not first demand the whole folded tail.For prefixes of a list, the corresponding Haskell definitions areThe empty prefix is available without inspecting the input in
inits :: [a] -> [[a]]
inits xs = [] : ninits xs
pinits :: [a] -> [[a]]
pinits [] = []
pinits (x:xs) = [] : map (x:) (pinits xs)
ninits :: [a] -> [[a]]
ninits [] = []
ninits (x:xs) = map (x:) (inits xs)inits. Every nonempty prefix of a list begins with its input's head, explaining the last equation. For pinits (x:xs), prepend x only to proper prefixes of xs, and include the empty prefix.On finite inputs,
inits [] = [[]], whereas both other functions return []. On an infinite input, all finite prefixes are proper and these definitions produce them incrementally. Fully constructing all elements of all prefixes takes work for an input of length , matching the size of that output; there are no repeated end-append operations to add another factor.inits is not a direct list fold: inits undefined = [] : undefined has a defined outer constructor, while foldr c z undefined is .Both For
pinits and ninits are direct list folds:pinitsFold :: [a] -> [[a]]
pinitsFold = foldr (\x yss -> [] : map (x:) yss) []
ninitsFold :: [a] -> [[a]]
ninitsFold = foldr (\x yss -> [x] : map (x:) yss) []pinits, the combining function is exactly the recursive step above. For ninits, expand inits xs = [] : ninits xs and useNeither step needs to inspect yss before producing its first outer constructor. Thus the definitions satisfy the fold factorisation criterion on partial as well as total lazy lists. Articles by others on the same topic
There are currently no matching articles.