First of all, I should point out that faster extensible records have already been developed, within the HList framework: Just Do It While Compiling! Fast Extensible Records In Haskell http://www.fing.edu.uy/~mviera/papers/pepm13.pdf The authors did it without needing the total order on labels. However, one of the encoding of labels described in the HList paper had total order. I guess we weren't motivated enough to exploit it.

The real benefit of keeping the row sorted is that { x = 0 , y = 0 } and { y = 0, x = 0 } have the same type. When a row is not sorted, as in HList, then if we for example have an instance Eq for a row (because all elements support Eq) then for using (==) both arguments would have to the same order in the row or we need a manual call to a permutation function. When keeping the row ordered, this is not necessary. The same kind of problem occurs

The same kind of problem occurs when we fix the type of a function to a specific row: ( using whishful syntax )

f :: Rec [ x = Int , y = Int] -> Int

If the row is not ordered, then f { y = 0 , x = 0 } will not typecheck and will require a manual call to permute the row.

This is all very true. However, if we wish to pass the function f above the record {y=0, x=0} (with permuted fields), we most likely wish to pass that function a record {x=0, y=0, z='a'} with more fields. Most of the time when we deal with extensible records, we really wish to explore their extensibility. Keeping fields sorted does not help at all in the latter problem -- we must manually insert the call to the subtyping coercion function. Once we do that, the problem with the order of the fields disappears. I also would like to point out that there are two sorts of record types. One sort is Rec [x: Int, y:Bool] in the imagine syntax. Current HList types are uglier versions of the above. But there is another sort: (HasField r x Int, HasField r y Bool) => r It represents an extensible record type. Extensibility is build in, and the order of the fields is immaterial. Quite a few functions on records can be given the above type. Furthermore, the second sort can be used not only with structural subtyping but also with nominal subtyping.