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.

_______________________________________________
Ur mailing list
[email protected]
http://www.impredicative.com/cgi-bin/mailman/listinfo/ur

Reply via email to