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