Mon 2 Apr 2012
In light of the burgeoning length of the ongoing record discussion sparked off by Simon Peyton-Jones in October, I would like to propose that we recognize an extension to Wadler's law (supplied in bold), which I'll refer to as the "Weak Record Conjecture" below.
In any language design, the total time spent discussing a feature in this list is proportional to two raised to the power of its position.
- 0. Semantics
- 1. Syntax
- 2. Lexical syntax
- 3. Lexical syntax of comments
- 4. Semantics of records
I base the Weak Record Conjecture on the stable of proposed record semantics, which now includes (among others) Simple Overloaded Record Fields (SORF), Agda-derived Records (ADR), Frege-derived Records (FDR), Type-Punning Declared Overloaded Record Fields (TPDORF), Syntax Directed Name Resolution, Type Indexed Records and the less seriously proposed Homotopy Extensional Record Proposal (HERP) and Dependent Extensional Record Proposal (DERP).
There is an additional option implied but not stated in all of this, which is the option to "Leave Well Enough Alone" (LWEA?), since you can always Man Up and Learn Lenses (MUALL). Given that every record proposal I've seen thus far breaks polymorphic field updates to some degree, and lenses are going to be compatible with whatever mess folks settle on, even preserving the status quo, this is the path I've chosen to take.
Now, based on the fact that discussions of syntax have already started, and the intuition supplied by the ordering already present in Wadler's insightful law, I would also like to conjecture that perhaps an even stronger version of Wadler's law might be able to be stated, the "Strong Record Conjecture".
In any language design, the total time spent discussing a feature in this list is proportional to two raised to the power of its position.
- 0. Semantics
- 1. Syntax
- 2. Lexical syntax
- 3. Lexical syntax of comments
- 4. Semantics of records
Under the Strong Record Conjecture, even in the unlikely event that universal accord could be reached on record semantics today — 164 days into this discussion — we'd still be due for at least another 3 years (328 + 656 days) of backlogged complaining over the syntax before anything gets done.
The evidence thus far is pretty strong that at least the Weak Record Conjecture holds — if anything the exponent is too small and may require further calibration, but we don't have much data yet on the Strong Record Conjecture. Consequently, and in the name of science, I plan to check in again on the record debate in 3 years. Hopefully by then we will have resolved the remaining semantic issues, and will have a better feel for the necessary time commitment required to resolve items 5 and 6.
April 4th, 2012 at 12:02 am
Both record conjectures are incorrect in the sense that Wadler’s Law is, because Wadler’s Law applies to all language designs, not just ones with an existing record design which doesn’t do the job.
If you extrapolated from only C++ discussions to all language design discussions, this would be called the Weak Concept Conjecture instead.
I have a suspicion that every programming language has a missing but highly desirable feature, or existing but broken realisation of said feature, that everyone would like fixed, but most obvious ways to fix it would have nontrivial interactions with existing features or libraries and/or break a lot of existing code.
BTW, if you think the Haskell records discussion is bad, you wait until someone bites the bullet on the module system.
April 4th, 2012 at 12:34 am
Pseudonym: Of course. :D In general the ’strong record conjecture’ can be viewed of as just a version of wadler’s original law, with a subset of the semantics separated out, since if you factor out the 2^4 factor, it IS the same law (modulo comments), but you could go back to the original 1992 version of the law, and … finish killing the joke completely.
April 4th, 2012 at 12:19 pm
The module system is an easy fix by comparison! (w/r/t nested modules only that is… once we get into ML/functors territory the can of worms/gate to hellmouth starts to open up.)