[Ur] Polymorphic variants and JSON

[Edward Z. Yang]

OK, totally in over my head with metaprogramming.

It might be helpful for me to articulate some of the problems
I'm having.

    1. I can't tell what arguments are implicit and which are explicit.
       My first intuition is that things with triple colons are implicit,
       but it turns out Urweb can infer a bit more than I thought, and
       I have a really hard time judging it.  For example, I think I
       want to use Variant.destrR. Which arguments do I need to pass
       it, which do I not?  The rampant use of un-inferred application (@)
       makes that harder.

    2. As a relative novice to metaprogramming in general, my understanding is
       definitions tend to be hard to read and write, but easy to use (this is in
       contrast to value level computation, where looking at the body tells me
       basically what a function does.)  But there are no docs, usage or
       otherwise, for most of the combinators in the metaprogramming libraries.
       This impedes understanding.

    3. Each level of the type system (kinds, types, values) has its own
       syntax, and while this is not necessarily a bad thing it makes
       it a bit more complicated to assess what is what, being unfamiliar
       with the syntax.  The fact that the grammar given in the manual
       uses Unicode symbols and not ASCII symbols exacerbates the problem.
       (Do we have an ASCII grammar lying aruond somewhere?)

Now, for the particular problem I'm trying to figure out: I'm writing the
ToJson method for the json_variant typeclass:

    fun json_variant [ts ::: {Type}] (fl : folder ts) (jss : $(map json ts)) (names : $(map (fn _ => string) ts)) : json (variant ts) =

I am given a value of type (variant ts).  This variant has a string name associated
with it in names, and the inside json typeclass to call for the inner data in jss.
So what I would like to do is use variant to "destruct" jss and names, gaining
access to a string (the name of the variant) and the appropriate typeclass
object for the inner data, and access to the inside data of the
variant (with these two types unified appropriately.)

OK. What do I want? How do I start? Do I want destructR? It doesn't seem
to have quite the right signature.

Edward

Excerpts from Edward Z. Yang's message of Sat Apr 14 13:44:35 -0400 2012:
> Oh, never mind, I'm being silly.
> 
> If I understand the current json_record right now, it requires all of
> the fields to be present, so this is not so good for the style of encoding
> variants I described earlier.  So I'm going to see if I can modify
> json_record into a variant json_variant (haha I made a pun), which
> takes a type level record but requires only /one/ key to be present.
> Or maybe it'll just prefer the first one that shows up?
> 
> Edward
> 
> Excerpts from Adam Chlipala's message of Sat Apr 14 13:39:34 -0400 2012:
> > Edward Z. Yang wrote:
> > > I'm a little confused by the definition of json_record;
> > > why does it take a (fl : folder ts) as an argument, but then
> > > not use it for anything?
> > 
> > I think this question refers to 
> > http://hg.impredicative.com/meta/file/e7d64ea0f922/json.ur .
> > 
> > In the definition of [json_record] there, I see the argument [fl] used 
> > several times.
>