I am happy to announce a new version of bwd for backward lists! The new release added init and a few other List functions introduced in OCaml 5.1 (is_empty, find_index, and find_mapi). It also added many inlining annotations.
Backward lists are isomorphic to regular lists but place elements backward. Using a different type for semantically backward lists can avoid bugs such as missing or misusing List.rev or List.rev_append. Our strategy is to keep the elements’ textual order and avoid functions such as List.rev. Initially, this package was created to eliminate bugs in our type checkers, but we have been using it almost everywhere since then. I recommend using bwd if you use list to store anything semantically backward.
When I first heard about this it seemed like a small idea not worth bothering with a whole library about. But after using it for a while I am a total convert, I probably use backwards lists more than forwards ones, and I don’t know how functional programmers have survived so long without them! I have only two impossible wishes:
I wish backwards lists could have as congenial a syntax as forwards ones, so we could write something more like [ a; b; c ] instead of Emp <: a <: b <: c.
I wish backwards lists could have a name that doesn’t make them sound like second-class citizens. In fact, if we had the world to do over, I think one could argue that these are the forwards “lists” and the other ones are “backwards”. After all, when I write a list on a piece of paper, or even list a bunch of things verbally, where do I add new items? At the end. But I suppose calling them “backwards lists” is probably best because it makes it clear to an experienced programmer what they are.
One last comment: in type theory based proof assistants, it seems most common to define addition of (unary) natural numbers by recursion on the second argument. I’m not quite sure why this is, although one advantage is than then we can write the successor of n (e.g. in a proof by induction) as n+1, the way we do on paper. But this definition makes it much easier to prove that appending backwards lists adds their lengths than for forwards lists, since appending backwards lists is also defined by recursion on the second argument!
It is possible to define other datatypes for which the [ a; b; c ] notation can be used by giving them constructors named [] and (::), but I don’t think you can define that notation to mean something completely arbitrary?
No, I suppose you would need to make that definition the actual backward list data type. So, theoretically possible, but practically not possible unless you are OK with breaking backward-compatibility
For this reason, the following functions (including List.rev ) are considered ill-typed and should never be used
If types are supposed to represent a set of things, then it makes sens that a list of numbers is still a list of numbers whatever the ordering.
If ascending lists and descending lists are supposed to represent a different set of things in your program, why not just create a new type for this domain specific problem?
type 'a sorted = Asc of 'a list | Desc of 'a list
let lst_a = Asc [ 1; 2; 3; 4 ]
let lst_b = Desc [ 4; 3; 2; 1 ]
let to_rev = function
| Asc lst -> List.rev lst
| Desc lst -> lst
;;
By tagging the data, I can’t see how one would make a mistake
The forward/backward direction here isn’t about ascending/descending ordering of the elements. It’s about the direction of the links in the linked list [a;b;c]: a -> b -> c (forward) v/s a <- b <- c (backward), which impacts what is the more efficient direction in which to access/iterate/fold through the elements of the list as well as where to add new elements.
Regular Stdlib.List, accessing elements in the “left to right” or “textual order” is O(n), and prepending to the list is O(1).
For the Bwd.List, accessing elements in the “right to left” or “backward textual order” is O(n), and appending to the list is O(1).
I think making the rev function ill-typed is to say, don’t reverse the elements, instead, just reverse the links and pick the direction you want to iterate in - tbh, I’m not seeing major applications in my everyday development (I’m probably missing something?). I can sort of see use-cases for proof assistants - that too with a vague analogy in my head to the ideas of induction v/s backwards induction.
I understand, but to me that sounds more like an implementation detail rather than a type
I thought maybe the lib would buy you not having to to do a List.rev at the end of a computation. But after having a quick play with it that doesn’t seem to be the case, I still don’t understand what are the advantages.
let duplicate lst =
let rec aux acc = function
| [] -> acc
| h :: t -> aux (h :: h :: acc) t
in
aux [] lst |> List.rev
;;
let%test _ = duplicate [ 'a'; 'b'; 'c' ] = [ 'a'; 'a'; 'b'; 'b'; 'c'; 'c' ]
let duplicate' lst =
let open Bwd in
let open Bwd.Infix in
let rec aux acc = function
| Emp -> acc
| Snoc (t, h) -> aux (acc <: h <: h) t
in
(* We would still have to reverse our result here *)
aux Emp lst
;;
let%test _ =
let open Bwd in
let open Bwd.Infix in
(* We would still have to reverse our result here *)
duplicate' (Emp <: 'a' <: 'b' <: 'c')
= (Emp <: 'c' <: 'c' <: 'b' <: 'b' <: 'a' <: 'a')
;;
The types of forwards and backwards lists are isomorphic. So anything you can do with a backwards list, you could do with a forwards list, by just remembering which lists are having elements added to and removed from their “front” and which to their “back”. The point, as with all static typing, is just that the types enforce that documentation for you.
Think, for example, of a batched queue implemented with two lists: if the dequeueing list is forwards and the enqueueing list is backwards, then the entire queue is always “in order” and there’s no danger of forgetting to rev when the dequeueing list is empty and you move the enqueueing list into it.
(In my experience, the claim in the Bwd documentation that you should never use rev is a trifle exaggerated, but not much.)
Here is a real-world example. Before the introduction of tail-mod-cons (TMC), the following code is the most straightforward way to write a tail-recursive map: (Note that this naive version is usually less efficient than the standard non-tail-recursive version, and that’s why TMC is so great—TMC automatically makes a function tail-recursive without (significantly) slowing it down. It’s the combination of simplicity and efficiency!)
let map f (l : 'a list) : 'b list =
let rec map_aux acc =
function
| [] -> List.rev acc
| x :: xs -> map_aux (f x :: acc) xs
in
map_aux [] l
The accumulator acc is a “backward” list because the elements are semantically in reverse; List.rev is used in the end to fix the order. It’s very easy, at least in our more complicated proof assistants, to forget about the List.rev. It took us a while to painfully track down why some list was reversed, and we decided to do something dramatic to prevent all bugs of this kind. If Bwd were used, the code without the final order fix simply could not type check:
let map f (l : 'a list) : 'b list =
let rec map_aux acc =
function
| [] -> acc (* <-- This will not type check! *)
(* [acc] is of type ['b bwd], not ['b list].
You need [Bwd.to_list acc]. *)
| x :: xs -> map_aux (acc <: f x) xs
in
map_aux Emp l
To clarify, this library does not change what you have to do. Its only purpose is to exploit typing to track the semantic directions of forward/backward lists so that type checkers can better help you. It does not make sense to reverse a list just to use the library; instead, what we have learned from our experience is to check whether some lists are already “in reverse” (for example the acc in the above map) and maybe it’s a good idea to give them a different type. The design principle is summarized as the controversial slogan “rev is ill-typed” but that’s more like our own secret coding convention. Please use List.rev whenever you feel it is appropriate.
That’s Bwd.to_list, because you are not (semantically) reversing the list!
I get it, but semantically a list doesn’t define a ‘backward’ or ‘forward’ order, so you could actually argue that Bwd.to_list should preserve the backward order in the output list. That’s why I find rev : 'a t -> 'a list more descriptive
OCaml has assigned a natural textual order to almost everything, including lists. That’s how the ‘backward’ or ‘forward’ order was determined. We went further and claimed that the textual order is your best friend and we will protect it at all costs. You don’t have to agree with this philosophy, but the entire library is consistently designed under this ideology. The argument you are referring to will unfortunately be incompatible with this presupposition. In particular, because Bwd.to_list preserves the textual order, it should not be called rev. More precisely, it converts
Emp <: 1 <: 2 <: 3
to
1 :: 2 :: 3 :: [] = [1; 2; 3]
and the numbers from the left to the right are still 1, 2, and 3, in the same textual order. We only care about the textual order and use it to determine whether something is “reversed”.
I think it would make sense to have a function calledrev : 'a Bwd.t -> 'a list, but it would be different from Bwd.to_list: it would convert Emp <: 1 <: 2 <: 3 to [ 3; 2; 1 ]. In other words, it would be the “obvious” isomorphism from backwards to forwards lists.
Putting aside our avoidance of rev-like functions, I feel rev has to have the type 'a bwd -> 'a bwd to mimic the rev function in the standard library. That is, it reverses the textual order but keeps the type. Not sure what other names could be used here (naming is hard), but maybe the functions you suggested could be called
val bwd : 'a list -> 'a bwd
val fwd : 'a bwd -> 'a list
where
let bwd xs = of_list (List.rev xs)
let fwd xs = List.rev (to_list xs)
so the suggested function fwd. However, for the obvious reason I’m a bit reluctant to include these functions.
Oh I see, so we can use a backward list as a LIFO I didn’t catch that.
Thanks, I appreciate the extra explanation. I find lists to be a little tricky actually. Sometimes being able to represent or use an empty list will lead to a bug (so I use a tuple then). Other times it’s perfectly reasonable.
So, overall, there’s something intriguing about the list type I can’t quite put my finger on.
