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 [_]).
_______________________________________________
Ur mailing list
[email protected]
http://www.impredicative.com/cgi-bin/mailman/listinfo/ur
