[Ur] Polymorphic variants and JSON

[Adam Chlipala]

Edward Z. Yang wrote:
>      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.

Without any explicit overriding of implict-ness, the only implicit 
arguments are (a) constructor (type-level) arguments with [:::] in their 
type portions, (b) type class witnesses, and (c) folders.

> 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.

I _think_ the above explanation (which is also lurking somewhere in the 
manual) says exactly which arguments are required.  Note (also as 
explained in the manual) that [@] switches to explicit passing of type 
class witnesses and folders, but leaves constructor (i.e., type-level) 
arguments implicit.  You use [@@] to make all three categories explicit.

>      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.

To me, the types more or less explain what the functions must do, thanks 
to "theorems for free"!  And then the function names add a bit more of a 
nudge, in cases with some ambiguity.

Do you have a question about a particular function that I might be able 
to explain?

>      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?)

The closest thing to an ASCII grammar right now is src/urweb.lex and 
src/urweb.grm, unfortunately.  The list of ASCII-to-LaTeX mappings is 
pretty small, so I hope it doesn't take long to internalize, and then 
the grammar in the manual should be straightforward to interpret.

> 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.

All of the specific functions like those in [Variant] are defined in the 
end in terms of [fold], which comes from [Top], a module that is open by 
default in all Ur programs.  I think it's a nice down-the-rabbit-hole 
exercise to understand how to build up the tower of helpful functions, 
starting just from [fold]; but of course you will want to avoid that 
when possible. :)

It looks to me like, for the [ToJson] part, you would ideally use a 
close variation of [Variant.destrR].  In particular, you want a function 
that takes one variant and two records, instead of one variant and one 
record.  Does it make sense that this is the key missing piece?  Do you 
see how to implement it?  I think it can be done without any new folding 
by combining [Variant.destrR] and [map2] (from [Top], though you don't 
need to qualify it as such to use it).

For the [FromJson] direction, I don't see a direct match with an 
existing fold function.  Intuitively, you want to fold over [jss] and 
[names], building a function that checks if the current name is in the 
JSON record syntax, and, if so, uses the current element of [jss] to 
parse the data.  (This is all modulo character-level decomposition of 
the string, which can be done as demonstrated in [json_record], though 
it may be easier for variant encodings of fixed JSON record size.)  The 
folding over two records part can be done with [foldR2] from [Top], but 
I don't see a way to avoid some manual manipulation of variants without 
writing new code.  (Though I can see [Variant.weaken] being useful to 
support a simple choice of accumulator type in the fold.)

I believe knowledge of how to accomplish the above tasks will follow 
from an understanding of the types of the different fold-based 
functions, starting with the most basic [fold], so please fire away with 
questions about them!