Tracking issue for HeapLang improvements

We (primarily @robbertkrebbers, @jung, @tchajed, @arthuraa) have a few ideas for improving HeapLang as a language to write programs in. One way to improve HeapLang is by adding libraries, and another way is to add primitives to the language.

Libraries are nice because they don't break backwards compatibility, don't make metatheory harder, and are easy to incrementally develop, test, and improve. There are already libraries floating around, so this effort would be mainly developing good specifications and ergonomics, then distributing the libraries so people can start using them.

Library support

Some libraries we would like to support include:

• n-ary products and sums, either on the heap or as pure values
• lists and maps, either on the heap or as pure values

Here are a few concrete tasks to get started:

• Implement pattern matching for products. It would look something like let: ("a", "b") := "p" in ... and would bind "a" and "b" to Fst "p" and Snd "p". This is interesting because it's the simplest example we could come up with of a derived construct with binders.
• Experiment with a nice sum pattern matching library, desugaring to match: but with support for a list of variants.
• Implement a generic list matching library, for list values.
• Implement a heap linked-list library. Give it a spec in terms of list val and then a derived spec that takes list_rep {A:Type} (l:list A) (Φ: A -> iProp) (v:val), relating the list reference v to a Gallina list via a representation predicate for each element.
• Implement a map library along the same lines as the heap linked-list library, using a gmap val val and a representation predicate.

Language improvements

One simplification to the language's representation is to consolidate constructors. The best illustration of this is simp_lang which already does this; for example, Fst, Snd, InjL, and InjR are all consolidated into a single UnOp op constructor with a Gallina inductive op to identify which operation it is. One resulting simplification is that these all share the same evaluation contexts.

We could have primitive algebraic data types. This has the strong downside of requiring metatheory like logical relations to handle them in some way, whereas right now they only need cases for binary sums and products, with a simple pattern matching construct for sums that takes two lambdas. n-ary pattern matching on sums takes an arbitrary number of lambdas, which is complicated.

Adding a type discriminator would allow a generic, polymorphic equality operator. For metatheory like logical relations, most likely most users would just forbid type discrimination (eg, by not including it in the type system or logical relation), partly because it breaks abstraction.