Sequences vs. Lists in F*: when to use each

[klinvill]

This is a question I believe I've seen come across the Slack before, but I seem to never remember the subtleties between sequences and lists, so I'm asking here for posterity.

Sequences (exposed as seq) and lists (exposed as list) are very similar in that they both represent ordered collections of elements. list looks to be a built-in F* type while seq provides an interface on top of the list type (in its implementation). When would you want to use seqs over lists for new modules? When would you want to use lists over seqs?

[nikswamy]

Sequences provide a functional-array interface to lists. The sequence interface is oriented around index-based operations---Seq.index, Seq.slice etc. Lists, in contrast, are more idiomatically used with pattern matching and induction or recursion.

I would use seq when the common operations on a structure are index-based, e.g., we use seq in libraries like LowStar.Buffer, Pulse.Lib.Array etc., as a functional model of mutable arrays.

Use list when the common operations are maps and folds.

The are conversions in both directions: seq_to_list and seq_of_list. So, if you do start off using lists and find that in a part of your development, sequences would be better, or vice versa, then you can convert. That said, as currently implemented, these conversions are actually quite expensive, which may matter if these conversions appear in executable code rather than in spec. That's because these conversion are implemented on top of the Seq.Base interface, rather than beneath it---which is useful because then the F* normalizer can reduce, say, seq_of_list [1;2;3]. We could additionally provide more efficient (almost) identity coercions in FStar.Seq.Base.

[mtzguido]

On the topic of the conversions being expensive, see #3203