[Ur] Polymorphic variants and JSON

Edward Z. Yang ezyang at MIT.EDU
Sat Apr 14 18:18:15 EDT 2012


Excerpts from Adam Chlipala's message of Sat Apr 14 17:29:39 -0400 2012:
> 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.

Aha, now I see this bit in the manual.  It's unfortunate that there's no
syntactic marker for type class witnesses and folders; while folders are easy
enough to identify (look for 'folder ts'), for any type class witness I need to
know if the 'json' in 'json a' is a type class or a regular type constructor,
in order to know if it's implicit.  (And even that's not enough, since
something like $(map json ts) counts as a typeclass witness too--so what is a
witness, anyway?)  But that clears things up a bit.

> To me, the types more or less explain what the functions must do, thanks 
> to "theorems for free"!

I wince a bit when types get to be several lines long.  :-)

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

Yeah, here is the ambiguity thing, since there exists a destr2R but
it doesn't have the right signature here.

map2 is useful.  With it, I get here:

    {ToJson = fn r => let val jsts = @map2 [json] [fn _ => string] [fn x => json x * string]
                                     (fn [t] (js : json t) (t : string) => (js, t)) fl jss names
                      in @Variant.destrR [ident] [fn x => json x * string]
                          (fn [p] (v : p) (js : json p, t : string) => "something") fl r jsts
                      end

I can't get this to unify:

    /home/ezyang/Dev/logitext/meta/json.ur:273:26-273:83: Unification failure
    Expression: 
    fn p ::: Type =>
     fn v : p =>
      fn $x : {1 : json p, 2 : string} =>
       case $x of {1 = js, 2 = t} => "something"
      Have con: 
    p ::: Type ->
     (p ->
       ({1 :
          {ToJson : (p -> string), 
            FromJson : (string -> {1 : p, 2 : string})}, 2 : Basis.string}
         -> Basis.string))
      Need con: 
    p :: Type ->
     (p ->
       ({1 :
          {ToJson : (p -> string), 
            FromJson : (string -> {1 : p, 2 : string})}, 2 : Basis.string}
         -> <UNIF:U1048::Type+1>))
    Differing constructor function explicitness
    Have: 
    p ::: Type ->
     (p ->
       ({1 :
          {ToJson : (p -> string), 
            FromJson : (string -> {1 : p, 2 : string})}, 2 : Basis.string}
         -> Basis.string))
    Need: 
    p :: Type ->
     (p ->
       ({1 :
          {ToJson : (p -> string), 
            FromJson : (string -> {1 : p, 2 : string})}, 2 : Basis.string}
         -> <UNIF:U1048::Type+1>))

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

OK.  I guess my first choice would have been to parse the JSON,
and then look at my type for the right jss (operationally speaking,
it's the most efficient), but maybe Urweb isn't dependent enough to
do that.  Certainly we make this easier by assuming that a variant
JSON will have only one field, so we parse it all out, and then
fold over [jss] looking for a match as opposed to a check.

But that seems basically clear enough.

Cheers,
Edward



More information about the Ur mailing list