Proposal for simplified Vinyl

[jonsterling]

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:

• Remove el and special universe stuff: just do it all in f.
• Remove Implicit class as well as Elem and Subset GADTs.
• 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.
• Removes the validation type; I encourage users to use a well-maintained left-accumulating validation type such as validation by @tonymorris / @nkpart.

This should suffice to resolve #59 and #54. There may also be something interesting to be done here with regard to #58.

Still needing to be added:

• Probably some other stuff I blew away

[acowley]

Yay! This is awesome! A few comments from skimming the changes:

• Rec's comment is out of date
• Identity needs a Storable instance (should Thunk have one, too?)
• I'd like some comments in Lens (eg, rreplace, whose type doesn't say much). I know this isn't necessarily user-facing API, but I still think it'd be valuable.

[jonsterling]

Thank you @acowley! I agree on every point, and totally—one of Vinyl's weak points has always been documentation, so please do keep nagging me about places where we can improve it. Particularly in the lens module, the types basically mean nothing to the user since they're meant to just be compatible with grown-up lenses...

[noinia]

This looks very nice :)

I played around a bit with this in the context of composing closed universes (#58). See this gist. It seems that that is indeed possible, although you do need the TyFun's again to pass around partially applied type-famlies. Also, the way I modelled the assignment you need to specify the type for the record. I couldn't come up with a way around this, but I didn't think about it for too long. Maybe we can do something similar like the 'withUniverse' functions that we have in vinyl-0.4. Then one would think there is enough information to infer the rest of the type.

[jonsterling]

@noinia This is very interesting, thank you for taking the time to work up that example. When I have some more time, I'd like to look at it in more detail.

Is there anything that could be done to the proposed design to make your use-case any easier?

[cartazio]

I like this simplified approach, it has much better type inference in the case when you dont specify the type of the list parameter! https://github.com/cartazio/HetList/blob/master/HetList.hs is my WIP where i'm using a copy of that Rec plus a few other hlist variants to figure out a more general desugaring for overloaded list syntax

[tel]

Is this more-or-less how fields would work now?

data s ::: t = Key

name :: "name" ::: String
name = Key

(=:) :: KnownSymbol s => (s ::: t) -> t -> FieldRec '[ '(s, t) ]
s =: r = Field r :& RNil

flens :: (KnownSymbol s, '(s, t) ∈ rs) => s ::: t -> Lens' (FieldRec rs) t
flens s = flens' s . elField where
  flens' :: forall s t i rs . ('(s, t) ∈ rs)
         => s ::: t
         -> Lens' (FieldRec rs) (ElField '(s, t))
  flens' _ = rlens (Proxy :: Proxy '(s, t))
  elField :: KnownSymbol s => Lens' (ElField '(s, t)) t
  elField = lens (\(Field t) -> t) (\_ t -> Field t)

Or can it be done more simply?

[cartazio]

So the defn of ElField becomes

data ElField (field :: (Symbol, *)) where
   Field :: KnownSymbol s => t -> ElField '(s,t)

so its a GADT that basically existentials the the symbol choice? neat!

[tel]

I really like the lens-as-proof mechanism for both Elem and Subset.

[jonsterling]

@tel I'm pretty wiped out right now, but I think that the answer to your question is yes; though forgive me if I've got it wrong, since I have just spent a few hours writing Rust and I cannot think straight anymore.

As regards the lens-as-proof mechanism, thank you! I was very pleased when I came upon it; it provides meaning to the type classes, and it also suggested new interesting things to be done, such as editing a swath of a record at a time. Having computational content here gives a kind of meaning explanation to the assertion "rs is a subset of ss", namely "We know how to retrieve rs from a product of ss, and we know how to replace rs in a product of ss", etc.

@cartazio The existential is there to ensure that we still know the symbol choice at runtime. :)

[tel]

@jonsterling No worries! Get some rust—I mean rest!

I am playing around with implementing an arrowized FRP in the style of Sculthorpe's thesis using Vinyl instead of their more stylized signal vectors. The need for record subsets is pretty important and I was fiddling with implicit definitions where subset means that there's a reordering such that you can split the larger into the smaller and something else... which is really hairy.

I saw this lens-based approach and it hit me like lightning that you'd found the right way to do that!

[cartazio]

ooo

[noinia]

Wonderful :) I was using this branch already for some time. Seems to work well :)