Yes, it is a very unusual definition of a record. As you rightfully noted, typically, a record is defined as a composite data structure mixing data types (indee

Yes, it is a very unusual definition of a record. As you rightfully noted, typically, a record is defined as a composite data structure mixing data types (indeed something more or less equivalent to a C struct basically). Access by name is not even truly necessary and the difference between tuples and records is minimal (you could build something looking exactly like field access on top of tuples with functions and would get as a result something indistinguishable from an actual record). The existence or not of an order is then totally accessory and it's generally straightforward to build an order on both provided the data types they contain is orderable by ordering the field and then using a lexicographic order.