| >> Explicit checking of the appropriate instantiations is something for more
or less official interfaces, not for every internal predicate. But there's no formal concept of "interface" in Prolog, and the module system
sucks (or doesn't exist, depending on implementation) and many programs don't
ever use it anyway, so instantiations errors are a possible issue at every
level of a program. For me at least it's a constant headache knowning how a
predicate must be called (hence my practice of documenting the structure of
inputs and outputs carefully). I really don't like the ad-hoc "type" checking in Prolog (as in integer/1
etc). Prolog doesn't have types, because pre-Church logic doesn't have types
(and post-Church logic is a mess; typed mess, but still a mess). And yet
Prolog terms (in the sense of a functor followed by comma-separated terms in
parentheses) are implicitly typed, under unification: T is the type of all
terms that unify with T. So making sure that terms are correctly instantiated
is the most prudent thing to do when checking the "type" of a term.
Unfortunately that adds too much clutter and I personally resent havng to do
it. I have seen various attempts to solve that conundrum over the years, for
example there's a package for SWI-Prolog that adds Hindley-Milner type
checking (brrr). I don't like any of them. It's a bit weird how that is the kind of thing that Prolog gets wrong that I
rarely hear as an actual criticism, as opposed to complaints about the cut, or
the imperfect declarative-ness. I guess all this would be solved in practice by the addition of a static type
system, checked at compile time, which would completely change the language of
course. Incidentally, I'm currently working on an ancient (30 years old)
Visual Prolog project; Visual Prolog is exactly that, a compiled Prolog with a
static type system. I feel that while it sure helps catch some errors, it
contrives to suck all the energy and life out of Prolog. Prolog is like
parcour: it lets you fly around town, jumping and rolling like Spiderman. So
sometimes you get a lamppost en plein dans la figure. So what. Who needs type
safety anyway? (She says while changing yet another bloody bandage) >> But you could save your beloved cut with minimal effort by using dif_si/2
(voir https://stackoverflow.com/a/20238931/772868) just before the cut. In
this manner you would get instantiation errors for exactly the cases you
cannot handle. Thanks for the pointer. I had a quick look. I think there's something similar
in SWI-Prolog's Picat-style matching with the "=>" operator that is an
alternative to ":-". I'm not sure exactly what it does (something about
"steadfastness", that you also mentioned, and that is a new term for me) but I
prefer to not use libraries that significantly change standard Prolog syntax,
for fear of backwards compatibility. |
Any predicate you write for someone else has an interface. Someone else includes you in a couple of weeks. All predicates that are not truly auxiliary ones which are more like basic blocks of command oriented programming languages - COPLs.
> instantiations errors are a possible issue at every level of a program
That is not the worst that can happen. Nor is non-termination the worst. The worst is if an unexpected failure or success happens that looks like a legitimate answer. However, for many, non-termination is seen as being worse than such real errors. The reason is that there are only very few Prolog systems that reliably catch resource errors or have reliable timeouts. Well, to be true, there is one system. And the others most often abort.
> (hence my practice of documenting the structure of inputs and outputs carefully).
> I really don't like the ad-hoc "type" checking in Prolog (as in integer/1 etc).
integer/1 is one of the orignal sins of DEC10 which remplaced the errors of Prolog I by silent failure. And everybody then followed suit. Mindlessly. There is library(si) that offers integer_si/1 to make things much cleaner.
As for your remarks on type systems for Prolog, one feature they do not provide is a dynamic conversion between regular Prolog and the typed part. There was an attempt some time ago but unfortunately the individual left for FP.
> Who needs type safety anyway?
It seems there are two different objectives: type safety and instantiation safety. Both are often confounded.
> SWI-Prolog's Picat-style matching with the "=>" operator that is an > alternative to ":-".
This approach does not distinguish between instantiation and type errors. Take the sum_list/2 from https://www.swi-prolog.org/pldoc/man?section=ssu
And then when adding the suggested catchall rule, both fail. Both. This throws us back by almost half a century. So now DEC10-style errors get into the 21st century. Prolog 0 and Prolog I were better. > "steadfastness", that you also mentioned, and that is a new term for meSince 1987-09-29 in common use, see the Prolog Digest of that date, posting by Richard O'Keefe. Here is my definition: an argument Ai is steadfast w.r.t. a goal g(A1,..Ai,..AN), when executing this goal is equivalent (complete operationally) to, g(A1,..CAi,..AN), CAi = Ai with CAi a fresh new variable. And more generally an argument Ai is steadfast, if this property holds for all goals.
A good example of a steadfast argument is the second argument of append/3. You can replace any goal append(Xs, Ys, Zs) by append(Xs, CYs, Zs), CYs = Ys without observable effect (except efficiency, resource consumption and the like). But even non-termination is preserved! Another one is the 3rd argument of phrase/3.
Or take your run_length_encoding/2/3, where the second argument is steadfast. You (presumably on purpose) accumulated in the second argument all the elements only to reverse them finally in a highly lispeling manner. At least no destructive nreverse.