On 10/02/2013 08:41 AM, Adam Chlipala wrote:
On 10/02/2013 06:28 AM, Sergey Mironov wrote:
I attempted to declare xmlify like that:
fun xmlify
[ctx ::: {Unit}]
[t ::: {Type}]
(fl : folder (map (fn _ => xml ctx [] []) t))
(r : record (map (fn _ => xml ctx [] []) t))
: xml ctx [] [] =
@mapX [ident] [ctx]
(fn [nm ::_] [t ::_] [r ::_] [[nm]~r] x => x)
fl r
The [ident] above indicates the type-level identity function, which
doesn't mesh with the type you chose for [r], and which explains why
the compiler expects [x] to have type [t]. Instead of [ident], you
should write [fn _ => xml ctx [] []] again.
By the way, you'll probably find use of this function easier if you
change the kind of [t] to [{Unit}]. Since you're ignoring the types
stored inside [t] at present, type inference won't be able to
reconstruct them uniquely from context.
Oh, and to make that more concrete, if I replace [{Type}] with [{Unit}],
then your example works with one small type annotation to guide the
choice of [ctx]:
val all : xbody = xmlify { A = <xml><p>blabla</p></xml> , B =
<xml><p>zzz</p></xml> }
Without that change, undetermined unification variables remain.
_______________________________________________
Ur mailing list
[email protected]
http://www.impredicative.com/cgi-bin/mailman/listinfo/ur
