What functions on lists satisfy a law with concat?

Question

What functions f :: [a] -> [a] satisfy the law:

f . concat = concat . f . map f

I can think of id, reverse, and const [] - are there others?

Jocasta

@WillemVanOnsem Interesting, but it's not so easy to find a g that makes f to have the wanted polymorphic type. Having a polytype is needed since otherwise f . map f won't type check. I found f xs = map (\_ -> head xs) xs as an example of a total function. last also works. – Submaxillary

Where does this problem naturally arise? (apart from exams) – Cyder

@Submaxillary Interesting, alas I think there are inputs where your f fails , e.g. on [[1], []] – Jocasta

@Submaxillary Try verifying f . concat $ [[1], []] vs concat . f . map f $ [[1], []] – Jocasta

Ah, you're right! I initially thought you were complaining about totality. These two examples return [1] and [1,1] so my f violates your law. I now wonder about using f [] = [] ; f (x:_) = [x] instead. – Submaxillary

@n.m. I noticed this law held with concat and reverse when thinking about possible laws that might hold between reverse, concat and transpose (prompted by trying to understand string diagrams). I wondered what other functions satisfy the same law. – Jocasta

@Submaxillary alas take 1 fails the property on [[], [1]] – Jocasta

Yep. QuickCheck also just told me that. – Submaxillary

Answer 1

There are no other (terminating) functions that satisfy the law. Below is an attempt of a proof, please poke holes in it.

If f drops any element (but not all), it fails the law.

Indeed, say f drops element with the index i from inputs of a particular length l, but preserves some other elements. Then it fails on the list [[], [], ..., [0..l-1], [], ...] (non-empty list at index i, l lists in total): f . concat returns a non-empty list, while concat . f . map f returns an empty list.

If f replicates any element, it fails the law.

Say f replicates element with the index i a finite number of times k > 1 times on inputs of a particular length l. Then it fails on the same list as above: f . concat returns a list with k occurrences of i, while concat . f . map f returns a list with k**2 occurrences of i.

So f must be either dropping all elements (i.e. be const []) or rearranging elements. Let's analyze the latter case.

It is convenient to treat f as a family of functions f_l, a separate function for each input length l. Suppose f_k is the first one that is neither id nor reverse, then it fails on [[1], [2..k]].

If non-termination is allowed, then the no-replication property does not hold (k may be infinite) and additional functions (say f [] = []; f (x:_) = repeat x) satisfy the law.

Cyder

Thanks, nice analysis! For the rearrangement case, I think we'd need to also rule out the cases where an f_i might be id but a different f_r might be reverse (which we could do by considering [[1,...,i],...,[(r-1)i,...,ri]]). I don't think your f that uses repeat satisfies the law, e.g. take 3 . f . concat $ [[], [1]] vs take 3 . concat . f . map f $ [[], [1]] – Jocasta

@MattR For your repeat counterexample, there is no finite amount of computation you can do to determine that the two are distinct. (i.e. compare "(==) never returns False" to "(==) always returns True".) It's not the usual definition of equality, but it is nevertheless a property you could consider, and presumably is the sort of thing implied by the phrase "if non-termination is allowed". – Urbanna

@DanielWagner I guess I'm interested in the question of whether two such expressions "mean the same thing", so that, say, you could use the law for equational reasoning to rewrite your program. That may not mean you can actually verify the law within Haskell itself in the case of infinite lists. It feels to me that something like "all finite prefixes denote the same value or both denote ⊥" isn't too outlandish an approximation of that intuitive idea? – Jocasta

@MattR It is not too outlandish, and indeed is the usual inductive equality. But there is also a coinductive equality that is sometimes useful, and that property is also being acknowledged in the answer here. – Urbanna

@DanielWagner Could you elaborate on what coinductive equality is? – Jocasta

@MattR I think "(==) never returns False" just about sums it up. Inductive equality is the relation you get if you demand that there be finite evidence that a given pair is in the relation; coinductive equality is the relation you get if you demand that there be no finite evidence that a given pair is not in the relation. (And this is how I think about induction and coinduction generally: induction is about the finite expansion of your set of rules, while coinduction is about the finite reduction of your set of rules.) Saying more than this requires a bit more than an SO comment's length. – Urbanna

@DanielWagner Your relation "== never returns False" isn't transitive - it seems odd to consider that as a notion of equality. – Jocasta

@MattR Can you show three sequences that break transitivity? :) – Cyder

@n.m. given a list defined as loops = loops, then loops, [1] and [2] – Jocasta

@MattR well loop isn't really a sequence, you cannot tell how many elements are there. Seriously though Haskell is not an ideal vehicle for this kind of reasoning. I think you cannot produce such a thing in Agda for example, although Agda has coinductive data types. But don't quote me on this. – Cyder

@n.m. I guess in context of the conversation, we were looking at the question of equality of concat . f . map f $ [[], [1]] with another list as a counter-example, and that of course also never produces any elements much like loops doesn't. I was curious about this idea that there might be another notion of equality that meant the law could be seen hold after all in that case, but I don't really understand "coinductive equality" (especially if it's not a transitive relation!) – Jocasta

@MattR Yes, I was being a bit sloppy to save space. I guess I should know by now that this doesn't work for math, but hope springs eternal. If you'd like to read more I think "bisimulation"/"bisimilarity" would be good search terms. – Urbanna