Records in Haskell: Type-Indexed Records (another proposal)

[Matthew Farkas-Dyck]

On 06/03/2012, AntC <anthony_clayden at clear.net.nz> wrote:
> Matthew Farkas-Dyck <strake888 <at> gmail.com> writes:
>> > Oh, and how do you deal with multiple record constructors as in H98:
>> >    data T a = T1 { x :: a, y :: Bool }
>> >             | T2 { x :: a }
>> >
>> Not sure what you mean. With an argument of such a multiconstructed
>> type, I would do as ever in Haskell: pattern-match.
>
> So please show what record declarations look like. And how they get turned
> into Has instances. Your example decl on the wiki for R a b c is not valid
> Haskell.

Yet. That's what this all is about.

> What's more the wiki hss it as a `type`. Did you mean a `data`? I'm
> confused.

Nope. The record type in this case is
{ X ::. a, Y ::. b, Z ::. c, ... }

A value of this type is a record.

>>
>> > You don't give full details for your Has instances, but presumably you'd
>> > do
>> > the same equality constraint style as SORF and DORF.
>>
>> I assume you mean
>> instance (v~a) => Has k v (R a) where ...
>>
>> I'm not sure why we need this, but I assume that we do, since it was
>> written by SPJ, so yes.
>>
>
> Matthew, you really, really need to understand why SPJ put it that way, if you
> want your proposal to be taken seriously. He wasn't just making it up.

Sorry. I am no Haskell wizard, and it wasn't very clear on the wiki.
"Improves" the type of the result...?

>> > You don't show how you'd do record update.
>>
>> Yep. It's on the wiki.
>> "qfmap X f r is r mutated by f at X"
>>
>
> So do you mean this is what developers put in the code?
>
>> > what is the type for:
>> >     r{ X = True }
>> > That is: update record r, set its X field to True.
>>
>> This is written as
>> qfmap X (const True) (r :: r) :: Quasifunctor X a Bool r s => s;
>>
>
> You mean this is what to put in the code?

Well, one could, but as I said, we might (rather, ought to) define
some sugar, since it's ugly (>_<)

> DORF is getting beaten up for the amount of boilerplate the programmer is
> expected to add (for fieldLabels, etc.) I can't compare apples with apples
> for
> your proposal, because I can't see what the code looks like that would
> appear
> in the program.
>
> So far (apart from Quasifunctor) all I can see is that you're varying the
> sugar, without adding anything to the semantics -- except you've not given
> the
> surface syntax, so I'm only guessing.

I have given the surface syntax, actually, just with no sugar.

I meant not to add to the semantics. Rather, I meant to simplify them.

Anyhow, since I read DORF a few more times, my proposal seems more
alike than I thought, when I wrote it.

Nevertheless, the magic types bother me, for the aforesaid reasons.

>
> AntC
>

Cheers,
strake