DEV Community: Gavin Mendel-Gleason

Type and mode checking in prolog (part 2): mavis

Gavin Mendel-Gleason — Thu, 08 Aug 2019 00:00:00 +0000

As we discussed in Part 1 of this short series on types in prolog, prolog has a rather graceful but silent method of reacting to a certain bugs. The exploitation of non-determinism can be extremely handy for searching spaces, but sometimes we just didn’t mean what we wrote, and instead of silent failure we would like to see an error.

One way around this problem which we presented in Part 1 was to use Hindley-Milner type (HM) checking to statically discover where we have variables which have a different type than we expect.

We’re going to take a different tack in this article and use dynamic type and mode checking with mavis. HM is great, but it wasn’t really written for prolog but for functional languages, and so doesn’t take any account of modes. It can also be a bit restrictive and heavy weight when modifying already existing code. We could of course dial it up, by introducing dependent types, but we’re not going to go there in this series (though how cool would this be?!).

With Mavis we get to specify both modes and quite complex types in a gradual fashion, adding them as necessary. The downside is that type checking happens only at run-time and is not statically checked. Unfortunately this means we only catch bugs during testing or deployment, but at least we catch them!

I’ve used both techniques in production code and find them both useful, but currently Mavis is more fully featured and more flexible and so I’ve done most development with it.

What is a mode? Prolog is a language of predicates, and we can think of any given substitution of variables as being either true or false at a predicate. But often times what we are actually doing when programming in prolog is taking what we know about some bound variables, in order to find other ones which would also satisfy the predicate. And very often we mean a predicate to only search for bindings given some set of already instantiated variables.

Take for instance the following programme:

/**
 * zip(+A:list(any),+B:list(any),-C:list(any)) is det.
 * zip(-A:list(any),-B:list(any),+C:list(any)) is det.
 *
 * Zip two lists into a list of pairs (or unzip, in the other two
 * modes)
 */
zip([A|RestA],[B|RestB],[(A-B)|Zip]) :-
  zip(RestA,RestB,Zip).
zip([],[],[]).

The benefit of this declaration is obvious from the results of querying for the following goal:

?- zip([1,2,3],a,C).
ERROR: Unhandled exception: The term a is not in the domain list(any)

We have effectively stopped zip from silently failing in the event of passing nonsense arguments. But what do all of these complicated mode descriptions mean?

There are two mode-lines given for the above programme. We use a preceding ‘+’ to denote required arguments and ‘-’ to denote supplied arguments. If an argument is required (‘+’), it must be bound at the time the predicate is called. If it is supplied (‘-’), it can be bound or not, but we will guarantee that we supply a binding if it is unbound.

In fact binding time status is a bit more complicated than this. It’s quite possible to have a ‘skeleton’ which has unbound variables inside of a defined term. For instance, you can obtain such a skeleton of a list with the goal:

?- length(L,3).
L = [_6186, _6192, _6198].

Is this +? Mavis interprets it as bound if it is compatible with the type declaration. To require a completely defined input you can use ++. In the future we want to include more specific user-defined designations modeling ourselves after those given in Mercury.

The final part of the mode describes the amount of determinism that the predicate is expected to have. Zip above is considered to be ‘det’ which means in all the modes that are described, and subject to its inputs being well typed, it will return precisely one substitution. The different determinism qualifiers are listed in the mavis documentation as follows:

failure: 0 solutions
semidet: 0 or 1 solution
det: 1 solution
multi: more than one solution
nondet: Any number of solutions including 0

There are allowable modes which are covered by the above given modes to make things a little more confusing. For instance, I can call zip with the following two different goals, both of which are accepted as legitimate and do not yield errors.

?- zip([1,2,3],[4,5,6],[1–4, 2–5, 3–6]).
true.
?- zip([1,2,3],[4,5,6],[1–4, 2–5, 3–7]).
false.

In the first case we supplied all of the arguments. This is more informative than any of the modes given, and consequently causes the determinsm to be demoted. We shift from being ‘det’ to being ‘semidet’. This demotion is taken care of for us automatically by mavis.We can also run the query backwards, since we have supplied the appropriate mode line above. This is the main reason we might want to specify multiple mode lines.

?- zip(A,B,[1–4, 2–5, 3–6]).
A = [1, 2, 3],
B = [4, 5, 6].

Mavis is really useful for finding bugs in production code during testing. I’ve recovered a large number of confusions, especially in the case of errors in my own thinking regards the determinism of various predicates. This can in turn have huge impacts on performance, since uncontrolled and unintended non-determinism can have surprisingly large impacts on speed.

There are however a number of things I’m unhappy with and I would like to see improved. I’ll list them out here as a sort of wish-list for mavis in the future.

There should be a good deal more that is done statically. Many of the mode and type declarations give plenty of information to yield compile time errors.
With a bit more declarative work we could even reordered queries automatically to produce much more desirable outcomes for specific modes — and in some cases we could even improve the termination behaviour!
The types should at least give us the flexibility of Hindley-Milner type declarations with free type variables which can be used repeatedly. This would give us a much more pleasing and specific type for ‘zip’.
Someday in the not too distant future it would be nice to see dependent types making their way in. For the dynamic case, as we currently have with mavis, this shouldn’t even be too terribly hard to implement in a hacky sort of way!

You can check out the lastest Mavis source here: https://github.com/GavinMendelGleason/mavis

Prolog meta-interpretation for syntax checking

Gavin Mendel-Gleason — Tue, 11 Jun 2019 00:00:00 +0000

Prolog is a fantastic toolkit for developing Domain Specific Languages (DSLs). Lexing and parsing are a breeze with the use of Declarative Clause Grammars (DCGs), and writing a interpreter or compiler is an essentially rule-based transformation problem anyhow.

But before we set about interpreting or compiling an expression, we need to know that a term, represented as an abstract syntax tree (AST) is well formed.

Writing a predicate which admits only those terms which conform to a given syntax is likewise very convenient in prolog. For instance, if we wanted to write down a predicate that checks the well-formedness of integer bearing lists, we might write it as follows:

isa_int_list([]).
isa_int_list([H|T]) :-
    isa_integer(H),
    isa_int_list(T).

When we undertake to use this predicate, we can certainly tell if a (already ground) list is well-formed. However, if it is not well formed, we are not given an enormous amount of feedback. We are instead entreated to the singularly uninformative result:

?- isa_int_list([1,2,x]).
false.

Well, we know it’s not an integer list, and given that we have an incredibly simple syntax, we can spot right away with the naked eye, the problem with the term. However, if the term is large, and the syntax is complex, returning false will not necessarily enlighten us to the source of the problem.

In the past I’ve dealt with this problem by writing relatively complicated syntax checkers, which throw errors when terms are known to be ill-formed, or keep track of failures to report to the top level.

This unfortunately defeats the clear expressive rule based qualities of the above code which neatly captures what we mean when we say that we have a list of integers. It both complicates the code, and increases the probability that you’ll not even express the intended conditions in the predicate.

Enter the metainterpreter

This is where metainterpretation comes to the rescue. Metainterpretation is a strategy for implementing custom interpretation of terms in prolog, using the fact that prolog is homoiconic and we can easily appropriate functionality from the host system. For an overview of metainterpretation, it’s worth reading Markus Triska’s examples here, or looking at the relevant section in The Art of Prolog.

Instead of writing a new predicate, we can reuse our predicate coupled with a metainterpreter which assumes a number of things about the predicate in question. We demand that the predicate be deterministic, i.e. it succeed in assigning the term to our accepted class in precisely one way. This is similar to the constraint that most type systems use to simplify checking and inference. We also demand that it draw from a relatively small number of primitive predicates and avoid cuts or other impurities.

You can look at the code here: https://github.com/GavinMendelGleason/typo

Our metainterpreter will then execute the predicate, bit by bit, and return none in the event that there is no error , and just (Error) in the case that something has gone wrong. The Error will carry with it all the information about all failed approaches to accepting the term. With this in hand, we can either look at the full failure tree, or we can use the quite effective heuristic, that the deepest failure is likely to be the one that almost succeeded. We can do this by calling deepest /2 to give us back the longest error stack. We can then print this stack with write_stack /1.

So what happens when we try our initial example with our metainterpreter?

-? metainterpret(isa_int_list([1,2,x]), ME),
   ( ME = just(E)
   -> deepest(E,S), write_stack(S)
   ; true).
x is not an integer
Left conjuct fails: isa_integer(x)
No successful clause for predicate isa_int_list([x])
Right conjuct fails: isa_int_list([x])
No successful clause for predicate isa_int_list([2,x])
Right conjuct fails: isa_int_list([2,x])
No successful clause for predicate isa_int_list([1,2,x])

Instead of false, we’ve found the most likely cause of failure, and the entire path up the syntax tree which resulted in the cascading failure!

Of course the reporting can be done differently, and the heuristic might vary with different uses, but I’ve found this an effective way of describing what has gone wrong. I’ve even found a bug in production code which was exposed when applying the metainterpreter as it tracked down an inadvertent non-determinism!

The take-away lesson for me was that sometimes its better to write a simple metainterpreter than it is to complicate your code. DSLs in prolog are easy to write and you can even write DSLs to help you write your DSLs.

Sometimes meta is betta!

Acknowledgments to Douglas R. Miles, who helped me sort out module manipulation issues.

Type and mode checking in prolog (part 1): type_check

Gavin Mendel-Gleason — Fri, 07 Jun 2019 00:00:00 +0000

When it comes to languages for rule processing, prolog has them all beat. It has so many exciting features that make it incredibly flexible, among them:

backtracking: we can try several strategies to solve a problem, and roll back if one doesn’t work. This also give us generators and testors using the same framework, enabling guess and check approaches to algorithms.
homoiconicity: which enables incredible metalogical madness including term and goal expansion and simplifying the writing of meta-interpreters.
DCGs (Declarative Clause Grammars): regexps are great, but when your language isn’t regular, DCGs give us one of the nicest ways to parse input around.

Yet when trying to write large software packages in anger for industrial purposes, there are some unfortunate warts that tend to plague this otherwise beautiful language. I’ve compiled a fairly long mental list, but right now I want to talk about two of these awkward elements and what to do about them.

When you write a predicate in prolog, you can often make a very efficient choice between clauses in the predicate by carefully choosing terms which enable us to discriminate between the clauses we would like to “fire”.

p(term_a) :- write(term_a).
p(term_b) :- write(term_b).

When we invoke p(term_a) we are graciously treated to the expected printout. And perhaps even better we, with a prolog such as swipl, we don’t even end up with any remaining choice-points due to the indexing of the argument, making our choice efficient as well.

However, in large scale projects, it can happen that we call p /1 with something quite unexpected, perhaps with term_c, due either to a typo, or a thought-o. Prolog’s method of dealing with this is to silently fail — and since failure in prolog is a normal course of events, the result can lead to irritating bug-searches which take quite a while to narrow the problem to its source.

Of course what we want for p /1 is to correctly type it. That is, we want to be able to add some additional information to p about the domain of its arguments such that we can dynamically, or even better, statically, determine that they are not of the required variety.

Hindley Milner and type_check

Enter Hindley-Milner (HM), a type system which allows us to write down just the sort of thing we’re concerned about when we call p /1. HM has a great number of advantages, allowing both inference of types in many cases, and the ability to write down our types in a nice algebraic fashion. It also includes many extensions which might be convenient in the case of prolog.

So how does HM work? Thanks to the work of Tom Schrijvers et al. we can try it out with the swipl package ‘type-check’. For our p above we can now write the following:

:- use_module(library(type_check)).
:- type term ---> term_a ; term_b.
:- pred p(term).
p(term_a) :- write(term_a).
p(term_b) :- write(term_b).

Here we add a type ‘term’ which is term_a, or (represented by the ‘;’) a term_b. We can now declare the arguments of our predicate p with a ‘pred’ declaration.

Now when we load our file, ‘type_check’ will attempt to find any type errors present in the code.

The first result of loading this file is the following message:

% TYPE WARNING: call to unknown predicate `write(term_a)'
% Possible Fixes: - add type annotation `::' to call
% - replace with call to other predicate
... :-
    'HERE'(write(term_a)).
% TYPE WARNING: call to unknown predicate `write(term_b)'
% Possible Fixes: - add type annotation `::' to call
% - replace with call to other predicate
... :-
    'HERE'(write(term_b)).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Type checking for module `first_blog' done:
% found type errors in 0 out of 2 clauses.
% Well-typed code can't go wrong!
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

Essentially our type-checker is telling us that it doesn’t know anything about write /1. Unfortunately the majority of standard ISO prolog is unknown to type-check. To really make it work properly for building software in the large we would need to add type annotations to our library. However, we have three different work-arounds provided by ‘type-check’.

The first two work-arounds I’ll demonstrate in tandem.

:- pred p(term).
p(term_a) :- write(term_a) :: write(any).
p(term_b) :- write(term_b) :< write(any).

Here we add type annotations to the code to inform the type checker that it can assume the type of the arguments of write /1 to be of type ‘any’. Both of these annotations appear to achieve the same outcome, however the former adds an additional wrapper to the call, ensuring that the arguments are actually of the appropriate type dynamically. The second is nothing more than a “trust-me” style hint to the type checker.

Similarly we can build up a database of trust-me style hints using the following syntax:

:- trust_pred write(any).

We can imagine how this could be extended to much of the standard library, for instance:

:- trust_pred append(list(T),list(T),list(T)).

This establishes that any call with append is to be treated as though it takes a list of some unknown type, another list of that same unknown type, and returns an output list of that type.

Given we have used one of these methods to properly type our predicate p, we can look at what type_check reports when we utilise p wrongly.

:- use_module(library(type_check)).
:- type term ---> term_a ; term_b.
:- pred p(term).
p(term_a) :- write(term_a) :: write(any).
p(term_b) :- write(term_b) :: write(any).
:- pred q.
q :- p(term_c).

The predicate q /0 is where we have inserted our buggy call. And indeed, type_check reports:

TYPE ERROR: expected type `unknown_type' for term `term_c'
            inferred type `term'
 in goal:
   p(term_c)
 in clause:
q :-
    'HERE'(p(term_c)).

Well, type_check has shown us our error, and we can now correct our bug at compile time rather than having to wait until we see the error in production.

Typing in the real world

This is really great, but there are some caveats. The type_check library really needs to have a few kinks ironed out for it to work in industrial practice.

The first thing is that the full standard library needs to be given appropriate typing in a library, so that you don’t have to constantly run around typing everything. And in order to do this, type_check needs to be made module aware, which it currently is not. Module-awareness adds a good deal of complexity as well — how do we import types for instance?

Second, the addition of dynamic checks at boundaries is absolutely fantastic, and precisely the right way to ease a language like prolog into using static typing disciplines. However, when should we apply these type checks? This leads us to the question of mode checking. We will look at dynamic type checking and dynamic mode checking in the next article on mavis.