On Wed, Nov 27, 2013 at 9:22 PM, AntC
adam vogt
writes: On Wed, Nov 27, 2013 at 4:24 PM, AntC wrote: 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**.
Hi AntC, Sorry. I typed "duplicate instances" while I intended to write "duplicate labels". The example that follows is about error messages when you try to make a record with duplicate labels.
And I'm talking about HList, not Atze's work.
Me too (at that point). I have not built a ghc with the necessary modifications to try out the openrec.
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?)
Closed type families (type family Foo a where Foo () = ..; ...) have equations that behave like overlapping instances. To use them you just need ghc-7.7 (or wait a few weeks for ghc-7.8) and just enable -XTypeFamilies.
... 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.)
Do you recall where that discussion was? The two versions of type family Failure I give are less satisfying than that the (class Fail a). I don't know of a type-level `error' besides the three approaches that have been named in this thread. Sometimes you might be able to re-work some things to get the type-level equivalent of a pattern match failure. Though it seems ghc isn't eager enough to point out "you're using a closed type family in a way that I will never be able to satisfy". For example: f x y | x == y = () -- becomes type family F x y where F x x = () But I'm not sure how to translate g x y | x /= y = () Besides re-writing it as g' x y | x == y = error "mistake" | otherwise = () Which translates to type family G' x y where G' x x = Failure "mistake" () G' x y = ()
And PLEASE say that records _can't_ contain duplicate labels.
I suppose there's one hole left. You're allowed to compile the following using HList: boom = boom :: Record [LVPair "x" Int, LVPair "x" Double] But I'm not sure that error is common enough to justify sticking a HRLabelSet constraint on every operation in the Record.hs. And even then you'd still be allowed boom in your program. Another idea is to copy the concept of a "smart constructor" for the type level. I don't think that is practical until HRLabelSet can be written as a type family. Doing the conversion means dropping ghc-7.6 support, since you can't write TypeEq as a type family without closed type families. I will wait until 7.8 is out (and a better Failure type family) before trying to re-write that bit. Regards, Adam