I wrote a tiny bit faster implementation of Data.List.inits that replaces the underlying purely functional queue with a mutable data structure and careful uses of unsafePerformIO. Can we use linear types instead of unsafePerformIO to encapsulate this as a purely functional data structure?
Implementing inits with a queue
The high-level structure of inits :: [a] -> [[a]] is the same between the standard library one and my version: scanl the input list with a queue as an accumulator, snoc-ing (pushing) elements to it. Then every prefix of the input list can be obtained by repeated uncons-ing (popping) from one of the accumulated queues.
-- pointful
inits :: [a] -> [[a]]
inits xs = empty : go empty xs
where
go q [] = []
go q (x : xs) = toList (snoc q x) : go (snoc q x) xs
-- pointfree
inits :: [a] -> [[a]]
inits = map toList . scanl' snoc empty
-- Queue API
empty :: Q a
snoc :: Q a -> a -> Q a
toList :: Q a -> [a] -- unfoldr uncons where uncons :: Q a -> Maybe (a, Q a)
This must be a real-time queue—uncons should run in non-amortized constant time—so that the output can be consumed lazily (notably map head . tail . inits :: [a] -> [a] should take linear time). This must be a persistent queue, because the same queue will be passed as an argument to both snoc (to construct the next prefix) and uncons (to produce the current prefix).
Implementing a persistent queue
The standard persistent queue is the banker’s queue described in Okasaki’s book. For inits, we also know that the only elements that will ever be pushed to the queue are the elements of the list. This allows a more efficient representation using a mutable (and resizable) array to hold the elements.
Every queue is a slice of the array: snoc appends an element at the end of the array, and uncons reads the first element of the slice. This is not a general purpose queue: we are assuming that every snoc is followed by at most one snoc, and uncons is never followed by a snoc. Under those assumptions, that data structure actually implements a purely functional interface: every queue is an immutable slice of the array; snoc only ever writes where no past slice can access.
Can we give pure (non-IO) types to the operations of that queue, and implement inits with it? Linearity is necessary to encode the usage assumptions, but is it sufficient?
Even ignoring the specifics of the implementation, I can’t imagine any linear types for a queue expressive enough to implement inits. The problem can be seen in the above definition of inits (which may be too naive to account for linearity): how can we reconcile the linearity of q with the recursive call go (snoc q x) under an unrestricted :? (Careful readers will also note the double occurrence of q, but that can easily be solved by merging toList and snoc as a single function.)
