[Ur] Unification failure when duplicating result of a monadic XML generator

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.