Extending the standard library and syntax

[nikolaushuber]

When working with Gospel I run into the same issues from time to time:

• Missing functions for sequences

Functions like mapi or map2 are defined for lists, but not for sequences. On the other hand, sequence has an append function, which is missing for lists. You can of course define them yourself, but maybe if there is enough interest they could also be added to the standard library directly.

• Signature mismatch for mem function

For lists the signature of the mem function is predicate mem (x: 'a) (l: 'a t), for sequences it is predicate mem (s: 'a t) (x: 'a)

• Boolean operators

The operators &&, ||, and not cannot be used as function names or applied partially. So for example if you want to fold over a sequence of booleans, you always have to write Sequence.fold_left (fun a b -> a && b) true xs

[n-osborne]

A new standard library is being written.
@mrjazzybread should be able to answer whether the new stdlib will answer these concerns.

&&, || and not are in fact part of the language, not the stdlib. This means they are actual nodes in the AST and can't be partially applied "by design". I believe it is worth considering changing that.

[mrjazzybread]

Missing functions for sequences
Functions like mapi or map2 are defined for lists, but not for sequences. On the other hand, sequence has an append function, which is missing for lists. You can of course define them yourself, but maybe if there is enough interest they could also be added to the standard library directly.

In the new standard library, one of our goals is to make it so the only type to describe a sequence of elements in specifications are sequences. In the next release, we will (probably) automatically coerce lists into sequences using of_seq, as well as other common coercions (e.g. int into integer). This is a bit ad-hoc and we are working on a more sophisticated way of transforming OCaml types into logical types. Since the List module will disappear from the standard library, it makes sense to add the functions that you mentioned as well as any others that were previously exclusive to the List module.

Signature mismatch for mem function
For lists the signature of the mem function is predicate mem (x: 'a) (l: 'a t), for sequences it is predicate mem (s: 'a t) (x: 'a)

In the future standard library, this specific case does not not matter since since the List module is going away regardless, but in general it is true that there are weird inconsistencies within the standard library. We hope to remove all of these in the near future.

Boolean operators
The operators &&, ||, and not cannot be used as function names or applied partially. So for example if you want to fold over a sequence of booleans, you always have to write Sequence.fold_left (fun a b -> a && b) true xs

Never really considered this and I have no strong feelings either way. I probably lean more slightly to having them defined as predicates in the library since it makes the semantics of the language more explicit and generally makes things slightly easier, both for users and maintainers.