[dmytrish]

Not exactly a big codebase, but it was a revelation for me how natural typecheckers can feel in Prolog: I basically rewrote typing rules with some tweaks: [1]

Also, tests were surprisingly enjoyable in Prolog: [2].

[1] https://github.com/EarlGray/language-incubator/blob/29755c32... [2] https://github.com/EarlGray/language-incubator/blob/29755c32...

[h_sakurai]

https://github.com/hsk/simpletapl/blob/master/prolog5/fullup...

I have rewritten all TAPL code in Prolog. It was very interesting.

https://github.com/mitsuchi/copl-in-prolog/

This is another textbook "Concept of Programming Language" implementations.

https://www.fos.kuis.kyoto-u.ac.jp/~igarashi/CoPL/

[PebblesHD]

Not a criticism of the code here by any stretch, I always find it impressive when people manage to understand languages that are totally foreign to me, that being said however Prolog has always struck me as uniquely unreadable. Even back in university when we looked briefly at different styles of programming, the code always ended up looking something like lines 107-132 in your example, which to someone jumping in is pretty much indecipherable.

Is anyone aware of any higher level abstractions for logic based languages that is actually used in industry? From what I’ve seen in the various banks and fintech groups I’ve worked with, prolog itself was very rarely if ever used ‘in anger’, but I have heard of it being used for automation so I’m very curious what that looks like.

[triska]

Regarding the code in question, it is possible to write it a bit more elegantly and more compactly, with a combination of techniques. For example, let's consider this snippet from lines 110 to 119:

    type(Ctx, case(T0, {z, Tz}, {s(V), Ts}), Ty) :- !,
      isvar(V),
      type(Ctx, T0, nat),
      type(Ctx, Tz, Ty),
      CtxS = [{V, nat} | Ctx], type(CtxS, Ts, Ty).
    type(Ctx, case(T0, {inl(Vl), Tl}, {inr(Vr), Tr}), Ty) :- !,
      isvar(Vl), isvar(Vr),
      type(Ctx, T0, uni(Ty1, Ty2)),
      Ctx1 = [{Vl, Ty1} | Ctx], type(Ctx1, Tl, Ty),
      Ctx2 = [{Vr, Ty2} | Ctx], type(Ctx2, Tr, Ty).

It is clear that the two clauses are mutually exclusive if the second argument is known, because they differ in various terms already in the head. For instance, {z, Tz} is clearly different from {inl(Vl), Tl}. A Prolog system with deep indexing, which is also used by Mercury, can detect this, and in such a system, we can therefore remove the two occurrences of !/0 in the code, yielding a more general and shorter version:

    type(Ctx, case(T0, {z, Tz}, {s(V), Ts}), Ty) :-
      isvar(V),
      type(Ctx, T0, nat),
      type(Ctx, Tz, Ty),
      CtxS = [{V, nat} | Ctx], type(CtxS, Ts, Ty).
    type(Ctx, case(T0, {inl(Vl), Tl}, {inr(Vr), Tr}), Ty) :-
      isvar(Vl), isvar(Vr),
      type(Ctx, T0, uni(Ty1, Ty2)),
      Ctx1 = [{Vl, Ty1} | Ctx], type(Ctx1, Tl, Ty),
      Ctx2 = [{Vr, Ty2} | Ctx], type(Ctx2, Tr, Ty).

The isvar/1 tests can be removed if we use a better representation of our data. For instance, if we use the wrapper v/1 to denote variables in the data, we can replace these clauses by:

    type(Ctx, case(T0, {z, Tz}, {s(v(V)), Ts}), Ty) :-
      type(Ctx, T0, nat),
      type(Ctx, Tz, Ty),
      CtxS = [{V, nat} | Ctx], type(CtxS, Ts, Ty).
    type(Ctx, case(T0, {inl(v(Vl)), Tl}, {inr(v(Vr)), Tr}), Ty) :-
      type(Ctx, T0, uni(Ty1, Ty2)),
      Ctx1 = [{Vl, Ty1} | Ctx], type(Ctx1, Tl, Ty),
      Ctx2 = [{Vr, Ty2} | Ctx], type(Ctx2, Tr, Ty).

Finally, the variables CtxS, Ctx1 and Ctx2 are only used once each, so we can simply write:

    type(Ctx, case(T0, {z, Tz}, {s(v(V)), Ts}), Ty) :-
      type(Ctx, T0, nat),
      type(Ctx, Tz, Ty),
      type([{V, nat} | Ctx], Ts, Ty).
    type(Ctx, case(T0, {inl(v(Vl)), Tl}, {inr(v(Vr)), Tr}), Ty) :-
      type(Ctx, T0, uni(Ty1, Ty2)),
      type([{Vl, Ty1} | Ctx], Tl, Ty),
      type([{Vr, Ty2} | Ctx], Tr, Ty).

With the necessary provisions in place, it may be possible to shorten it further, by generating such code automatically from more declarative descriptions, using a mechanism called term expansion which is available in most Prolog systems. It is analogous to what other languages such as Rust call macros.

[Spooky23]

Prolog was really friendly to creating little DSLs.

I used to be a specialist in a product called Tivoli Enterprise Console. Which was a late 90s/2000s era event correlation system that used an ancient prolog dialect as its rules engine.

I had an awesome boss who let me do whatever, a limited set of tools, and a partner in crime who complemented my style. So we ended up implementing an Oracle database interface in Perl and a client application that allowed others to add facts to the database. Periodically, we’d load the facts into the prolog system and could make queries to tell us what apps were impacted, did we care about them, who was responsible, etc.

The end system was able to identify app owners, system administrators and other information on any of about 20k servers and lots of network gear. We were able to take a flow of about 300k daily events and cook it down to about 40-50 actionable alerts and a few hundred automated actions.

The whole thing took about 3 months to build and another 4-6 to tweak. We got promoted and moved on, but the system hummed along for about 4-5 years until IBM started killing the underlying product. I think the place pivoted that functionality to ServiceNow.

[dmytrish]

That's the largest piece of Prolog code I've ever written, so criticism is warranted and I'm glad to learn how to improve it. I still wanted to share it to show how typing rules translated almost directly to Prolog clauses.

I agree that this piece of code was written in a more academic mindset, with large dose of TAPL-specific jargon and abbreviations which can easily throw anybody off if not known beforehand. I do not have good examples of industrial-grade Prolog code bases, if that's what was asked.

[molenzwiebel]

Worth checking out if you're interested in using constraint/logic programming languages for type checking is the Statix (https://www.spoofax.dev/references/statix/) language, which is used in the Spoofax language workbench. It works similarly to Prolog in solving constraints, but adds support for scope graphs, which are a generic approach to specifying the name binding behavior of programming languages through logic constraints.