adam vogt
writes: On Wed, Nov 27, 2013 at 4:24 PM, AntC wrote: The difficult part of extensible records is exactly avoiding duplicate labels. TRex achieved it, but needed costly language extensions. HList achieves it, using a fragile combination of extensions (and giving impenetrable type errors if your program gets it wrong).
Why do you say that errors regarding duplicate instances are impenetrable?
Hi Adam, So do you think you're disproving me by showing a message "No instance for ..."? _Obviously_ "No instances" means duplicate instances -- NOT! Errm anyway, I didn't say "duplicate instances": I said errors re duplicate **labels**. And I'm talking about HList, not Atze's work. Yes, one of the (sources of) errors is alleged missing instances. Another is iresolvably undecidable instances. Another is type mis-matches. Often a single mistake in the program triggers a whole slew of errors. (There might be multiple different record types in the pgm, variously mashed together, as happens in real-life databases. Finding the one mistake can be hard work.) Don't get me wrong, HList is a hugely impressive piece of work. Especially given how 'primitive' was Haskell at the time. It relies on overlapping instances. And Oleg (at least) has repeatedly expressed doubts about the whole overlap business. (There's hints of that in the HList paper.) Whether or not you agree with him, as one of the authors, I think we should pay attention.
... Richard's overlapping/closed type functions ...
Atze's code uses them.
OK, good. (I didn't look at the code so much as at the stated design.) I did notice that Atze uses FunDeps as well as type functions. But that he doesn't use OverlappingInstances. (Or perhaps they're smuggled in via some of the imports?) I'm puzzled by Atze also needing extensions to the compiler to support closed DataKinds.
Failing when you insert an element whose label already exists can be done ...
Then PLEASE implement that. ...
... This Failure is the same trick as done with Fail in HList ...
... AND show that the resulting error handling is tractable. (If I remember, the authors of HList regarded that way of failing as a 'hack', and were not very happy. Using Richard's closed type functions it should be possible to avoid that hack -- which is why I was wanting to use them. So I'm more puzzled. OTOH, I did feed raise that unhappy hack with Richard at the time, as a counter-example that I couldn't understand how he'd handle. So perhaps he didn't.) And PLEASE say that records _can't_ contain duplicate labels. And PLEASE don't mention Leijen's paper. Instead: compare/contrast the semantics to TRex, and to MPJ/SPJ's 'Lightweight Extensible' proposal (which was found to be a bit too heavyweight to implement ;-) AntC