[Haskell-cafe] Return of the revenge of the revisit of the extensible records, reiterated
vogt.adam at gmail.com
Thu Nov 28 04:16:25 UTC 2013
On Wed, Nov 27, 2013 at 9:22 PM, AntC <anthony_clayden at clear.net.nz> wrote:
>> adam vogt <vogt.adam <at> gmail.com> 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**.
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
>> ... 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 = ()
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.
More information about the Haskell-Cafe