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 pair(KeyType,ValueType), ground(Type), 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 lgtunit.
2 Likes
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.
1 Like
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.
1 Like
Quite similar indeed to Logtalk’s mode/2 directives if we don’t take into account the TYPE_IN/TYPE_OUT notation:
https://logtalk.org/manuals/userman/predicates.html#mode-directive
You use meta instead of mode and the atoms for the number of proofs are different but with same meaning.
Interesting. Thanks for the example.
Same.
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.
2 Likes
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.
My dream is that modern Prolog will have an evolution similar to what is happened to javascript with the adoption of typescript, i.e. a system of type/mode annotations that can be used to statically reduce in an incremental way the possibility that the unexpected happens while still allowing to write as we are used to when we want or need that.
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).
4 Likes
I agree with what you seek for the most part.
Just to clarify what you mean.
When I read that, I see typescript as a separate language from javascript and that typescript compiles to javascript.
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.
1 Like
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.
2 Likes
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 
1 Like
Useful links
Click to expand
Papers:
Towards Typed Prolog - See links under SWI-Prolog for related source code.
SWI-Prolog:
library(errors)
package type_check - Link to code is dead.
However for Pack type_check – prolog/type_check.pl clicking 
links to code
package typedef
Mercury:
The Mercury Language Reference Manual - Chapter 3 - Types
Discriminated unions
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,
foo(-1, Y)
Is that a problem with the type or “domain”?
1 Like
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.
For the 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.
1 Like
How about:
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.
As noted:
The programming language Mercury is being used for some of the examples and why I have added it in the post with links.
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.