[Ur] Polymorphic variants and JSON

[Edward Z. Yang]

OK, this one is being fiddly:

   val (r, s') = @foldR2 [json] [fn _ => string] [fn ts => variant ts * string]
                  (fn [nm ::_] [t ::_] [rest ::_] [[nm] ~ rest] (j : json t) name' acc =>
                      if name = name' then
                          let
                              val (v, s') = j.FromJson s'
                          in
                              (make [nm] v, s')
                          end
                      else
                          let
                              val (v, s') = acc
                          in
                              (Variant.weaken v, s')
                          end)
                  (error <xml>Unknown JSON object field name {[name]}</xml>)
                  fl jss names

(Never mind the fact that this will always result in an error, I'm planning on fixing
that later).

This particular permutation gives me:

    /home/ezyang/Dev/logitext/meta/json.ur:300:55-300:69: Can't resolve type class instance
    Class constraint:  Top.folder[[Type]] rest

and I don't know how to spell the implicit arguments correctly or what
folder I should be giving it (it's /almost/ 'fl' except that the
entries in front need to be lopped off).  Is there a version of fold which
also gives me folders?

I've also tried holding the type of the variant to be 'ts' through the entire
fold, but then Urweb isn't smart enough to unify:

    Can't unify record constructors
       Have: 
    [#1 = Basis.variant (([nm = t]) ++ <UNIF:U1173::{Type}>), 
      #2 = Basis.string]
       Need:  [#1 = Basis.variant ts, #2 = Basis.string]
      Field:  #1
    Value 1:  Basis.variant (([nm = t]) ++ <UNIF:U1173::{Type}>)
    Value 2:  Basis.variant ts
    Can't unify record constructors
    Have:  <UNIF:U1173::{Type}> ++ [nm = t]
    Need:  ts

Edward

Excerpts from Adam Chlipala's message of Sat Apr 14 18:23:19 -0400 2012:
> Edward Z. Yang wrote:
> > (And even that's not enough, since something like $(map json ts) 
> > counts as a typeclass witness too--so what is a witness, anyway?)
> 
> Yes, records built by mapping over type classes are also witnesses. :)
> 
> > 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>))
> 
> I think this error message is actually pretty good!  In the expression 
> quoted, you need to change the binder of [p] to mark it as explicit, not 
> implicit.  The easy way to do that is to change [[p]] to [[p ::_]] (note 
> no space between [::] and [_]).