[Ur] json implementation - need some help understanding what's happening here?

[Adam Chlipala]

Marc Weber wrote:
> val json_record : ts ::: {Type}     -- implicit. is automatically inferred
>      ->  folder ts                    -- first arg?
>      ->  $(map json ts)               -- second arg?
>      ->  $(map (fn _ =>  string) ts)   -- third arg?
>      ->  json $ts                     -- result type?
>    

This is just normal function type syntax, so the questions about 
"argument numbering" aren't particularly interesting.  (Your answers are 
correct.)

> 1) map json?
>    Now: What does "map json" exacly mean?

The built-in constructor function [map] applies a function to every 
field of a type-level record, constructing a new record based on the 
results.  It's really just like normal 'map' from functional programming.

> What does mapping over a class (json is a class?) do?
>    

In Ur, a class is just a type-level function, mapping the indices into 
the class internal implementation.  The answer to your question follows 
from that.  Alternatively, another way of putting it is that the 
constructor [map json ts] denotes a type-level record with a field for 
each entry of [ts], where each field contains a [json] instance for the 
appropriate type.

>    Is map described somewhere? It seems to be a primop because its listed
>    in the syntax files and in the lexer file.
>    

The manual gives a complete description of its syntax and semantics, 
though not necessarily in a form accessible to people without expertise 
in semantics.

>    That also seems to be the reason why map is called mp in all
>    remaining files (eg list.ur)
>    

Right.

> 2) number of arguments? I'm still totally missing the point. json_record
>      is used like this:
>
>          type address = {StreetAddress : string,
>                          City : string,
>                          State : string,
>                          PostalCode : string}
>
>
>          val json_address : json address = json_record {StreetAddress = "streetAddress",
>                                                         City = "city",
>                                                         State = "state",
>                                                         PostalCode = "postalCode"}
>      only one argument is passed - however json_record still has 3
>      explicit ones?
>
>        ->  folder ts                    -- first arg?
>        ->  $(map json ts)               -- second arg?
>        ->  $(map (fn _ =>  string) ts)   -- third arg?
>    

The first two are inferred, because they meet Ur's rules for being 
considered type class witnesses.  A folder is always a type class 
witness, and the second argument qualifies because it is a record of 
type class witnesses, which are considered to be witnesses themselves.

>      Which section of the manual do I have to understand so that I can
>      follow what ur is doing here?
>    

I'm not sure it's all documented, but the closest thing I see now is in 
Section 4.3, in the paragraph beginning "Handling of implicit."

> 3) is it possible to write a generic show function which does not
>     require json_record to be called for each possible record type?
>    

It's only possible if you don't want the output to depend on the record 
field names.  Ur provides no way to introspect on the syntax of field names.