I'm interested in clarifying a bit of programming semantics. I want to represent programs as mathematical objects to see how the structure of those objects is reflected in the structure of the programs.
The two programs I'm looking at are "filter"--which filters sets of objects based on a predicate on those objects, and "group"--which partitions sets of objects.
It seems clear to me that filter is a function related to the equalizer of a set. Shown with the type signature below, filter is defined as a function which takes a predicate function as its input and returns a function on sets as its output. $$ filter : (a\to\mathbf{2})\to \{a\} \to \{a\} $$ The core logic of filter relies on applying the user supplied predicate, $\Omega$, to determine inclusion of the elements in the output, pseudo code for filter follows: $$ \begin{align} filter\: \Omega \: as = &\mathrm{forall} \: a\in as\\ &\dots \mathrm{if}\: (True = \Omega \: a )\\ & \qquad \textrm{then: include } a \textrm{ in output}\\ & \qquad \textrm{else: don't include } a \textrm{ in output}\\ &\dots \end{align} $$ This core logic bears a resemblance to the pullback, in set, of the two functions, $\top:\mathbf{1} \to \mathbf{2}$, and $\Omega : a \to \mathbf{2}$ The statement, $ \mathrm{if}\: (True = \Omega \: a )$ being the "diagram chase" of the two paths in the pullback square for the element, $(\top \circ \: !)\:a = (\Omega \circ id)\: a $. The left hand of the proceeding involves the constant function, $!$, and always resolves to "True". The right hand side involves the identity function.
Now to the question. This pullback can be reformulated as an equalizer of $\top \circ \pi_l$ and $\Omega \circ \pi_r $, where $\pi_l$, and $\pi_l$ are the left and right projections of $\mathbf{1}\times\{a\}$. Dual to an equalizer is the co-equalizer, which in set is the (reflexive, symmetric, transitive closure) of the equivalence relation imposed by forcing $f(a) \sim g(a)$. In programming, my group function is defined as a function which takes a tagging function, $\Gamma:a\to\Bbb{N}$, as its input and returns a partitioning function as its output. $$ group : (a\to\mathbb{N})\to \{a\} \to \{\{a\}\} $$ Following my discussion above, I was wondering if this program somehow fit into the co-equalizer scheme similar to how I posed filter in terms of it's characteristic function, $\Omega$. Specifically, filter is pulling back $\top$ and $\Omega$, but I can't seem to place what two functions group would be pushing out. Neither seem to be $\Gamma$. What would it be?
Thanks.
I'm not quite sure which parts of your question are important and which are incidental, but I think maybe that the meat of your question is about constructing equivalence relations and quotient objects, which can be done abstractly in a regular category.
In particular, to any morphism $f : X \to Y$, the equivalence relation $\Theta$ generated by $f$ is the pullback $$\begin{matrix} \Theta &\to& X \\ \downarrow & & \downarrow {\small f\!\!\!\!\!} \\ X &\xrightarrow{f}& Y \end{matrix}$$ Of course, by abstract nonsense $\Theta$ represents a subobject of $X \times X$ given by the equalizer $$ \Theta \to X \times X \overset{f \circ \pi_0}{\underset{f \circ \pi_1}{\rightrightarrows}} Y$$
Then, given any equivalence relation on $\Theta$, we can construct the quotient object of $X/\Theta$ as the coequalizer $$ \Theta \overset{\pi_0}{\underset{\pi_1}{\rightrightarrows}} X \xrightarrow{p} X / \Theta $$
By the first isomorphism theorem, there is a monic $i : X / \Theta \to Y$ that represents the image of $f$, and $f = i \circ p$.
One thing to note is that $X / \Theta$ doesn't have an intrinsic interpretation of its elements; e.g. in the case of a "tagging" map $\rho : A \to \mathbf{N}$, the quotient $A / \Theta_\rho$, whether it looks like a subset of tags or a set of subsets of $A$ depends on how you make use it.