This is also known as "The Fundamental Theorem of Stream Calculus" in stream calculus. Using coinduction for an (infinite) stream sigma, eg

    sigma(0)      = head(sigma)
    sigma'        = tail(sigma)
    (a ++ sigma)' = sigma

I think that would fix the issue at the type level (up to a point; for unsigned types, the "correct" type for the result of a subtraction is underdetermined -- it could be any of {same type, larger signed type, same-size signed type} depending on the circumstances).

But I think the more serious niggle is the fact that that first element shows up in the output at all. OTOH, I suppose you could write a discard_first iterator adaptor that ignores the first write and increment and passes the rest through to the underlying output iterator.

T{} is now sort of that, but it didn't exist yet when adjacent_difference was written.