[Haskell-cafe] Return of the revenge of the revisit of the extensible records, reiterated

[adam vogt]

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**.

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