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.

Pierre R. 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.

1 Like