-
Notifications
You must be signed in to change notification settings - Fork 17
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
MapTest-058 map as function #28
Comments
Yes, I think you are right. |
If the test is wrong then Saxon is wrong, so I've raised a Saxon issue at https://saxonica.plan.io/issues/4692 |
@benibela Good hint. That's something that also needs to be fixed in BaseX. |
I'm puzzling a bit over the transitivity rules. A number of the rules in §2.5.6.2 contain the phrase "because of the transitivity rules", but are the transitivity rules explicit? We obviously expect that subtype(A,B) and subtype(B,C) implies subtype(A,C), but where is this stated? The "if and only if" at the start of §2.5.6.2 doesn't seem to leave much room for inferring the relationship by transitivity. Now, Equally, So I guess we should read rule 35 as "Ai is map(K, V), and Bi is function(xs:anyAtomicType) as V? (or, by the transitivity rules, if Bi is function(P) as W where subtype(P, xs:anyAtomicType) and subtype(V?, W)". |
Further thinking on this. It's true that |
See also w3c/qtspecs#14 which I have raised as an issue against the spec. |
The answer is in F&O, section 17.1: "A map can also be viewed as a function from keys to associated values. To achieve this, a map is also a function item. The function corresponding to the map has the signature function($key as xs:anyAtomicValue) as item()*." I've struggled with this as well. This rule is not in XP31, but probably should be.
No, only one.
The same.
I think this conclusion is correct, but only if R is taken as item()*. This makes sense, because a map can take any item as value, and any atomic type as key. It's irrelevant if the type of the map itself is more specific. The function signature is always the same. It follows that the test is invalid. Edit: rule 30 in XP31 says so much, note "is" in the sentence: "Ai is map(*) (or, because of the transitivity rules, any other map type), and Bi is function(xs:anyAtomicType) as item()*." |
Thanks Abel, for the reference to F&O. The statement you quote conflicts with XP31 §2.5.5.8 which says: "The function signature of a map matching type map(K, V), treated as a function, is function(xs:anyAtomicType) as V?. "; but it agrees with what I'm proposing in w3c/qtspecs#14. The test as written is incorrect, though, because $s(42) returns (), which is not permitted by the function signature, therefore the map cannot be an instance of this function type. |
Yes, I agree, I was too quick in saying it was valid, forgot the type arity, and meanwhile edited. |
Indeed, it conflicts with 2.5.5.8. The other rules in both specs seem correct though (specifically 2.5.6.2, item 30). |
Actually, I think I'm confused on the covariance of the return type. If the target type returns string (or int, or any other more specific type for that matter), surely that should be wrong? Meaning, I think the return type of the target function only matches if it's |
Conversely, this also means that the argument of the target function can be more specific. |
@michaelhkay, if I look at your fixes, it looks like you apply contravariance to both the argument and the return type, but only the argument type is contravariant. Just like other functions, the return type should be covariant. I think we're confusing function coercion (https://www.w3.org/TR/xpath-31/#id-function-coercion) with instance-of relations here, and as such, I think I've misunderstood part of the discussion. Re-reading 2.5.5.8 seems true after all (though confusing), as it mentions function-coercion as a potential surprise in the last example, and it explicitly states that a map "is a" Moreover, it has this example, where
In short, I think the rules for sequence type matching where the target is a function and the source is a map, are:
This does not apply where a function is expected as an argument to another function, in which case function coercion takes place, and the return type may be a different type, leading potentially to runtime type errors. Same is true, for instance, in XSLT with In OP's example, the function-coercion rules do not apply (3.12.1 of XQ31). This means that a type error should be raised. Going over the suggested changes in c77205f, I don't think these are all correct:
|
I am implementing this behavior and was puzzled over these test failures in the test suite: MapTest-059
MapTest-063
MapTest-064
MapTest-065
Turns out this behavior matches what @abelbraaksma said. So my reading of the spec is the same as the one by @abelbraaksma three years ago, which perhaps counts for something. |
In
And this as one of the
If this is to be read as:
then in my reading of the spec this should be |
Looking at MapTest-059:
I believe the result is true: informally, because you can call this map as a function supplying any Finding justification for this in the specs is more difficult, and there are some known problems with the 3.1 specs in this area. See for example qt4cg/qtspecs#18 . But I think the XPath 3.1 spec in §2.5.5.8 has the clear (and correct) statement: The function signature of a map matching type Note that this only depends on So the map in this example matches the type Rule 35 of XPath §2.5.6.2 also states that I think the same reasoning applies to the other examples, and the examples are correct. But you're right that it's a confusing area and there are some muddled statements in the specs (which we have tried to improve in 4.0.) Unfortunately you haven't really explained why you think the test results are wrong. If you can explain your chain of reasoning from the specs, that might help us to make further clarifications. |
3.11.2:
If
So the equivalent signature for the map function would be:
2.5.5.8 Map Test
That matches, given the above signature and contravariant argument types. Now we get to the tricky part:
This part I find hard to understand:
Then it mentions Then there's talk about the rules for function coercion, which essentially means that we can ignore the function type for the purposes of passing it into a function - only It then says that a type error will occur if you call I tried a different interpretation - given a
wouldn't hold anymore as contravariance would make K too strict; this rules state any function, say, It seems odd to have to derive the function return value from the map signature, but not the argument, which is I believe is your interpretation. If we interpret the spec this way, what does the |
True. It is odd. It happens because the map-as-a-function returns () rather than throwing a type error if you supply a key of "the wrong type".
That's an excellent point. This is a bug which is still present in the spec. What it should say is not
Function coercion muddies the waters. These tests use |
I have this question:
Nothing in the types states this map will always return a string or an empty sequence - that's deduced from its contents, but there's no type information that says so here, is there? We'd have to derive the type |
A map (like a sequence) does not have an intrinsic type: the result of the expression |
The history of this text (of which you are aware) is interesting: https://www.w3.org/Bugs/Public/show_bug.cgi?id=29586 It used to read:
This matches my current interpretation based on other evidence in the spec.
This follows: Then it said:
Notice the word Now it reads:
And that's the interpretation we're stumbling over. Consider this part of the spec in 3.1.5.3:
This seems to be consistent with the original text but not the new text, as this map matches It goes on to say:
which seems to lend weight to this interpretation, as |
Yes, there was a lot of debate about it because different parts of the specification were inconsistent and we brought them into line. |
While the change might have been useful for other reasons, I don't agree the specification has become more consistent with this change. A line like:
makes me conclude map has that signature, and not the signature |
You already said most of this earlier, but I needed to construct this reasoning for myself. Considering
You say it should evaluate to true by examining its contents, and I said false. In 2.5.5.7 Function Test it refers to the subtype relationship.
So what's the signature of a map? I constructed it as fixed based on other evidence in the spec like
which follows your line of argumentation. Now on how to implement it. In my implementation it would be tricky to derive the function signature from an arbitrary map - it would require logic that examines all the value sequence types and combines them into a new sequence type that unifies them all, logic that's not required elsewhere. Instead, we can interpret How should this be implemented? I will go into this next. |
We can interpret What map test? The
or
Let's examine
which evaluates to and
which evaluates to So it would appear we need to strip the This rule implies that empty sequences aren't allowed. We don't have a test for it (and we should), but in Saxon:
is also Here is MapTest-064:
which is And MapTest-066:
which is also Let's try
this evaluates to This leads to the following rules to turn a return value into a map test:
I'd feel more comfortable if I could construct this rule from the specification instead of from the test suite and Saxon's behavior, but I struggle to reason about this. |
MapTest-058 has
But the type of this map is
function(xs:anyAtomicType) as xs:string?
(2.5.6.2.35) which is notfunction(xs:anyAtomicType) as xs:string
The text was updated successfully, but these errors were encountered: