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

[Matthew Farkas-Dyck]

On 03/03/2012, AntC <anthony_clayden at clear.net.nz> wrote:
> Apart from the Quasifunctor bit, I think you'll find your proposal is a rather
> cut-down version of DORF, just using different syntactic sugar.

> (Oh, and with the arguments to Has in a different order, just to be confusing.)

Not so. I chose this order to make it easier to curry.

> You do have the equivalent of fieldLabel decls. Those are all your type
> indexes: data X = X, etc.

True, but data is not a new keyword.

> And you suggest defining
>     x = X

We can define x = X, if we wish, but we need not; we could rather
define x as a selector. It's just that lower-case labels are customary
in Haskell.

> Which is equivalent to DORF mapping from field name `x` to phantom type
> Proxy_x, (but DORF keeps `x` as a field selector function, similar to H98).

Ah, not quite. In DORF, the phantom type is an implicit, magical type,
but in TIR it's an explicit, declared type.

In DORF, either the magical type is in scope, or not; in the former
case, it might clash with a user-defined type, and in the latter, if I
wish to call set, how shall I type its argument?

In TIR, the key type is user-defined, so if there be a clash, then the
user is at fault.

> To make `x` a selector function instead, you'd go:
>     x = (.) X           -- or probably x = get X, see below
> Which is exactly the same as DORF (after adjusting for the different order
> of
> arguments).

True.

> And presumably instead of X you'd want a LongandMeaningfulLabel?

No! Real Programmers never choose such names!

I jest. Yes, plainly, I would. X is just an example.

> And if your
>     data Customer_id = Customer_id
> was always an Int field, wouldn't it help the reader and the compiler to say
> that? (That's the main extra part in fieldLabels.)

It might help the reader, but so would a simple comment. Nevertheless,
this is fair.

It might help the compiler, but that's an argument by premature
optimization, I think (^_~)

> I think you don't want all those type vars in your record decls -- but only
> vars for the mutatable types, like this:
>
>   type R c = { X ::. Int, Y::. String, Z ::. c, ... }
>
> Then you don't need a Quasifunctor instance for every field, only the
> mutatable ones.

Yes, I know. That is just a very general example.

> Oh, and how do you deal with multiple record constructors as in H98:
>    data T a = T1 { x :: a, y :: Bool }
>             | T2 { x :: a }
>
> It wouldn't work to have a different record type for each constructor, 'cos
> you'd turn functions that use them from mono to polymorphic (overloaded --
> needing a class and instances).

Not sure what you mean. With an argument of such a multiconstructed
type, I would do as ever in Haskell: pattern-match.

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

> I think you still need method get and sugar to turn the dot notation into a
> call to get. Having method (.) will usurp altogether dot as function
> composition -- you'll make a lot of enemies! And we need tight binding for
> dot
> notation, so we might as well treat it as special syntax.

Not need. (.) is quite a valid name. Nevertheless, this is fair. I
meant dot as an example (though one that might ultimately be chosen).
I like bang, myself; others seem to favour get. The trouble is, in the
latter case, that we'd need to change certain widely-used libraries...

> 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"

> The litmus test is 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;

> AntC

Cheers,
strake