Documentation of invariant is poorly specified / incorrect

[tom93]

The documentation discusses the invariant that is relied on to preserve safe use. It gives two statements of the invariant; the first is correct but poorly specified, and the second is incorrect. Below I describe the issue, suggest a fix for the first statement, and suggest an alternative statement that in my opinion is clearer. Please let me know if you are interested in a PR for either of those.

---

The invariant is stated in two different ways (intended to be equivalent):

(A) For any xs :: DList a: fromList (toList xs) = xs

(B) (For any xs :: DList a:) toList (fromList (toList xs)) = toList xs

Statement (A) is correct but poorly specified, because it doesn't explain what = means here. The LHS and RHS are (records containing) functions, and Haskell doesn't have a notion of function equality (the == operator is not defined for functions). For the statement to make sense, it should explain that it uses extensional equality. That is, given xs :: DList a and ys :: DList a, we define xs = ys if for all l :: [a], (unsafeApplyDList xs) l = (unsafeApplyDList ys) l.

Statement (B) is incorrect -- it is actually a tautology, and is not equivalent to statement (A). To see why, let l :: [a] = toList xs. Substituting l in place of toList x in statement (B) results in toList (fromList l) = l, and it can be shown that this is true for all l. The example purporting to show that statement (B) can be broken in fact shows no such thing, because the LHS and RHS are equal in that example:

import Data.DList
import Data.DList.Unsafe (DList(UnsafeDList, unsafeApplyDList))

xs :: DList a
xs = UnsafeDList (const [])

main = do
  -- Check whether `toList (fromList (toList ys)) = toList ys` holds when ys = xs `snoc` 1
  putStr "LHS = "; print $ toList (fromList (toList (xs `snoc` 1)))
  putStr "RHS = "; print $ toList (xs `snoc` 1)
  -- Both are [].

(It is certainly surprising that toList (xs `snoc` 1) = [], but that does not break statement (B).)

---

In my opinion, would be clearer to state the invariant as follows (as done in Lean 4):

A difference list xs :: DList a is well-behaved if for all l :: [a], unsafeApplyDList xs l = unsafeApplyDList xs [] ++ l.

In other words, xs must represent some fixed collection of elements, and the behaviour of unsafeApplyDList must be to prepend these elements to l.