Types with SWI-Prolog

Split Topic
10

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
11

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?

12

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
13

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
14

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 :smile:

1 Like
15

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 image links to code
package typedef

Mercury:
The Mercury Language Reference Manual - Chapter 3 - Types
Discriminated unions

16

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
17

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
18

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.

19

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.

20

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
...
21

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.

22
  1. I didn’t know about check/0. Thank you for pointing it out.
  2. It seems too easy to fool it. Or maybe I am missing something?
binary_tree(nil).
binary_tree(t(_, L, R)) :-
    binary_tree(L),
    binary_tree(R).

foo(X) :-
    binary_tree(X).

bar :-
    foo(foo).

The step itself does say “Checking trivial failures” so maybe this isn’t considered “trivial”?

I still would like to know, however, is this a type error or is it another kind of error?

23

I guess that if you define a type for binary_tree/1, it becomes a type error. I merely wanted to point out there are ways to proof a call makes little sense that does not really involve typing. And yes, the check just checks concrete goals and verifies there is at least one clause that may match. Tools like these do not proof the program is correct (which is in general impossible anyway), but they do proof that the program shows behaviour that is most likely not intended. The compiler also complains on e.g., X == Y if one of the variables is a fresh variable and the goal thus always fails. This isn’t wrong, just most likely not intended. If you want to fail, use fail/0 :slight_smile:

24

Hi Jan,

since “Prolog with Types” seems to be a broad topic with many (incompatible?) views, I was just trying to get a feel of what you and others consider to be the scope of the discussion.

I am sorry I am not using well-established terminology. I didn’t want to provide undeniable proof that I don’t really know what I’m talking about.

I would like to have a typed Prolog. I suspect one can do a lot at compile time without adding any annotations or declarations.

Something I have observed is that “Prolog with Types” discussions go into topics like determinism and modes. My impression so far is that “simple” compile-time type inferrence doesn’t need to address these issues in order to bring value.

I hope I am making sense.

EDIT: it seems that the package by Tom Schrijvers comes closest to what I mean.

25

The work by Tom is in the end exactly what I do not want. He designed a type system that proofs type consistency. The price that you have to pay are a lot of annotations to give the reasoner enough material as well as explicit indications that some goal should not be type checked. This type system can also deal poorly with type overloading (handle multiple types in one predicate). This (in my view) results in a de-facto different language.

I want static analysis that finds likely wrong programs with as little as possible user annotations and allowing the user to write Prolog the way s/he likes. If you want to allow for type overloading you’ll have to track the control flow for arguments of different types. Modes and determinism is, at least when I was thinking about this, indispensable. It is simplest form, you must know that atom/1 lets an atom pass and blocks anything else. You also need to realise that atom/1 followed by a ! implies that subsequent clauses won’t see an atom. And yes, such a system can not say “your program is free of XYZ errors”, but as long as it cannot say “your program is correct” I only care that it points at as many as possible errors.

Ciao is definitely the most advanced in this area. Although I never really used their assertion language, I think it got too complicated and typically too slow to be of real practical value. That is why Edison came up with a simplied runtime checking system based on the Ciao assertion language that proved (for him) more practical.

Possibly the sweat sugar doesn’t exist. On the other hand I’m quite sure it is possible to write rather simple tools that will point at a lot of dubious code. Typing is merely one target though.

2 Likes
26

Inspired by watching some youtube lectures by Barbara Liskov on her type hierarchy theory (which I find much more useful than OOP) I put together the following diagram of what I consider to be Prolog supertypes and subtypes.

The next step is to gather the predicates related to each.

any
├── atomic ; constant
│   ├── number
│   │   ├── integer
│   │   │   ├── nonneg            % Integer >= 0 
│   │   │   ├── positive_integer  % Integer > 0 
│   │   │   ├── negative_integer  % Integer < 0
│   │   │   └── between(U, L)     % Integer >= L, Integer =< U 
│   │   └── float
│   │       ├── rational          % includes integers
│   │       └── between(U, L)     % Float >= L, Float =< U 
│   ├── text
│   │   ├── atom 
│   │   │   ├── symbol            % with or without single quotes
│   │   │   ├── char              % Atom of length 1
│   │   │   ├── code              % Unicode point
│   │   │   └── blob
│   │   │       └── stream 
│   │   └── string                % double or single quoted
│   └── boolean 
└── compound
    ├── callable                  % Can also be functor/0 symbol
    ├── list ; proper_list
    │   ├── list_or_partial_list
    │   ├── list(Type)
    │   ├── chars
    │   └── codes
    ├── tree ; graph            % Not defined as a formal type
    │   ├── cyclic
    │   └── acyclic
    └── dict

I’ve edited the above diagram to remove var after reading @Jan’s comment above:

One of the issues with this is that it blurs the distinction between types and instantiation . var , nonvar and ground are not types.

What this little exercise made me think is that using the documentation for must_be/2 leads to a very silly type system because important things missing here are collections like set, queue etc.

1 Like
27

Can you provide a link(s). While I do find some of her videos on YouTube, I can’t seem to find the one(s) on type hierarchy theory. :smiley:

28

Her academic paper is at https://www.cs.cmu.edu/~wing/publications/LiskovWing94.pdf (I must confess I haven’t read it very far).

One of her talks is at https://www.youtube.com/watch?v=GDVAHA0oyJU which covers a lot of ground besides her work on abstract data types.

I generally find she is a brilliant communicator who covers problems I’ve encountered. I regard op/3 as harmful as goto, so it’s nice to hear a Turing award winner articulating clearly why “extensibility” is an awful idea because it encourages unreadable code.

Some other talks on youtube by her are at https://www.youtube.com/watch?v=qAKrMdUycb8&t=3717s and https://www.youtube.com/watch?v=_jTc1BTFdIo.

1 Like
30

Personally I do not see them as missing. Most programming languages, especially the popular Object Oriented ones have collections but the languages are also not split into many variants so if there is only one official version of the language then adding to it becomes the standard. Prolog has variants such as SWI-Prolog, SICStus, GNU Prolog, ECLiPSe, YAP Prolog, and Prolog has the standard definition, which does not define collections, as such they would not be in the base definition of types.

What might be better would be if each add-on/plug-in that used certain types added some has_type/2 predicates, but then again has_type/2 is not in the standard, so each variation of Prolog may or may not have it.

The real problem is that Prolog is such and old language that is still used today, that it did not evolve along the same lines as other languages.

The other way I look at the whole typing thing is that Prolog is not a programming language for solving problems directly, instead Prolog is used to create an intermediate language, and that language is used to solve the problem. I think of Prolog as having an indicator

image
image.jpg734×720 108 KB

that on one end points to fully deterministic code, and at the other end points to pure code.

The more deterministic the code is, the more type checking is needed. The more pure the code the less type checking is needed, and in pure code, AFAIK, there should be no type checking because the code should be fully abstract. Also as you move from deterministic to pure, the arguments move from being either strictly input or output to being both.

The reason I think you don’t see Prolog talked about in this way is because most people don’t think of it like that and there is no line between the code used for solving the problem and the code used for creating the language to solve the problem.

Make sense. :smiley:

I added the image to give some idea of what I am thinking, but I don’t like the colors on the indicator, words such as deterministic, semi-deterministic and pure should be used instead.

Your changes and notes have me rethinking about how I think of has_type/2 and now I am starting to think of it more like Hoare logic instead of typing rules.

2 Likes