Is anybody out there doing category theory with Prolog?

[dcnorris]

Of course, strongly typed functional programming languages have long had a categorical flavor. Haskell with its monads, etc. There is a funny story in this blog post, as follows:

1990 - A committee formed by Simon Peyton-Jones, Paul Hudak, Philip Wadler, Ashton Kutcher, and People for the Ethical Treatment of Animals creates Haskell, a pure, non-strict, functional language. Haskell gets some resistance due to the complexity of using monads to control side effects. Wadler tries to appease critics by explaining that "a monad is a monoid in the category of endofunctors, what's the problem?"

All that aside, given the deep undercurrent of logic in category theory, it would seem entirely natural that people would be doing categorical work in Prolog, too. Who is doing such work? (BTW, I posted a question like this on Mathstodon but have not yet received a positive reply.)

[bakaq]

I have a heavy interest in both category theory and Prolog, so I thought about things like that before. Prolog is different from Haskell in that it is basically untyped and has all of the non-determinism stuff, so (from what I tried, which was very little) it's hard to make direct analogies with "Haskell style category theory". My intuition is that there is probably a way to formulate Prolog (and things like DCGs) in terms of category theory, but that will probably look very different from Haskell (I don't think DCGs are a Monad for example).

In a more practical note, I think trying implement a version of things like monads in Prolog would be very useful. DCGs take a lot of the responsabilities that in Haskell you would give to a monad, like state. However, there are somethings that I think monads do much better than DCGs, like side-effects. The way I've seen to do pure Prolog with side effects is to calculate your whole program with pure Prolog and then do the side effects after. Some helpers like phrase_from_file/2 make the Prolog safely interleave with the side effects, but I feel those are fundamentally limited in some way. I believe having an parallel to the IO monad of Haskell could maybe make pure Prolog easier to work with.

On using Prolog to research category theory, I think it's very promising. Using Prolog and constraints you could "model check" small categories which is interesting, but you could also make more complex proof-systems that handle specific types of categories, like topoi which encode many kinds of logics.

I'm very new to category theory and kind of new to Prolog in general also, so please correct me if I said anything incorrect or misleading.

[aarroyoc]

I do not know a lot about category theory, so maybe this is unrelated, but some time ago I found a paper which uses Monads to introduce logical programming non-determinism. The LogicT type: https://okmij.org/ftp/papers/LogicT.pdf and https://hackage.haskell.org/package/logict-0.8.1.0/docs/Control-Monad-Logic.html

[bakaq]

Well, in this case I think you can say that Prolog is a monad, and that is very funny but also interesting.

[dcnorris]

Using Prolog and constraints you could "model check" small categories which is interesting,

In fact, this is what I am up to at the moment in some very 'applied' work — computing monoidal preorders generated by a graph. Prolog with CLP(Z) feels perfectly adapted to this investigation.

but you could also make more complex proof-systems

This is maybe the topic of a separate question I've been meaning to ask. Why so much proof-assistant work being done with Agda, Coq, etc. — and not Prolog?

[mthom]

I'm writing a theorem prover in Scryer Prolog for my Shen implementation right now. I use Racket's syntax-parse library to transcribe from Shen's sequent calculus syntax into ISO Prolog.

I also have some CWM solutions I'm slowly transcribing into LaTeX on my computer. Not related to Prolog as such but I'm thinking of ways to diagram chase effectively in Prolog. Mac Lane co-wrote a sort-of sequel to CWM called "Sheaves in Geometry and Logic" I've been meaning to read for years, and it explores some of category theory's connections to mathematical logic @dcnorris mentioned.

On the subject of monads, DCGs are very much like Haskell's state monad. Also continuations are the mother of all monads, which we also have in Scryer in the form of delimited continuations. So in some sense we already have them.