# Type-Indexed Records

Proposal for new Haskell record system. Record selection is simple operator. Keys are arbitrary types. Scope is controlled as scope of key types.

# Basics

Type classes for types with member at 'k'

`class Has k v r where (.) :: r -> k -> v;`

which means that r has member of type v with key type k, and for types with mutable member at 'k'

`class (Has k u r, Has k v s) => Quasifunctor k u v r s where qfmap :: k -> (u -> v) -> r -> s;`

which means that r and s have members of types u and v, in turn, both with selector k; thus, one can mutate the member at 'k' with an arbitrary function of type u -> v, and the overall function is of type r -> s; i.e. one can lift a function of type u -> v to a function of type r -> s.

A record type is of the form

`type R a b c ... = { X ::. a, Y ::. b, Z ::. c, ... };`

which automatically generates

```
instance Has X a (R a b c ...);
instance Has Y b (R a b c ...);
instance Has Z c (R a b c ...);
...
instance Quasifunctor X a a' (R a b c ...) (R a' b c ...);
instance Quasifunctor Y b b' (R a b c ...) (R a b' c ...);
instance Quasifunctor Z c c' (R a b c ...) (R a b c' ...);
...
```

## Record selection and mutation

Let

```
type R a b c = { X ::. a, Y ::. b, Z ::. c, ... };
-- keys
data X = X;
data Y = Y;
data Z = Z;
```

Then `r.X :: a`

is the member of `r`

at `X`

, and `qfmap X f r`

is `r`

mutated by `f`

at `X`

; thus also for other keys `Y`

, `Z`

, ....
We might define some sugar for `qfmap`

.

We can define

```
x = X;
y = Y;
z = Z;
```

to allow `r.x`

, `r.y`

, `r.z`

, ....