I assume the big picture here is the need for supporting parametric types? In the
error module, I find only
list(Type). But there are several others that are useful such as
char(CharSet), … As these as other parametric types are easy to add by the user itself (using the multifile predicates declared in the
error module), the question is if there’s enough demand to add them by default. In the case of Logtalk, the extensive list of types supported by default was motivated mainly by the QuickCheck support in
I assume the big picture here is the need for supporting parametric types? In the
I guess the big picture is that types are not settled for SWI-Prolog. The library(error) is mostly about throwing compliant errors in a comfortable way. That involves must_be/2, which is mostly about using a type test and if this fails throw a proper error. What constitutes a type is rather ad hoc in this library At some point we should have a proper notion of types and instantiation. There are a number of more established ways to declare types around. It is mostly a matter of reviewing these carefully, come to an agreement and implement type annotations. What we can/should do with them can be decided later and should IMO remain flexible. At some point I would like to see a type, mode and instantiation annotation that is easy to use and expressive enough. This doesn’t necessarily maen in can express everything.
I’m happy with Logtalk’s
mode/2 directives but open to discuss alternatives that could be implemented by several systems.
A few days ago, me, Anne, and Michael Ritcher were discussing a nasty case: how to write a
mode/2 directive (or the PlDoc equivalent) for a predicate that closes a difference list, converting it into a normal list? You may remember Paul’s blog post on difference lists, which prompted that discussion.
Internally we use something like that:
:- meta(NAME(TYPES1, TYPES2) is DET).
DET is one of erroneous, det, multi, failure, semidet, nondet
TYPES is either TYPE_IN/TYPE_OUT or one of the following shortcut:
T and +T are a synonym of T/T + is a synonym of nonvar/nonvar +T is a synonym of T/T - is a synonym of var/nonvar -T is a synonym of var/T
We use this also for meta predicates using types like e.g.
:- meta(my_pred(+det(+integer, -integer), -integer) is det).
For a predicate closing an open list we would use something like:
:- meta(ol_terminate(open_list(T)/invalid, -list(T)) is det).
A predicate can have more than one signature for different use patterns.
One of the issues with this is that it blurs the distinction between types and instantiation. var, nonvar and ground are not types. They indicate instantiation. In my view (which I think is the way most people in LP think about these issues) is that a single type is either a primitive type (integer, atom, …) or a compound with a given name/arity where the types of the arguments are specified. A complete type is a disjunction of single types. So, we can have e.g.,
:- type list(ElemType) --> [ElemType,list] | .
Typically there is a type like
any (paper) to indicate any term, including variables.
Now, a term can be of some type, which implies it is instantiated to something that satisfies the type (recursively) for all subterms that the type specifies. A term can also be compatible with a type. That means that everything that is instantiated satisfies the type, but not everything the type specifies need to be instantiated. A variable is compatible with any type. So,
- [a,b] is a list(atom)
- [_,c] is compatible with a list(atom)
- [a|_] is also compatible with a list(atom)
- [1,a] is not compatible with a list(atom).
Now, an input argument must be of a given type and an output argument must be compatible with a given type in entry and is of the same type on exit.
I once started a little playground that defines types as a constraint. If you apply a type on a term this can result in failure (error) of the term is not compatible with the type, a constraint on one or more of the variables in the term if the type is compatible or simply true if the term is of the given type. I still think that is a good starting point, also because constraints make reasoning about types easy.
In my experience to allow a (partially) instantiated argument where an output argument is expected leads to any kind of troubles and unexpected failures (as the determinism changes consequently).
This does not happen if signatures defines more strictly what is expected on enter/exit.
A trival example:
append(+list(T), +list(T), -list(T)) is det.
append(+list(T), -list(T), +list(T)) is semidet.
append(-list(T), +list(T), +list(T)) is semidet.
This would permit to reason on determinism and to know statically if some signature is incongruent with the implementation.
Quite similar indeed to Logtalk’s
mode/2 directives if we don’t take into account the TYPE_IN/TYPE_OUT notation:
meta instead of
mode and the atoms for the number of proofs are different but with same meaning.
Interesting. Thanks for the example.
Typically when you use partially instantiated output arguments you expect failure is an option. The nice thing is that the implementation can use this to optimize, i.e., “if the user is expecting this, I can quickly prove this will never happen instead of computing all possible results and matching them”. The SWI-Prolog RDF database as well as several builtins look at what should normally be considered output for this reason.
I also kind of dislike a rigid long description as you give for append above that still doesn’t cover quite useful applications such as
... append(_, [anchor,Y|_], List)
to find elements that follow some specific term. Many clean logical predicates can be used in similar ways and this is one of the aspects of Prolog that I appreciate.
Note that the list of description for append was not meant to be complete.
We might also have the following and others:
append(-list(T), partial(list(T)), +list(T)) is semidet.
My experience is that top enemies in Prolog programming are unexpected determinism (e.g. unexpected failure, unexpected choice points, etc.) and lack of type check.
I’m fine if someone want to continue to use append as
append(any, any, any) is nondet
or if another user is not interested that items have the same type, or whatever needs arise.
IMO the point is that type/mode annotations should allow to specify the constraints as strict/lax as needed.
In almost every Prolog program there are specific parts that should never fail, should never generate more than one result or aren’t prepared to receive any set of arguments (e.g. non-steadfast clauses) and the lack of possibility to ensure that with proper annotation is in my experience the hugest of the problems in Prolog programming (that otherwise is the greatest thing since sliced bread).
I agree with what you seek for the most part.
Just to clarify what you mean.
So your idea would mean there would, or would not be a separate language?
Note that in some case trace/2 can come handy. If you quickly want to verify something never fails you can use
?- trace(mypred, fail).
The 8.1.x series implementation of trace/1 is in Prolog and the implementation is a good basis for many runtime checks.
wrt steadfastness my approach is to make sure exported predicates are steadfast. Local helpers may not be.
It definitely would not be a separate language, but the same Prolog with optional type/mode annotations that help to statically check that expectations are respected.
We have no problems with dynamic/run-time checks: we have tons of assertions and determinism checks that are in place in development build and with an huge amount of tests this definitely help.
Nevertheless I can bet that a large amount of mistakes still remains hidden waiting only an opportunity to show themselves when you definitely don’t want
Click to expand
Towards Typed Prolog - See links under SWI-Prolog for related source code.
Small question (I need to understand what the discussion is about).
Given this program:
foo(X, Y) :- between(1, 3, X), Y is -X. bar(X) :- foo(x, X).
If we had types, should the compiler catch the problem? And should the compiler need explicit type annotations/declarations or should it find the problem on its own?
What if I had, in my code,
Is that a problem with the type or “domain”?
Yes. It can figure out that this results in a call between(1,3,x), which is a type error. And no, knowledge about the types for between/3 suffice and this should be provided by the system.
foo(-1, Y) case there is no error. You can only proof failure but to do so you need the semantics of between/3. A good checker probably should know more about the semantics of some built ins. The checks that are there now are generally based on observed common errors and after writing the check on how often it finds errors and how many alerts are false positives.
binary_tree(nil). binary_tree(t(_, L, R)) :- binary_tree(L), binary_tree(R). foo :- binary_tree(foo).
Is the compiler supposed to give me a type error?
The difference from the previous example is that the “type” would have to be inferred from the definition of
binary_tree/1, not from the use of a built-in or a type declaration.
While it is not noted in the title of the post, some of would also consider the modes as something that needs to go along with the types.
The current version already acts appropriate:
?- check. % Checking undefined predicates ... % Checking trivial failures ... Warning: The following goals fail because there are no matching clauses. Warning: binary_tree(foo), which is called from Warning: /ufs/wielemak/src/swipl-devel/linux/bt.pl:7:4: 1-st clause of foo/0 ...
While Jan gave a reply with regards to the error message, the problem I forsee with the above definition is that the two predicates are not tied together into a single type.
In Mercury (link) it would be
:- type tree(T) ---> leaf(T) ; branch(tree(T), T, tree(T)).
and Mercury is also using Polymorphic types with that type definition.