On 07/20/2014 05:52 AM, Sergey Mironov wrote:
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.
Right. I do believe your original code can be elaborated with type annotations into a type-correct program, but the Ur/Web type inference engine isn't smart enough to do it. One minor issue is that the type of [main] was genuinely ambiguous, but adding a [: transaction page] annotation there resolves the ambiguity.
It turns out that turning the second [r] reference into a [useMore r] gets us to a type-inferrable program, but I think that's just a fluke. Basically, type inference for Ur/Web is undecidable, and we should be happy that this small change is enough to get everything to work. ;)
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)] ?
The [use] parameter describes the environment of previously defined form fields, which determines the expected types of any <submit> handlers. Your alternative [join] operator doesn't quite make sense from that perspective.
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 [] == [] ++ [] ?
Type inference is getting especially confused by your polymorphic type parameters for [inp] and [frm]. Removing them and hardcoding those type indices as [[]], I get a different error message about the occurs check failing, and it makes sense that it would fail. C'est la vie. Undecidable type inference, etc. ;)
Regards, Sergey 2014-07-19 22:49 GMT+04:00 Sergey Mironov <[email protected]>: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.
_______________________________________________ Ur mailing list [email protected] http://www.impredicative.com/cgi-bin/mailman/listinfo/ur
