Version 3 (modified by 6 years ago) (diff) | ,
---|

# 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`

, ....