[Ur] Unification failure when duplicating result of a monadic XML generator
Sergey Mironov
grrwlf at gmail.com
Sun Jul 20 05:52:01 EDT 2014
I've learned the situation a bit more, and now think that it is not a
bug, but a feature of the typesystem. Basis.join's definition says
that it's right fragment's type depends on it's left fragment's type:
use2 should be equal to (use1 ++ bind1) :
(from the manual:
val join : ctx ::: {Unit} → use 1 ::: {Type} → bind 1 ::: {Type} →
bind 2 ::: {Type} → [use 1 ∼ bind 1 ] ⇒ [bind 1 ∼ bind 2 ] ⇒
(*left fragment *) xml ctx use 1 bind 1 →
(* right fragment *) xml ctx (use 1 ++ bind 1 ) bind 2 →
(* the result*) xml ctx use 1 (bind 1 ++ bind 2 )
)
I feel that it is the key to understanding of the problem. But I still
can't figure out the exact meaning of the second parameter of [xml]
constructor, refered as 'use' above. What does it mean? Why we can't
define a symmetrical join with signature like [ xml ctx use1 bind1 ->
xml ctx use2 bind2 -> xml ctx (use1 ++ use2) (bind1 ++ bind2)] ?
And the second question: Why doesn't compiler accept the join call
which have empty use's and bind's? Shouldn't it figure out that [] ==
[] ++ [] ?
Regards,
Sergey
2014-07-19 22:49 GMT+04:00 Sergey Mironov <grrwlf at gmail.com>:
> Hi.
>
> Here is the issue I've faced recently. The code below failed to
> compile with 'Unification failure' (full text is below the program).
> Looks like a bug, please check!
> Sorry if it is a duplicate, quick search shows no matches for such a
> problem for me.
>
> Regards,
> Sergey
>
> --
>
> fun mkrow [o ::: {Unit}] [inp ::: {Type}] [frm ::: {Type}] [o ~
> [Table,Tr]] (x:xml (o++[Tr]) inp frm) :
> transaction (xml (o++[Table]) inp frm) =
> return <xml><tr>{x}</tr></xml>
>
> fun main {} =
> r <- mkrow (<xml><td>an item</td></xml>);
> return <xml>
> <head/>
> <body>
> <table>
> {r}
> {r} (* <--- LINE 26 *)
> </table>
> </body>
> </xml>
>
> --
> The error message:
>
>
> /home/grwlf/proj/urbugs/XML.ur:26:3: (to 27:8) Unification failure
> Expression:
> Basis.join [<UNIF:U232::{Unit}>] [<UNIF:U233::{Type}>] [[]]
> [<UNIF:U235::{Type}>]
> (Basis.cdata [<UNIF:U232::{Unit}>] [<UNIF:U233::{Type}>] "\n")
> (Basis.join [<UNIF:U232::{Unit}>] [<UNIF:U233::{Type}>] [[]]
> [<UNIF:U235::{Type}>]
> (Basis.cdata [<UNIF:U232::{Unit}>] [<UNIF:U233::{Type}>] " ")
> (Basis.join [<UNIF:U232::{Unit}>] [<UNIF:U233::{Type}>]
> [<UNIF:U235::{Type}>] [[]] r
> (Basis.join [<UNIF:U232::{Unit}>]
> [<UNIF:U233::{Type}> ++ <UNIF:U235::{Type}>] [[]] [[]]
> (Basis.cdata [<UNIF:U232::{Unit}>]
> [<UNIF:U233::{Type}> ++ <UNIF:U235::{Type}>] "\n")
> (Basis.cdata [<UNIF:U232::{Unit}>]
> [<UNIF:U233::{Type}> ++ <UNIF:U235::{Type}>] " "))))
> Have con:
> xml <UNIF:U232::{Unit}> <UNIF:U233::{Type}> <UNIF:U235::{Type}>
> Need con:
> xml <UNIF:U232::{Unit}> (<UNIF:U233::{Type}> ++ <UNIF:U235::{Type}>)
> <UNIF:U229::{Type}>
> Constructor occurs check failed
> Have: <UNIF:U233::{Type}>
> Need: <UNIF:U233::{Type}> ++ <UNIF:U235::{Type}>
>
> PS Removing line 26 a well as inserting [r2 <- mkrow (...);] followed
> by changing line 26 to [{r2}] brings program back to working.
More information about the Ur
mailing list