Export a general "Attr" for use with closed universes?

[ocharles]

We have ElField, but that works with a huge universe - namely, anything that is a KnownSymbol. The tutorial hints at a way to work with smaller universes, but has to define (=::) and Attr itself. I think these can be exported by vinyl, reducing the amount of boiler plate users have to write:

newtype Attr (f :: TyFun k * -> *) (attr :: k) =
  Attr {unAttr :: Apply f attr}

(=::) :: sing t -> Apply f t -> Attr f t
_ =:: v = Attr v

This is using Apply from singletons, so I suppose you might have to incur that as a dependency - but maybe it can be defined locally. The idea is to write an interpretation type family as normal, and then generate defunctionalisation symbols from that type family in order to use with Apply.

The tutorial then becomes:

Let’s define a universe of fields which we want to use:

data Fields = Name | Age | Sleeping | Master deriving Show
type LifeForm = [Name, Age, Sleeping]

type family ElF (f :: Fields) :: * where
  ElF Name = String
  ElF Age = Int
  ElF Sleeping = Bool
  ElF Master = Rec Attr LifeForm

genSingletons [ ''Fields ]
genDefunSymbols [''ElF]

Now, let’s try to make an entity that represents a man:

jon :: Rec (Attr ElFTypeSym0) LifeForm
jon = (SName =:: "jon")
   :& (SAge =:: 23)
   :& (SSleeping =:: False)
   :& RNil

The only downside is that jon now needs a type annotation, because we can't infer what defunctionalisation symbol to use with Apply.

Thinking out loud, feel free to close this if it's outside the scope of vinyl itself.

[acowley]

Avoiding the singletons dep would be good, but the part that reads the worst to me is having to mention ElfTypeSym0. We would have to improve that, either by not providing the TH to generate it, or having a more rigid and predictable name generation mechanism (eg changing the splice generating function to something like genTypeSymbol and dropping the numeric suffix of the result).