What is the justification for the type of unfoldr in Haskell?

Question

The example given in the documentation of unfoldr :: (b -> Maybe (a, b)) -> b -> [a]:

unfoldr (\b -> if b == 0 then Nothing else Just (b, b-1)) 10

can easily be written with a redundant pair:

unfoldr (\b -> if b == 1 then Nothing else Just (b-1, b-1)) 11

What does unfoldr need the pair (a,b) for? Why is its type not (a -> Maybe a) -> a -> [a]?

Laquitalar

@jwodder, both fragments result in [10,9,8,7,6,5,4,3,2,1] when I test in ghci... – Laquitalar

Related question – Sympathetic

Answer 1

A function with type

(a -> Maybe a) -> a -> [a]

restricts the output list element type to be the same as the state which is threaded through the generation process. unfoldr is more general in that it allows an independent type of state to be used.

Godchild

The question I have is whether this theoretically more general type serves any practical purpose or not and if yes if you can give a good example. Certainly the standard example does not make the usefulness of the more elaborate type apparent, as I showed in my question. – Laquitalar

@Laquitalar Replace Just (b, b-1) with Just (show b, b-1). – Halvorson

@Laquitalar A more useful example is: repeat n x = unfoldr (\b -> if b == 0 then Nothing else Just (x, b-1)) n. The type of repeat is Int -> a -> [a], so that repeat 5 1 == [1,1,1,1,1] but also repeat 5 'a' == "aaaaa". With your version of unfoldr you cannot implement repeat as a simple call to unfoldr. – Halvorson

Answer 2

Leveraging a bit of theory, one can recover the types for folds/unfolds of a recursive type, including lists, understanding why they are what they are.

Let A be a fixed type. The type "list of As" satisfies the isomorphism

List ~~ Either () (A, List)

which can be read "a list value is either a special value (the empty list), or a value of type A followed by a list value".

In a more succinct notation we could write Either as an infix +:

List ~~ () + (A, List)

Now, if we let F b = () + (A, b), we have that

List ~~ F List

The above is a fixed point equation, which always arises when using recursive types. For any recursive type defined by T ~~ F T we can derive the type of the related folds/unfolds (also known as cata/ana or induction/coinduction principles)

fold   :: (F b -> b) -> T -> b
unfold :: (b -> F b) -> b -> T

In the case of lists, we then obtain

fold    :: ((() + (A, b)) -> b) -> List -> b
unfoldr :: (b -> (() + (A, b))) -> b -> List 

The unfold can also be rewritten noting that Maybe c ~~ () + c:

unfoldr :: (b -> Maybe (A, b)) -> b -> List 

The fold can instead be rewritten using

((x + y) -> z) ~~ (x -> z, y -> z)

getting

foldr :: (() -> b, (A, b) -> b) -> List -> b

then, since () -> b ~~ b,

foldr :: (b, (A, b) -> b) -> List -> b

finally, since (x, y) -> z ~~ x -> y -> z (currying), we have

foldr :: b -> ((A, b) -> b) -> List -> b

and again:

foldr :: b -> (A -> b -> b) -> List -> b

and with a final flip x -> y -> z ~~ y -> x -> z:

foldr :: (A -> b -> b) -> b -> List -> b

---

How do those types follow from the (co)induction principles?

Domain theory states that least fixed points (F(T)=T) coincide with least prefixed points (F(T)<=T), when F is monotonic over a certain poset.

The induction principle simple states that, if T is the least prefixed point, and F(U)<=U, then T<=U. (Proof. It is the least!. QED.) In formulae,

(F(U) <= U)  ==>  (T <= U)

To deal with fixed points over types, we need to switch from posets to categories, which makes everything more complex. Very, very roughly, every <= is replaced with some morphism. For instance, F(U)<=U now means that there is some morphism F U -> U. "Monotonic F" means that F is a functor (since a<=b implying F(a)<=F(b) now becomes (a->b) implying F a -> F b). Prefixed points are F-algebras (F u -> u). "Least" becomes "initial". And so on.

Hence the type of fold: (implication is -> as well)

fold   :: (F u -> u) -> (T -> u)

Unfold derives from the coinduction principle, which deals with greatest postfix points T (which become coalgebras)

(U <= F(U)) ==> (U <= T)

Ledaledah

Certainly very interesting, but I feel that you have not given enough attention to the part where you introduce the initial types of folds and unfolds. How do those types follow from the (co)induction principles? – Laquitalar

@Laquitalar True. Edited to shed some light. – Ledaledah