Mode declarations only allow specifing ‘:’ for meta-arguments but meta_predicate/1 uses ‘:’ for module-sensitive arguments and 0…9 for predicates.
Is this difference an oversight, or is there something deeper? It would be nice if such comments could be used with a linter – I found a subtle bug using logtalk’s linter because I’d specified meta_predicate with 0 instead of 1.
Mode declarations (mode directives in the case of Logtalk) are indeed quite useful for some lint checks. A(nother) notable case is to provide more accurate steadfastness warnings by checking that variable aliasing in a clause head really happens in an output argument.
SWI-Prolog doesn’t have a mode/1 declaration. It might actually get that at some point. I’m not sure. It only specifies modes for documentation purposes in PlDoc. And yes, handling module sensitive arguments is rather limited. Even the statement that : implies + is generally not true. I’m happy to extend that if we can come up with a nice notation. Possibly p(0:Goal) would do for 0..9? Normally we have of Mode Var[:Type], but for 0…9 the type is always callable, so the ambiguity is ok.
In Logtalk, the information provided by its mode/2 directives is made available by the reflection API allowing any tools, such as lgtdoc, to retrieve and use it.
Btw, using predicate mode indicators in meta_predicate/1 directives is ambiguous. For example:
:- meta_predidate(forall(0,0)).
:- meta_predicate(bagof(?,0,?)).
In forall/2, 0 means @ but in bagof/3 0 means +.
Mode declarations are an abstraction. There is a lot more that can be said about arguments and which necessary for many analysis tasks. I think the first 0 of forall and the 0 of bagof are the same: they both enumerate all solutions of the argument. Forall uses negation over the second argument, something which you would like to know for tabling.
As for modes, I always have my doubts about the first argument of bagof and friends. This is a typical input argument that is not (well, temporary) bound by the goal. It can (and often is) a variable though. So, both +, ? and @ make (some) sense to me. I think the output should be - as it is a pure output argument. To me, - means it may be instantiated, but then it is the same as providing a variable and unifying. SWI-Prolog uses -- for things that should stricktly be a variable. Here are also two cases we do not distinguish: the predicate produces some handle we cannot predict (e.g., the open/3 stream) or the predicate is not steadfast. I would not always call the latter an error, in particular not for local helpers where you know the argument is always unbound.
Indeed. Still, I see mode directives/declarations as a step in the right direction that enables some progress.
Not from an argument instantiation perspective. I interpret your statement as coming from a meta-predicate perspective of what the arguments are used for. But there’s more to it as you mentioned above.
Only ? makes sense to me. + means that the argument must be bound, which is not true in general. @ means that the argument would not be (further) instantiated, which is also not true in general.
Fully agree that the ISO Prolog standard requirement of type-checking of output arguments is a questionable idea at best.
Accurate non-steadfast predicate detection requires predicate analysis that benefit from mode information. Still, I would not be surprised by false positive warnings to be generated for some cases. The current implementation in Logtalk of the steadfastness lint warning only looks for variable aliasing in clause heads with a cut in the clause body, which results in two many false positives (hence being turned off by default).