Use the usual left-to-right pattern matching order:
zip :: [a] -> [b] -> [(a,b)]
zip []     _      = []
zip _      []     = []
zip (x:xs) (y:ys) = (x,y) : zip xs ys
The result stops when either list ends, so its length on finite total inputs is the smaller input length. Elements remaining in the longer list are discarded.
Strictness is asymmetric. Writing the bottom value as , zip is strict in its first list but not uniformly strict in its second: zip undefined ys is undefined, whereas zip [] undefined = []. With a nonempty first list, an undefined second list does make the result undefined. Neither pair component is forced merely to produce the outer result constructor: zip [undefined] [undefined] already has a defined outer cons and pair. This follows from ordered pattern matching and lazy evaluation, not from the behavior on total lists alone.[ref]
Apply the supplied function to corresponding elements while preserving the stopping rule:
zipWith :: (a -> b -> c) -> [a] -> [b] -> [c]
zipWith f []     _      = []
zipWith f _      []     = []
zipWith f (x:xs) (y:ys) = f x y : zipWith f xs ys
Because of lazy evaluation, constructing a result cons does not by itself evaluate f x y.
The two required equations are
zipWith f xs ys = map (uncurry f) (zip xs ys)
zip xs ys       = zipWith (,) xs ys
Either equation defines one operation from an independently defined other operation. They do not together supply an effective recursive definition of the intended operations. Substitution makes the first output constructor depend on itself without first emitting anything, so the mutually recursive program has the bottom value as its least solution. At the level of equations they also fail to characterize the intended operations uniquely: returning [] for every call of either operation satisfies both equations, as does the intended list zip. A constructor-producing base/step definition is essential for productivity.
zero, one :: Num a => [a]
zero = 0 : zero
one  = 1 : zero
For ordinary numeric coefficients such as Rational, zero == zero does not terminate, while zero == one is False. The former comparison never finds a differing coefficient or reaches two empty lists; the latter rejects the unequal first coefficients immediately. Equality of denoted formal power series is mathematical equality of all coefficients, whereas this executable list comparison is a potentially nonterminating procedure.
Addition and subtraction of formal power series are coefficientwise:
plus, minus :: Num a => [a] -> [a] -> [a]
plus  = zipWith (+)
minus = zipWith (-)
Here every valid input is an infinite coefficient list. If finite polynomial coefficient lists were admitted, they would need zero-padding before these definitions: ordinary list zip otherwise truncates to the shorter length.
The coefficient index supplies the multiplier for a formal derivative and the divisor for a zero-constant formal integral:
deriv :: Num a => [a] -> [a]
deriv as = zipWith (*) (map fromInteger [1..]) (tail as)

integral :: Fractional a => [a] -> [a]
integral as = 0 : zipWith (/) as (map fromInteger [1..])
Using fromInteger makes the index stream unbounded before conversion to the coefficient type. The formal derivative drops the original constant coefficient; the formal integral prepends its chosen zero constant. With exact Rational coefficients these are exact algebraic operations. Analytic convergence is unnecessary for operations on formal power series over a characteristic-zero field.
The derivative fixed-point equation is unsuitable as an executable definition: requesting its first coefficient asks for the second coefficient of the same stream, then the third, indefinitely. It is not productive. As an algebraic equation it is also missing the constant coefficient: every scalar multiple of the formal power series exponential, including zero, satisfies it.
expx :: Fractional a => [a]
expx = plus one (integral expx)
The initial coefficient is available as 1 + 0; each subsequent coefficient needs only a previously determined coefficient. The recurrence relation is and , so . This proves both uniqueness of the formal solution and productivity of every finite coefficient list prefix.
The derivative relations and initial values give , , and . Integrating from zero yields and . Thus use mutually recursive lazy lists:
sinx, cosx :: Fractional a => [a]
sinx = integral cosx
cosx = minus one (integral sinx)
Both heads are available immediately, and later coefficients depend on earlier coefficients of the other stream. The resulting formal power series are and . Their zero coefficients and alternating signs follow directly from the coupled recurrence relations, providing a coefficientwise proof without assumptions about analytic convergence.

Articles by others on the same topic (0)

There are currently no matching articles.