Let me answer all your messages at once here.

Okay, let me tell you more on Prolog and its implementations. But first disclaimer. I deeply understand mathematical logic and I deeply understand how Prolog should work and what hypothetically can be achieved in Prolog. I have master degree in mathematical logic. But I don’t know what features actual Prolog implementations have. In fact, I never actually wrote any programs in Prolog-like languages. Also, I really deeply understand CSM (computer science metanotation). Let’s begin with example. Here is one simple type system written as CSM:

Context free grammar (i. e. abstract syntax, i. e. BNF):

Terms: x, y ::= [x] | length(x) | 42
Types: t, u ::= int | arr(t)

Rules (i. e. Horn clauses):

----------------
|- 42 : int

|- x : arr(t)
----------------
|- length(x) : int

|- x : t
----------------
|- [x] : arr(t)

Note that [x] above means array with exactly one element: x. I. e. I cheated by describing one-element arrays only. :)

As easily can be seen, relation |- length([[42]]) : int is provable in CSM above.

Also note that in CSM above |- has no any sense without : and vice versa. I. e. |- x : t is simply atomic construct.

This was very simple example of CSM. If you didn’t understand it, then it will be very hard to understand anything below. Ask any questions if you want.

Okay, now let’s translate this CSM to Prolog. I will use Mercury ( https://mercurylang.org/ ). So, here we go:

% Comments start with "%"
% Note that this code will not compile yet, I will tell later how to compile it

% Here is head, you may ignore it:
 :- module hello.
 :- interface.
 :- import_module io.
 :- pred main(io::di, io::uo) is det.
:- implementation.

% Now grammar

:- type term % Terms
        ---> sing(term) % [x]
        ;    length(term) % length(x)
        ;    forty_two. % 42

% "type term" above is simply algebraic data type. It correspond to "enum Term { ... }" in Rust

:- type typ % Types % I used "typ" instead of "type", because "type" is Mercury keyword
        ---> int % int
        ;    arr(typ). % arr(t)

% Here we declare our type relation, i. e. "|- x : t", i. e. "x has type t"
:- pred has_type(term, typ). % |- x : t

% Now rules. First conclusion, then premises

has_type(forty_two, int).

has_type(length(X), int) :- has_type(X, arr(T)).

has_type(sing(X), arr(T)) :- has_type(X, T).

% Now main

main(!IO) :-
    if has_type(length(sing(sing(forty_two))), T) then io.write(T, !IO) else io.write_string("fail", !IO).

typ and term are what I call syntactical types. I. e. types of nodes of our AST. They should not be confused with actual types of our target language (I will call them target types), such as int and arr(int). Target types are represented by values of syntactical type typ.

But… the code above will not compile, because I leaved mode and determinism markers. In other words, Mercury is not able to process arbitrary CSM, we must explicitly tell Mercury how Mercury should process it. I. e. we should guide Mercury execution. Okay, let’s supply mode and determinism markers (this is diff):

-:- pred has_type(term, typ).
+:- pred has_type(term::in, typ::out) is semidet.

Okay, now the code will compile. You may see warnings, but they are okay. The program will print correct target type, i. e. “int”.

What we just did? We specified that term is input and type is output. I think this is completely reasonable. See again at 7:34 in Steele’s talk. In his video term is input and type is output, too. He essentially talks about modes.

How to run this code? I installed Mercury to Debian using these instructions: http://dl.mercurylang.org/deb/ . Then created file hello.m with contents above. Then I compiled it using mmc --make hello, then I run it using ./hello; echo (echo is needed, because ./hello doesn’t print newline).

This book https://www.mercurylang.org/documentation/papers/book.pdf was helpful when writing code above.

I hope you understood the program above, otherwise I think you will not understand anything below.

Now let’s discuss desirable properties hypothetical Prolog implementation may have.

Property 1. It should have support for user-defined algebraic data types (ADT), such as typ and term above. As you can see, this is mandatory for translating CSM to Prolog. As we can see, Mercury has this property. Also note that ADT definition doesn’t necessary look like ADT definition. For example, let’s consider Makam. Here is Makam tutorial: https://astampoulis.github.io/blog/makam-tutorial-01/ . Author gives this example there:

stringconst : (S: string) -> expr.
intconst : (I: int) -> expr.
boolconst : (B: bool) -> expr.
add : (E1: expr) (E2: expr) -> expr.
array : (ES: list expr) -> expr.

This look like declarations of some functions. But conceptually we defined ADT named expr and its variants called stringconst, etc. So, Makam satisfies property 1, too, despite its documentation seems not to mention term “ADT”. But Datalog, at least as described in Wikipedia ( https://en.wikipedia.org/wiki/Datalog ) seem not to satisfy this property. But it is possible that actual Datalog implementations add this property.

Property 2. Support for lambdas, aka binders, aka capturing-free substitution. Well, “capturing-free substitution” and “support for lambdas” is probably different things, but they are still very closely related. This is the same capturing-free substitution Steele talks at 33:15. Okay, so lambdas and substitution are very desirable properties. For example, let’s consider https://en.wikipedia.org/wiki/Simply_typed_lambda_calculus . In section “Typing rules” we see rule 3. It involves lambda. In this article http://adam.chlipala.net/papers/MakamICFP18/MakamICFP18.pdf we can see that this rule can be encoded in Makam so:

typeof (lam T1 E) (arrow T1 T2) :−
(x:term → typeof x T1 → typeof (E x) T2).

Yes, this is exactly same rule modulo names for variables. Note that E here refers to what I call syntactical function. Or you may call it syntactical substitution. Or AST with hole. Also, note that idiomatic Makam code doesn’t use contexts (context is called Γ in that Wikipedia article), so we don’t see any Γ in Makam code. So, well, this Makam code absolutely exactly matches that rule 3 from Wikipedia, but this may be hard to understand. Anyway, what I want to say is this: property 2 is desirable for encoding CSMs and Makam has this property.

Property 3. There is no need to augment CSM with some markers to process it. Well, as we saw, Mercury doesn’t satisfy this property, because one need to specify modes and determinism markers.

Property 4. It is possible to enter any CSM to this Prolog implementation. This property doesn’t hold for Mercury, because not every CSM can be augmented with correct modes.

Property 5. If this fact has proof, then the implementation can find it. This property seems not to be hold for original Prolog. As well as I understand, original Prolog has quirky unreliable semantics. Prolog looks like logic engine, but (as well as I understand) it doesn’t implement logic correctly. So, AFAIK it is possible to construct CSM with particular fact such that this fact is provable, but Prolog will not find its proof. AFAIK this is exactly same complain, which we see in article you gave me: https://www.amzi.com/articles/prolog_under_the_hood.htm . So, Prolog is dishonest and unreliable. (When I say “unreliable” I mean “unreliable as logic engine”.) So, please, never use original Prolog. But, AFAIK you can enter any CSM (assuming it has no lambdas) to Prolog. Without any additional markers. So, it seems Prolog satisfies properties 1, 3 and 4. Well, there is some cheating here: Prolog is untyped, so it doesn’t have ADTs, but AFAIK we can somewhat emulate ADTs using functors, so let’s assume property 1 holds. Also, AFAIK Prolog doesn’t have lambdas, so property 4 holds with condition “assuming CSM doesn’t have lambdas”. So, in Prolog we have 1, 3 and 4, but don’t have 5. Mercury seems to be honest. If there is a proof, Mercury will find it. So, Mercury is honest, you can rely on it. Mercury is true logical engine, as opposed to Prolog. Prolog woes from https://www.amzi.com/articles/prolog_under_the_hood.htm don’t apply. Mercury has 5, but it doesn’t have 3 and 4. So there is a trade-off here: either we restrict set of possible programs and place burden on programmer in form of writing modes markers (Mercury), either we allow somewhat arbitrary CSMs, but will get unreliable broken semantics (original Prolog).

In this point you may ask: “But what exactly you mean when you say that Prolog is unreliable?” Well, let’s consider this Prolog program:

f(X) :- f(X).
f(a).

Here a is some fixed constant and X is variable. Then I asked Prolog (I used SWI-Prolog) is f(a) true. Prolog looped and did not produce any answer. It failed with stack overflow. But it is obvious that f(a) is true! It simply is present in our hypothesizes! So, yes, the main problem with Prolog from my point of view is here: it is very easy to trick Prolog into infinite loop. And for this reason I state that Prolog doesn’t satisfy property 5.

Now let’s compare with Mercury. Well, I just entered similar program to Mercury and got to infinite loop, too. :( But I have read here https://www.mercurylang.org/information/doc-latest/mercury_ref/Implementation_002ddependent-extensions.html , that I can specify --check-term to check for loops. I specified this option and yes, I got a message in compile time. So, yes, if your program belongs to particular set of programs (this set inclusion can be tested in compile time by specifying particular options), then you are guaranteed to get proof if it exists. (Well, everywhere I say “get proof” I don’t mean getting actual proof, I mean that the implementation can say “yes, it is true” or that implementation will produce some answer, say, target type of your term). (Also, Mercury doesn’t know that function “io.write” terminates. So when writing programs for real you should specify option --enable-term instead [see https://www.mercurylang.org/information/doc-latest/mercury_ref/Implementation_002ddependent-extensions.html ] and mark which functions you want to check for termination.) (Also, I spent some time playing with --check-term. It seems that this checker is very stupid, in lot of cases it cannot prove termination, when I know for sure that the program terminates. But still I will say that overall Mercury is reliable enough.)

In this point you may ask: “But what if Prolog has termination checker, too?” Well, possibly, I don’t want to check this. Anyway, I simply has a feeling that Prolog is unreliable mess. For Mercury I don’t have such feeling. All checks already present in Mercury together with --check-term makes it very reliable system.

Okay, so Prolog program above turns out to be very hard task for Prolog implementations. You either reject it in compile time (this is violation of property 4), either it runs and fails to loop without producing answer (this is violation of property 5).

Recently I said this:

I have in my TODO list item “Try to find Prolog/CSM implementation, which truly searches all proofs. If such doesn’t exist, then write my own”

I meant that I want to find (or write) Prolog implementation, which satisfies properties 1, 3, 4 and 5 in the same time. I don’t know whether such implementation exists already. And I know how such implementation would work. I. e. I can imagine algorithm. In simple terms such algorithm will try everything in parallel. Such implementation will produce answer (i. e. “true”) for above program in finite time. But there is another trade-off here: such implementation will be usually slower than alternative implementations, such as Mercury. Mercury has its restrictions and mode markers for a reason: they allow efficient implementation.

Here is interesting place from https://www.mercurylang.org/documentation/papers/book.pdf (p. 51):

Prolog programmers take note: unlike Mercury, Prolog programs commit to the first solution of Gc. The Prolog equivalent of the above goal would have Y = 9 as its only solution, not Y = 25 or Y = 49

This seems like another proof of Prolog’s unreliability (but I didn’t try to deeply understand this sentence).

Property 6. When there are multiple answers, implementation can find them all. For example, when given term can have multiple target types. Well, Mercury has this property, I was able to write program, which exploit it: https://paste.debian.net/1289302/ . I had to use solutions for this.

Property 7. The implementation is typed. Well, original Prolog doesn’t have this property. Mercury has. Makam has, too.

Property 8. The implementation can find answers with free variables. (Yes, this property is distinct from property 6.) For example, let’s assume that our first CSM example also has syntax for empty lists. I. e. our ADT for terms now looks so:

:- type term % Terms
        ---> sing(term) % [x]
        ;    length(term) % length(x)
        ;    forty_two % 42
        ;    empty_list. % []

Then we would get this additional rule:

has_type(empty_list, arr(T)).

Unfortunately, this would mean that solving has_type(empty_list, U) will get answer U = arr(T), i. e. answer will contain free variable. This seems not to be supported by Mercury. So for such situation you will need some unnatural encoding. So, Mercury does not have property 8.

Property 9. Computation always terminates. Yes, you may say that this is same as property 5. But it is not. Property 5 says: if there is at least one solution and we asked for at least one solution, then some solution will be printed and then the program will terminate. But if there is no solution, there is okay to loop forever. Property 9 says that program will always terminate, even if there is no solution. Properties 1, 4, 5 and 9 cannot be held in the same time. Because this would mean that we can in finite time determine whether given formula is provable in given logic. This is impossible, because we can encode Turing machine as CSM and this would mean that we can check in finite time whether Turing machine terminates, which is, as we know, impossible.

I said above that I can imagine algorithm, which has properties 1, 3, 4, 5. It will not have property 9. I. e. it will loop forever in many cases when there is no solution.

Also that hypothetical algorithm will have property 6. We can run CSM, which specifies axioms for propositional logic and program will run ad infinitum, printing all provable facts. Program will run forever and any provable fact will eventually appear in its output.

End of list of properties.

Okay, so I hope one day I will check whether various Prolog implementations have these properties (this may happen, say, in 10 years). This is list of Prolog implementations I will consider:

• Original Prolog :(
• Listed on https://www.lix.polytechnique.fr/~dale/lProlog/
• • Makam
• Mercury
• Twelf
• Datalog
• Soufflé

You may try to do the same. At least you now know what to look for.

---

FWIW my main interest is to write a SHORT and correct type checker for the metalanguage of https://oilshell.org

I think implementation of Oilshell itself should be in some well-known language. Haskell and Ocaml are good for implementing languages. Also see https://hirrolot.github.io/posts/compiler-development-rust-or-ocaml.html . If you also want Oilshell to be fast, then possibly Rust is good choice. Yet another variant is to wait when Mojo will be released.

But okay, let’s assume you chose to implement Oilshell in your own Python dialect. What language to implement its type checker in? Well, again, I suggest simply using some “normal” language. Such as Haskell or Ocaml. This will allow you to directly write your type checker. It will be relatively short. You may also chose something Prologish. But as I described above, this is minefield. But depending on exact task this may be acceptable solution.

If you already more or less understand algorithm of your type checker, i. e. you understand control flow of your type checker, then this means you already assigned modes to your type judgements in your head. This means Mercury may be good solution. Another situation is if you can write rules, but don’t understand control flow of your checker, i. e. you have no algorithm. Then assigning modes will be difficult.

Anyway, if you really want to try something Prologish, then try to write your rules in text editor in Prolog syntax. Then try to understand what properties from above list you will need from Prolog implementation. And then find Prolog implementation, which have these properties. :)

Another possible good solution is Makam. There is very good tutorial here: http://adam.chlipala.net/papers/MakamICFP18/MakamICFP18.pdf . Also see https://astampoulis.github.io/blog/ . In this article https://astampoulis.github.io/blog/makam-tutorial-01/ author proceeded straight to writing interpreter and parser in Makam.

But again: all these Prolog variants don’t have such care (i. e. devs’ effort) as Ocaml and Haskell. Also it is possible they will require some effort to integrate it with bigger system, i. e. pass information from it and to it.

control flow dependent null safety

Sounds very unusual. I have no idea how to implement this in Prologish languages. Ocaml and Haskell recommended

Basically I think Prolog does not have the YACC property of helping you check that your grammar is implementable efficiently, and of reporting ambiguities

As I said above Mercury has similar properties

OK so then my question is something like – can I translate type checkers in OCaml to Prolog with modes?

If you already have type checker in OCaml, why translate it to Prolog? But, okay, if you want, then it simple. If you have function f : a -> b, then its Mercury equivalent will be :- pred f(a::in, b::out) is det..

Does Prolog (or datalog) have any Yacc-like properties that make it better than a general purpose language, when used as a metalanguage?

Yes, Prologish languages have advantage: they directly correspond to CSM, i. e. they allow you to write typing rules directly. Some of them, such as Makam and Mercury also seem to have capture-free substitution built-in, which is very good, too.

Why did TAPL choose ML for their implementation language rather than Prolog/datalog?

I think because they wanted to show how actually the program is implemented.

And again I think even the ML implementations are far from “engineering reality”, as far as I can see

Rust was implemented in Ocaml first. Coq is implemented in Ocaml. CompilerCert is implemented in Ocaml. Isabelle is implemented in Isabelle/ML, which is ML dialect. So, Ocaml is pretty good “engineering reality”. It is full-blown programming language. You can do anything from it, including writing ActivityPub servers (I recently saw an article on writing ActivityPub server in Ocaml.)

(Personally I know Haskell, but don’t know Ocaml. Still I have read many articles on Ocaml and I see that this is a good language.)

then where does “Prolog with modes” fall down?

Prologish languages allow very concise programs as opposed to general purpose languages. But in the same time it is possible that in some moment you will hit some unavoidable restriction of such Prologish language. I. e. Prologish languages are shorter and they are very strict. (Also, this post [ https://lobste.rs/s/11k4ri/how_should_i_read_type_system_notation#c_b8ricb ] was written as your answer to yourself. I saw it by chance only.)

Right he says the first metalanguage is non-deterministic, but this one is deterministic

I suggesting looking carefully at these two slides and understand why one is deterministic and another is not. In slide 6:00 both conclusions have same form: no_conflict with arbitrary parameters. So if we want to check no_conflict for some set of arguments, we don’t know beforehand which rule to apply, so we have to run both. But note that in this slide we see very small part of CSM. We don’t see whole CSM, so we don’t know input/output modes. But even if all arguments to no_conflict are input, i. e. all them are known, then we still don’t know which rule to choose. I. e. even in simplest case we have non-determinism.

Now let’s see slide 7:00. This time it seems we see whole set of rules. And we know intended meaning of our relation (i. e. ... |- ... : ...): we know that it supposed to mean “has type of”, and thus we know that gamma/context and term are inputs and type is output. Now we can ask ourselves: is it possible by shape of inputs alone (i. e. context and term) to see what rule to apply. Yes, it is possible! If term is variable, then first rule applies, if term is lambda, then second rule applies, etc. I recommend try to imagine full algorithm for type checking for this slide.

---

Also, I highly recommend this cool demo: https://petevilter.me/post/datalog-typechecking/ , https://lingo-workbench.dev/ .

This demo is possibly of interest, too: https://github.com/voodoos/mlts . It is toy programming implemented in Lambda-Prolog

Another question is – it’s not enough for “Prolog with modes” to exist, it also has to be expressive enough

My guess is this deterministic metalanguage only works for a small minority of languages, e.g. if you take

Java < Go < MyPy < TypeScript

in roughly ascending order of “complexity” or “featurefulness”

then where does “Prolog with modes” fall down? My guess is it falls down even BEFORE Java

Because otherwise we would see people writing more of those type systems in Prolog, rather than a few toy blog posts here and there

Actually it seems like Prolog WITHOUT modes even falls down before Java