Use nested records and tuples instead of arbitrarily long ones

[robdockins]

If I remember correctly, the idea was to make the current n-ary tuple and record syntax be sugar for a more basic binary nested construct.

[robdockins]

Quoth @brianhuffman

I'm considering multiple possibilities for encoding records and tuples.

1. Data types "UnitType :: sort 0" and "PairType :: sort 0 -> sort 0 -> sort 0", with constructors "Unit" and "Pair". Tuples would be encoded by combinations of these, nested like Nil and Cons. These could either be ordinary SAWCore datatypes, or they could be hard-coded into the term AST. Projections like "x.2" would be represented as something like "fst (snd (snd x))". Again, "fst" and "snd" could either be hard-coded in the AST, or they could be ordinary SAWCore functions (this would require them to have explicit type arguments, however). For records, you would have variants of PairType/Pair/fst/snd that take an extra string argument for the field label.

One problem with this approach is that nothing prevents you from constructing ill-formed tuples, e.g. a sequence of "Pair" constructors with no "Unit" at the end. We would have to add special cases to the parser/pretty printer to handle this.

Another problem is that order of record fields matters: {x=1,y=2} is different from {y=2,x=1}, and has a different type.

2. Use kinds "TypeList :: sort 1" and "TypeMap :: sort 1", with constructors "TNil :: TypeList", "TCons :: sort 0 -> TypeList -> TypeList", "TEmpty :: TypeMap" and "TInsert :: String -> sort 0 -> TypeMap -> TypeMap". Then we could have "TupleType :: TypeList -> sort 0" and "RecordType :: TypeMap -> sort 0". Value-level constructors would be basically like plan 1.

This encoding would be a bit more heavyweight. On the other hand, it avoids ill-formed tuple and record types and values. It also might make sense to treat "TypeMap" as a non-free datatype, so that record field order wouldn't matter.

[robdockins]

Quoth @atomb

I think (2) seems a bit more elegant. I don’t like the possibility of malformed tuple encodings, or the potential for type mismatches due to changes in field order. Both of those problems have already come up at some point in the past, and though they’re relatively easy to avoid, it’s nice if we can guarantee by design that they won’t happen. Do you have a sense for whether (2) would be more difficult to implement than (1), or if it would just mean somewhat bigger terms?

[robdockins]

Note: Cryptol seems to impose a total order on fields names (alphabetical? it seems [but in what sorting order...]) for the purposes of defining the lexicographic order in the automatic 'Cmp' instance for records.

[brianhuffman]

This was implemented in a series of changesets last September: 051f40d, a66ed9f, 47a445b, b50d42e, a16b784, 43085ae