johnbernier

Set theory is not going anywhere. It may be pushed to the sidelines by new developments in category theory but that is not the same as going extinct like the dodo.

In computer science we typically count from zero, not from one. So even though a category has two different sorts of entities: objects and morphisms, since we count from zero, ordinary categories are one-dimensional. Objects are zero dimensional and morphisms are one dimensional.

Since you are concerned with sets and functions, the following analogy is helpful to build your intuition for the subject.

Dimension 0: sets

Dimension 1: functions

Dimension 2: commutative squares

Dimension 3: commutative cubes

The majority of categories, expressed in terms of structured sets and functions, never touch on the second dimension. That is the domain of 2-categories, which although they have three types of elements are nonetheless considered to be two dimensional because we count from zero. That is also where commutative squares come in to play, because as you can imagine squares are quite obviously two dimensional.

Functions are 1-dimensional lines or arrows from one place to another. Sets are more analogous to points then anything else, and so naive set theory is zero dimensional. But I think you have the wrong question. You should ask the opposite question: what if functions can be re-expressed or founded on higher dimensional category theory?

That works for any function f that is precomposed by a bijection. Then the bijection and its inverse cancel out, so that is correct. Many of these examples with regards to precomposition and postcomposition might be embedded in other categories, such as slice categories: C/f or f/C. However, of all the different categories you can use to make a model of functions I have singled out Sets^(->) because it forms a topos.

The property that Sets^(->) is a topos gives us a lot to work with. All impredicative constructive mathematics can be defined internal to Sets^(->). This is interesting because it means almost all mathematics can be done internal to Sets^(->), with functions instead of sets as its first class logical objects.

Secondly, the fact that it is a topos gives us an internal logic in Sets^(->). The internal logic of Sets^(->) is a trivalent logic with three values: true, false, and half truth that fails to satisfy the law of excluded middle. Sets^(->) has its own distinct system of logical operators and connectives which generalize those in classical logic and that can be used on all subobjects.

All aside from that, Sets^(->) has an incredibly remarkable logic of quotients. It has been shown that the dual logic of quotients in Sets^(->) is intuitively similar to the partition pairs construction of Hartmanis and Stearns in Algebraic Structure Theory of Sequential Machines (1966). So the immense power of the topos Sets^(->) is enough to capture their central construction for creating a computational structure theory, and mine.

All this demonstrates that Sets^(->) by itself has an incredibly rich theory which is worthy of further exploration. The theory of Sets^(->) is really the functional counterpart of set theoretic foundations, a foundation for a different kind of function-based mathematics, and the means by which we can create a system of logical reasoning for functional programs.

[1] https://ncatlab.org/nlab/show/topos

[2] https://ncatlab.org/nlab/show/internalization

[3] https://ncatlab.org/nlab/show/internal+logic

[4] Hartmanis, J., & Stearns, R. E. (1966). Algebraic structure theory of sequential machines. Prentice-Hall.

The topos of functions Sets^(->) has as its objects functions and as its morphisms m: f -> g function pairs (h,k) that make a commutative square with gh = kf. If we take function pairs like (h,k) as our morphisms then we can do several things to simplify them: like making the two functions in the pair equal or making one of them into an identity.

1. precomposition: with precomposition you should use a function pair (h, 1_b) that has an identity for the second part to form a morphism m: fg -> f like so: https://q.uiver.app/?q=WzAsNCxbMCwyLCJBIl0sWzIsMiwiQiJdLFswL...

2. postcomposition: with postcomposition you should use a function pair (1_b, k) that has an identity for the first part to form a morphism m: f -> hf like so: https://q.uiver.app/?q=WzAsNCxbMCwyLCJBIl0sWzIsMiwiQiJdLFsyL...

3. conjugation: with conjugation you can actually use an equal function pair (g,g) to morphism a function f to its conjugate gfg^{-1}. Then we see that this forms a commutative square for gfg^{-1}g = gf. Thusly, there is always a morphism from any function to its conjugate by a bijection like so: https://q.uiver.app/?q=WzAsNCxbMCwyLCJBIl0sWzIsMiwiQSJdLFswL...

Therefore, I would say that precomposition, postcomposition, and conjugation form special types of morphisms between functions defined by special properties like having one function be the identity or having both functions be equal to one another. Then beyond that we can classify these morphisms by rather or not their components are projections, injections, or bijections to get towards what you are speaking about. This all fits in to the perspective that functions are objects in Sets^(->), so that is nice.

I can't say I've ever used APL but I have heard of it. It has some very interesting syntax and notation, but I have made it far enough to actually try it out yet.

In this post I describe my own journey getting in to functional programming. Early on I gained a deep fascination with functional lenses, and their ability to let us focus on a portion of a data structure. Yet it seems to me that this should be part of a larger logical theory of functions.

If we can peer in to focus in on parts a data structure, we should also be able to focus in on parts of functions. To expose how functions behave relative to parts of structures like those determined by lenses. I describe how commutative squares let you do that. A large assortment of references is provided at the end for interested parties who want to know more.

I've recently tried QT creator and it was hard to figure out at first as many things are, but once I did it didn't have any problems or visual bugs for me. Overall it seems to be working pretty great, but rather or not you have issues depends upon your install, what version you are using, what operating system your are using, etc. So who knows.

But I think that QT creator should have a faster initial load then Visual Studio Code, because the later has to open up an entire browser render-er to work. QT creator opens instantly on my system, but visual studio code lags for a second. The weird visual bugs might indicate something else wrong with your system which is messing up the program. A picture might help us to find what the bug is so we can fix it.

As for the less enjoyable to use thing, there isn't much I can do about that. Visual studio code is probably more fun to use, and React isn't too bad either. Using React can be a joyful experience indeed. But enjoyment issues aside, I think that a good C++/QT based application should have a performance advantage over one made with HTML/CSS/JavaScript and Electron. Visual studio code can be more enjoyable but still perform slightly less well, because it doesn't have to make a difference to the end user that it does things a couple milliseconds slower.

The issue is exactly this. More and more people are coming into the development space using HTML/CSS/JavaScript and the information on the other technologies is harder to grasp and get a hold of.

What happened is naturally growth. There are more developers today then ever before, corresponding to the rise in the global population. As there are more and more developers, there is an associated rise in the number of people wanting to get into making desktop GUI applications. Most people don't know desktop frameworks like QT and Swing, so new people coming into the application development space are going to make applications in what they know: HTML/CSS/JavaScript.

Yet even as this happens and HTML/CSS/JavaScript rises that doesn't mean that there is a decline in the making of desktop applications. I think that desktop applications made with native technologies are being built as much as ever, its just that the industry as a whole has grown to accommodate the vast influx of new HTML/CSS/JavaScript developers. For example, my favorite applications are build in Swing (IntelliJ and related projects) or in QT.

> Just for completeness I should mention Linux, it is the best computing platform to happen to the world and should be admired in every way – except one! the desktop/UI sucks, its awful in almost every way

I say that KDE is awesome. So that is just your opinion, and not everyone agrees.

> Developing desktop apps in 2022 is essentially an HTML/CSS/JavaScript endeavour

That does not follow.

> the performance of a well written UI in a modern browser out-performs a native desktop application in every category of sped, usability and presentation for most usual use cases.

That is not my experience. Visual Studio Code doesn't seem to run as smoothly as I would like. Meanwhile every C++/QT application I have run works perfectly. Where are you getting this from?

In this post, I describe how to use Clojure to create Graphviz visualizations of the information flow lattices of finite maps and finite functions with the Locus computer algebra system. A collection of diagrams are provided so that readers can get a visual intuition for the subject.

The JVM lets you program in whatever you want to and then use code written in whatever comfy language (Java, C/C++ via native interop, Kotlin, etc) or a Lisp dialect (Clojure). I frequently use Java and Clojure together in the same project to great satisfaction, but I know what you mean anyways. We need WASM to get around the web question. I just hope it can fulfill the promise you have set upon it.

The basic idea of an information flow was introduced by Hartmanis and Stearns in the algebraic structure theory of sequential machines. This is a beautiful and elegant formalism for describing how information flows in sequential machines. Now using new mathematics I have put this theory on its highest level of generality. But its not enough that this should be a mathematical theory, so I also discuss its implementation.

At the center of an implementation of information flows is the idea of a partition image. This codifies how a particular function maps a piece of information into some other piece of information. To implement this intuitive idea, I define a type hierarchy of different partition and function classes and use multiple dispatch on them to determine the right algorithm to use on a case-by-case basis.

Upon review, Hartmanis and Stearns appear to have come closest to my work. I would recommend readers take a look at Algebraic Structure Theory of Sequential Machines (1966) prior to my paper to get a background motivation for my treatment of the subject. The idea of partition pairs in that textbook coincides with epimorphism classes in the Sierpinski topos.

So basically, all I am doing is updating that prior work and turning it into a Topos Structure Theory of Sequential Machines. I arrived at the concept of partition pairs independently through the Sierpinski topos. Hartmans & Stearns came up with the same idea for its engineering applications. It often happens that when an idea is good, it tends to crop up independently in multiple different places.

Hello, I do research in the area of program data-flow analysis. The theory of data-flow analysis has been extensively studied. Data Flow Analysis: Theory and Practice by Khedker, Sanyal, and Sathe is a reference textbook. This subject essentially studies how programs move data from one memory location to another.

My work in this field has led me to search for new mathematical foundations for dataflow analysis. These foundations will abstract the concept and address a number of issues. Firstly, traditional dataflow analysis only works on explicitly defined product types like bit vectors. This provides a limited scope for the theory. To generalize from this, we can use partitions, which can model any type of information accessible by a function.

Then to model dataflow relations in this new abstracted setting, I have suggested the use of the Sierpinski topos. Using this fundamental topos, we can model dataflow relations between information locations represented with the highest level of generality. This forms a broad generalisation of the notion of congruences from abstract algebra.