Stefan Monnier monnier@iro.umontreal.ca wrote more than a year ago:
Wondering if you might have an idea:
In Typer, the basic datastructure is the "algebraic datatype" (which combines a sum, product, and recursion), and the basic eliminator is the "pattern matching case".
It works OK, but is unsatisfactory: 1- both of those are fairly large/complex. 2- it means that extracting a record field is a "case" operation that discards all but the required field, so it's an O(n) operation (where n is the size of the record), if not in the final code, at least in intermediate code. 3- it means the choice of representation of datatype tags is hardcoded in the blackbox compiler.
While point n°2 might seem irrelevant, it is a pain with large records, such as those you might get when records are used to represent modules: the encoding of the simple "String.concat" reference ends up taking space proportional to the number of primitives exported from the "String" module, which can be rather large.
I just pushed a new branch "report/itd" where I'm working on an article that tries to provide a partial answer. It doesn't try to address point 3 and keeps tags (which I call "labels") abstract (I'm not sure it should be addressed at this level).
I intend to submit it to CPP'2019 two weeks from now (Oct 18). Anybody interested is welcome to join. The main contribution is supposed to be first a proof of equivalence of "CC + tuples + tags + union + eq-type + recursion" and "CC + inductive types" (where those inductive types follow the design of Gimenez's "case + guarded recursion") and second a proof that the intended low-level semantics (where `case` doesn't do anything more than C's `switch`) is valid.
Formalizing CC in something like Coq is pretty hard, so clearly these proof will be paper proofs (and won't be in the paper, except maybe for some highlights).
Stefan