VinylRecords/Vinyl — pull request #66 by jonsterling (2014-09-15 00:32:59+00:00)
Title: Proposal for simplified Vinyl

So I'd like to discuss simplifying Vinyl's type structure to have only two parameters: an interpretation functor `f :: u -> *` and a list of rows `rs :: [u]`.

The primary reason for having the `TyFun/$` stuff before was that I thought it was important to be able to express the interpretation of the universe as a function. Now, I am not so sure, after having had some experience encoding it with a plain GADT in some stuff at work. The other reason it was nice to have the interpretation `el` and the effect modality `f` separated was that it enabled some nice compositional behavior (the effect modality would never interfere with the interpreter, and so it prevented you from having to do some plumbing to, for instance, get a record which can be applied pointwise to another record with `<<*>>`, etc.).

But to be quite honest, the setup has never sat well with me, particularly when it is in some sense equivalent to one which is done with fewer parameters compositionally. In the past, I have never been able to quite figure out how to do this nicely, but it may be the case that I have gotten close enough now.

Some things now compose better (for instance, you can now transport records across natural transformations between universe interpreters!). Other things may compose slightly worse (it will take experience to see).

Changes in this pull request are:

- [x] Remove `el` and special universe stuff: just do it all in `f`.
- [x] Remove `Implicit` class as well as `Elem` and `Subset` GADTs.
- [x] Add (decidable!) type classes to replace `Elem` and `Subset`: the proofs are lenses. This is *really* cool, because not only do we have lenses into specific fields in a record, we actually have lenses into arbitrary (and possibly non-contiguous) slices of a record. And these *just work* without any type annotations in general.