Use the input list as the seed of the tree unfold:
buildUnfold :: [a] -> Tree a
buildUnfold = unfold step
  where
    step []  = error "build: empty input"
    step [x] = Left x
    step xs  = Right (split (length xs `div` 2) xs)
On a singleton seed, unfold produces the same leaf as build; on a longer finite seed, it recursively builds the same two pieces. Induction on input length proves buildUnfold = build on finite nonempty inputs. The empty-input qualification remains essential: a tree unfold cannot supply a missing empty-tree constructor.
The necessary domain is a finite, nonempty list: the datatype has no representation of an empty leaf sequence, and the supplied size-based balance condition does not specify an infinite-size construction.
build :: [a] -> Tree a
build []  = error "build: empty input"
build [x] = One x
build xs  = Two (build ys) (build zs)
  where
    (ys,zs) = split (length xs `div` 2) xs
For length , the two nonempty pieces have and elements. Their sizes differ by at most one, and both are shorter than the input. Induction therefore proves termination and the required leaf-balanced binary tree property at every node. The same induction, using ys ++ zs = xs, proves flatten (build xs) = xs. This straightforward implementation takes running time; computing the length repeatedly is acceptable here because no faster construction was requested.
Let be the number of leaves; the total number of nodes is . List concatenation copies its left operand. For a tree whose left subtree contains leaves at each successive internal node, these copied lengths are . Their sum is , so the worst-case running time is .
A difference list representation avoids copying prefixes:
flattenFast :: Tree a -> [a]
flattenFast t = go t []
  where
    go (One x)   acc = x:acc
    go (Two l r) acc = go l (go r acc)
The recursion invariant is go t acc = flatten t ++ acc. The leaf case is immediate; the internal-node case uses associativity of list concatenation. Each node is visited once and each leaf contributes one output constructor, giving running time when the result is fully consumed. This is linear flattening of a binary tree and does not assume balance.
Both versions preserve left-to-right leaf order:
flatten :: Tree a -> [a]
flatten (One x)   = [x]
flatten (Two l r) = flatten l ++ flatten r

flattenFold :: Tree a -> [a]
flattenFold = foldTree (\x -> [x]) (++)
The tree fold replaces each leaf by a singleton list and each internal node by list concatenation. The defining equations of flattenFold are consequently those of flatten, proving their equality by structural induction.
For the paper's leaf-labelled binary tree, the combining operation receives the results of the two subtrees, and the other argument handles a leaf:
foldTree :: (a -> b) -> (b -> b -> b) -> Tree a -> b
foldTree f g (One x)   = f x
foldTree f g (Two l r) = g (foldTree f g l) (foldTree f g r)
Its constructor equation is foldTree One Two = id. More generally, a function h satisfying h (One x) = f x and h (Two l r) = g (h l) (h r) equals foldTree f g on finite trees, by structural induction. This is the tree fold specialized to a datatype with labels only at leaves, rather than at internal nodes.
A shared recursion computes both components:
split :: Int -> [a] -> ([a],[a])
split n xs | n <= 0 = ([],xs)
split _ []         = ([],[])
split n (x:xs)     = (x:ys,zs)
  where (ys,zs) = split (n-1) xs
For a defined count and a spine with available constructors before termination, each of take and drop makes recursive calls, whereas split makes that many once. The number of recursive calls is halved. The irrefutable pattern in the local pair binding also avoids evaluating the recursive pair merely to expose the first output element.
On proper lazy lists this has the intended two component values. There is a small bottom value distinction outside that domain: the displayed single-pass definition must inspect a positive-count input spine before returning its outer pair, whereas the literal expression (take n xs, drop n xs) exposes the pair constructor even if xs is undefined. The algorithmic answer concerns the two components and the stated call count; it need not silently claim equality under a test that observes this outer constructor alone.
Include nonpositive counts and exhausted input explicitly:
take :: Int -> [a] -> [a]
take n _      | n <= 0 = []
take _ []             = []
take n (x:xs)         = x : take (n-1) xs

drop :: Int -> [a] -> [a]
drop n xs     | n <= 0 = xs
drop _ []             = []
drop n (_:xs)         = drop (n-1) xs
The tests on the count precede inspection of the input list. Thus take 0 undefined = [], while drop 0 undefined = undefined, exactly as these list prefix and list suffix operations require. No element value is inspected merely to traverse the spine.[ref]
Fix s and put . The right fold equations give
These are exactly the left fold equations. Structural induction, with the induction hypothesis quantified over all accumulators, proves equality on finite terminating lists.
To include the other input spines, first observe that both applied expressions give on an undefined spine. The same induction proves equality on every finite prefix ending in : the step k s x f a demands the continuation f when its result is demanded. Finally use that the two applied operations are Scott continuous maps, taking the limit over prefixes interpreted as a finite approximation of a lazy list. This covers infinite spines, on which both applied expressions are , and proves the identity for all lists under the stated Haskell semantics. The intermediate right fold builds an accumulator-transforming function; it does not provide a terminating left fold of an infinite list.
Assign and . The application s y x forces for a fresh type ; applying f to that result forces . No further equations identify these four type variables. The principal type is therefore
k :: (u -> v -> w) -> v -> (w -> r) -> u -> r
k s x f y = f (s y x)
Every compatible typing is an instance of this one, because type inference imposed precisely the two application constraints and no class constraints.
Let , using the specified operation . Direct evaluation gives , , , and .
Suppose with the same integer result type. The empty list forces . The two singleton calculations force and . But then
contrary to . No such c,b exist. This is the information restriction in the fold factorisation criterion: equal folded tails must remain indistinguishable after the same head is attached. A larger, function-valued result type can retain the missing information, as the continuation representation of a left fold does below.
Over integers, choose s = (-), c = flip (-), and a = b = 0. The left fold and right fold both compute the negative of the sum of a finite list. The combining functions differ: s 1 2 = -1, whereas c 1 2 = 1.
For every accumulator , pattern matching makes foldl s a undefined the bottom value. Now use structural induction on a finite list prefix ending in the bottom value. The induction step is foldl s a (x:ps) = foldl s (s a x) ps; the induction hypothesis applies to every accumulator, including s a x. Consequently every such finite approximation has result .
An infinite lazy list is the limit of its finite prefixes, each interpreted as a finite approximation of a lazy list. Definable Haskell operations are Scott continuous maps, so the result on the infinite lazy list is the supremum of the results on these approximations. Every result is , hence foldl s a xs = undefined on every infinite input spine, irrespective of whether s would inspect the accumulator.
For a concrete separation, choose s = (&&), a = True, and xs = False : repeat True. The left fold is , whereas the right fold returns False after observing the first element: False && r does not demand r. It is reaching the end of the input spine, rather than strictness of the combining operation, that prevents this left fold from returning.
The right fold replaces the two list constructors by its two arguments; the left fold instead updates an accumulator while traversing the list.
foldr :: (a -> b -> b) -> b -> [a] -> b
foldr c z []     = z
foldr c z (x:xs) = c x (foldr c z xs)

foldl :: (b -> a -> b) -> b -> [a] -> b
foldl s a []     = a
foldl s a (x:xs) = foldl s (s a x) xs
Thus foldr is the natural list fold: it preserves the constructor arrangement while replacing [] by z and (:) by c. In particular, foldr (:) [] = id. More generally, the fold factorisation criterion says that the defining equations characterize the corresponding structural recursion. Association and lazy evaluation are separate: the accumulator in this definition of left fold is not automatically evaluated at each step.[ref]
By linearity of expectation, . Expanding the square and again using linearity of expectation gives
Here the zero means imply and . The covariance expansion itself does not require independence. Under the additional independence stated here, , so it simplifies further to .

Pinned article: Introduction to the OurBigBook Project

Welcome to the OurBigBook Project! Our goal is to create the perfect publishing platform for STEM subjects, and get university-level students to write the best free STEM tutorials ever.
Everyone is welcome to create an account and play with the site: ourbigbook.com/go/register. We belive that students themselves can write amazing tutorials, but teachers are welcome too. You can write about anything you want, it doesn't have to be STEM or even educational. Silly test content is very welcome and you won't be penalized in any way. Just keep it legal!
We have two killer features:
  1. topics: topics group articles by different users with the same title, e.g. here is the topic for the "Fundamental Theorem of Calculus" ourbigbook.com/go/topic/fundamental-theorem-of-calculus
    Articles of different users are sorted by upvote within each article page. This feature is a bit like:
    • a Wikipedia where each user can have their own version of each article
    • a Q&A website like Stack Overflow, where multiple people can give their views on a given topic, and the best ones are sorted by upvote. Except you don't need to wait for someone to ask first, and any topic goes, no matter how narrow or broad
    This feature makes it possible for readers to find better explanations of any topic created by other writers. And it allows writers to create an explanation in a place that readers might actually find it.
    Figure 1.
    Screenshot of the "Derivative" topic page
    . View it live at: ourbigbook.com/go/topic/derivative
  2. local editing: you can store all your personal knowledge base content locally in a plaintext markup format that can be edited locally and published either:
    This way you can be sure that even if OurBigBook.com were to go down one day (which we have no plans to do as it is quite cheap to host!), your content will still be perfectly readable as a static site.
    Figure 5. . You can also edit articles on the Web editor without installing anything locally.
    Video 3.
    Edit locally and publish demo
    . Source. This shows editing OurBigBook Markup and publishing it using the Visual Studio Code extension.
  3. https://raw.githubusercontent.com/ourbigbook/ourbigbook-media/master/feature/x/hilbert-space-arrow.png
  4. Infinitely deep tables of contents:
    Figure 6.
    Dynamic article tree with infinitely deep table of contents
    .
    Descendant pages can also show up as toplevel e.g.: ourbigbook.com/cirosantilli/chordate-subclade
All our software is open source and hosted at: github.com/ourbigbook/ourbigbook
Further documentation can be found at: docs.ourbigbook.com
Feel free to reach our to us for any help or suggestions: docs.ourbigbook.com/#contact