A type for ordered lists?

Community
1

Not so long ago the cargocut crew introduced the nel library, a “very simple implementation of a non-empty list”.

In a project I’m working on we’ve had a few bugs due to forgotten List.rev calls, or missing track of the original and desired order of lists after a few List.rev_map and List.rev_append. Postfix hungarian notation (*_rev identifiers) added more noise than it helped. We ended up decorating the list with polymorphic variants: type 'a ol = [> `Straight of 'a list | `Reversed of 'a list ].
I asked the cargocut-ists for advice and we’re moving the discussion here.

I’m wondering if there’s a nice, pure type-system way of keeping track of the order (meaning, the order of insertions of elements) of a list.

@pytre wrote:

Isn’t this naïve approach sufficient? We can quickly achieve compatibility with the list API, and it’s easy to extend this module; and could we perhaps use the rev_empty constructor (or from_rev_list with from_rev_list []) to start with cons?

module Ol : sig
  type ('ord, 'a) t = private 'a list constraint 'ord = [< `Rev | `Ord ]

  (** {1 Building ordered list} *)

  val empty : ([ `Ord ], 'a) t
  val singleton : 'a -> ([ `Ord ], 'a) t
  val from_list : 'a list -> ([ `Ord ], 'a) t

  (** {1 Cons} *)

  val cons : 'a -> ([ `Rev ], 'a) t -> ([ `Rev ], 'a) t
  val append : ([ `Ord ], 'a) t -> ([ `Ord ], 'a) t -> ([ `Ord ], 'a) t

  (** {1 Kind Alteration} *)

  val rev : ([ `Ord ], 'a) t -> ([ `Rev ], 'a) t
  val unrev : ([ `Rev ], 'a) t -> ([ `Ord ], 'a) t

  (** {1 Manip preserving order} *)

  val map : ('a -> 'b) -> ('k, 'a) t -> ('k, 'b) t
end = struct
  type ('ord, 'a) t = 'a list constraint 'ord = [< `Rev | `Ord ]

  let empty = []
  let singleton x = [ x ]
  let from_list x = x
  let rev x = List.rev x
  let unrev x = List.rev x
  let map f x = List.map f x
  let cons x xs = x :: xs
  let append xs ys = xs @ ys
end

let x = Ol.from_list [ 1; 2; 3 ]
let y = Ol.cons 10 (Ol.rev x)

then hacked a bit more:

It is possible to adopt a more manual approach (by exhibiting the direction of the list):

type ('ord, 'a) t = private 'a list

type (_, _) dir =
  | Ord : ([ `Ord ], [ `Rev ]) dir
  | Rev : ([ `Rev ], [ `Ord ]) dir

val flip : ('a, 'b) dir -> ('b, 'a) dir

val empty : ('k, 'a) t
val singleton : 'a -> ('k, 'a) t
val from_list : 'a list -> ([ `Ord ], 'a) t
val from_rev_list : 'a list -> ([ `Rev ], 'a) t

val rev : ('k, 'j) dir -> ('k, 'a) t -> ('k, 'a) t

(* etc *)

To be perfectly honest, my gut feeling is that the “order of construction” is an invariant that I find ‘easy’ to maintain (which is a weakness in my reasoning, I grant you).

After which a type-system wizard was summoned, and @octachron shared this incantation:

For the direction, you can encode the negate function inside the pair of types itself to get rev without a supplementary argument

type yes = Yes type no = No
type ord = <neg: rev; ord:yes >
and rev = <neg:ord; ord:no >
type ('order,'a) t
val make: 'a list -> (ord,'a) t
val rev: (<neg:'n; ..>, 'a) t -> ('n,'a) t

and I’m wondering if I listened enough in class.

Please share any idea you may have on the subject, it’ll be nice to build a little library afterwards.

3 Likes
2

The techniques here for tracking the desired property with phantom types are nice to see :slight_smile:

But I wonder, if we find ourselves needing a data structure that has a “correct order” determined by insertion (rather than an ordering based on the links of some cons cells) does it perhaps indicate that we actually want to be working with a queue rather than a list?

3

In the case that prompted my question I don’t think a queue would have solved my problem. I’m really folding, mapping, and concatenating lists, all in tail recursive style for efficiency (though we haven’t compared perf with TRMC). This make it easy to forget one rev or add one too many!

1 Like
4

The conversation was synthetized in a @pytre 's blog post: grim.cargocut.org - Lists that keep track of their reversal (with other experiments)

5
  • Do you think this kind of invariant is important enough to track in the type system?

I generally get along fine by naming the intermediate values with _rev suffixes. Works well if the scope is small enough.

let xs_rev = List.rev_map f xs in
let xs = List.filter p xs in
let xs_rev = List.rev_map g xs in
…

It doesn’t scale very well but then when I hit the scale I tend to move away from lists (most likely to Seq).

  • Would we want to expose a library to address this problem?

If the library is only tracking the reversal for the stdlib traversors I don’t think it’s particularly useful. If the library is offering rev-based version of all the traversors (filter, filter_map, etc. but also more fun ones like partition) and also proposing something interesting for merge and the like then maybe.

Also, I’d be unlikely to use the library if I can’t use the built-in list syntax. If I have to use a cons function or a Cons constructor, then I might as well just use Seq or such.

So I’d say the library would have a narrow design space that’s viable.

6

How about the following approach, which strengthens the type of module List instead of encoding the direction into an incompatible GADT type?

mli:

module type LIST = sig
  type 'a t =
    | []
    | ( :: ) of 'a * 'a t

  (* A fresh alias, NOT an alias to the built-in 'a list type. *)
  type 'a list = 'a t

  (* Copy all function sigs from module List, except those related to reversal.*)
  val length : 'a list -> int
  val compare_lengths : 'a list -> 'b list -> int
  (* ... *)
end

module rec FwdList : sig
  include LIST
  
  val of_list : 'a List.t -> 'a t
  val to_list : 'a t -> 'a List.t

  val rev : 'a t -> 'a RevList.t
  (* other defs for rev_map, etc. *)
end

and RevList : sig
  include LIST

  val of_list : 'a List.t -> 'a t
  val to_list : 'a t -> 'a List.t

  val rev : 'a t -> 'a FwdList.t
  (* other defs for rev_map, etc. *)
end

ml:

module type LIST = ...

module List' = struct
  include List
  
  type 'a list = 'a t
  
  let of_list = Fun.id
  let to_list = Fun.id
end

module FwdList = List'
module RevList = List'