A functional language based on modal logic

I’ve been wanting to port FileOrganiser over to another language, and also completely change the way it works, and make it cooler. In 2021 I wrote a program to keep a directory sorted, and that was a good idea, but now I want to take that idea and do it a completely different way in a completely different language.

The idea

There should be a programming running in the background, pointed at some directory on my file system. When there is a new file created in that directory my program should be able to apply a function to that file, and get back another function that, when called, will move the file somewhere else. Maybe it will get renamed, or just moved to a subdirectory, it doesn’t matter.

The first time I did this, someone requested a scripting interface, e.g. if a file with the extension .zip is created, we should pass it to a function that can unzip it. Or whatever. Basically, the goal should not be a program that moves files around, but rather a program that, when certain events occur, can apply a predicate (Fn(x) -> Bool) to that event, and if the predicate is satisfied (returns true) can then apply a function to it.

The bad idea

So I started to think about this, and had the realisation that this can be modeled using possible world semantics. Without getting too much into it, here is the gist.

A world is set of propositions, and we use Kripke Semantics to describe a set of possible worlds. Really, it’s just a digraph. Where the nodes are our worlds, and edges (called accessibility relations), are just mappings of one world onto another.

$$\begin{array}{rl}K=\{& \{W_0,W_1,W_2\}\\ & \{(W_0,W_1),(W_1,W_2),(W_2,W_2)\}\\ \}& \end{array}$$

or

graph LR

0 --> 1
1 --> 2
2 --> 2

Accessibility relations, really. Are just functions. They map the propositions in one world to propositions in another world. So why reimplement my simple library when I could write a declarative programming language based on modal logic to do the same thing?

File Organiser (as an example)

Worlds, and accessibility.

let’s say we have a directory with the following structure:

Dir:
	- Pdfs
	- Images
	- Archives
	- Fonts
	- Other

We can think of this nicely sorted directory as our world zero. There’s no other kind of file, just subdirectories. We can then define this world (or state) formally like so:

$$x\in W_0⟺Dx$$

where D is a one place predicate stating that $x$ is a Directory. Although this is a definition of $W_0$, what we really want is a predicate that tells us if our current world is $W_0$.

$$W_i=W_0⟺\forall x\in W_i(Dx)$$

which is to say that our current world is equivalent to $W_0$ if all elements in our world satisfy the predicate of being directories.

But let’s look at another possible world where our directory looks like this:

Dir:
	- Pdfs
	- Images
	- Archives
	- Fonts
	- Other
	- Stalneker & Lewis.pdf

We want to be specific when defining our predicate for this world, so we’ll say that $x$ is either a directory (D), or a PDF file, and we’ll call this $W_p$ for PDF (P)

$$x\in W_p⟺Dx\vee Px$$

and

$$W_i=W_p⟺\forall x\in W_i(Dx\vee Px)$$

Our accessibility relation, then, is a function $W_p\to W_0$ and if the goal is sorting our directory, then it’s obvious where our PDF file should be. We just have to move it into the PDF subdirectory. Let’s write a little fake program:

(defn PDFSorter [file]
	(mv file if file is PDF))

Thus, with this little function, our graph has edges

graph TD
WP -- PDFSorter --> W0

Handling other types of files.

Maybe it would be nice if we could sort something other than PDFs. Maybe there’s another possible world where we have a zip file. I won’t bother with formal notation, we’ll just write our relation:

(defn ZipSorter [file]
	(mv file if file is ZIP))

graph TD
WP -- PDFSorter --> W0
WZ -- ZIPSorter --> W0

But, idk, I download a lot of fonts, so maybe it’s worthwhile to inspect the ZipFile, and if it contains fonts, to move it there.

(defn ZipSorter-but-fonts [file]
	(mv file if file is ZIP AND HAS_FONTS))

graph TD
WP -- PDFSorter --> W0
WZ -- ZIPSorter --> W0
WZ -- ZipSorter-but-fonts --> W0