Do Hask or Agda have equalisers?

Question

I was somewhat undecided as to whether this was a math.SE question or an SO one, but I suspect that mathematicians in general are fairly unlikely to know or care much about this category in particular, whereas Haskell programmers might well do.

So, we know that Hask has products, more or less (I'm working with idealised-Hask, here, of course). I'm interested in whether or not it has equalisers (in which case it would have all finite limits).

Intuitively it seems not, since you can't do separation like you can on sets, and so subobjects seem hard to construct in general. But for any specific case you'd like to come up with, it seems like you'd be able to hack it by working out the equaliser in Set and counting it (since after all, every Haskell type is countable and every countable set is isomorphic either to a finite type or the naturals, both of which Haskell has). So I can't see how I'd go about finding a counterexample.

Now, Agda seems a bit more promising: there it is relatively easy to form subobjects. Is the obvious sigma type Σ A (λ x → f x == g x) an equaliser? If the details don't work, is it morally an equaliser?

Answer 1

tl;dr the proposed candidate is not quite an equaliser, but its irrelevant counterpart is

The candidate for an equaliser in Agda looks good. So let's just try it. We'll need some basic kit. Here are my refusenik ASCII dependent pair type and homogeneous intensional equality.

record Sg (S : Set)(T : S -> Set) : Set where
  constructor _,_
  field
    fst : S
    snd : T fst
open Sg

data _==_ {X : Set}(x : X) : X -> Set where
  refl : x == x

Here's your candidate for an equaliser for two functions

Q : {S T : Set}(f g : S -> T) -> Set
Q {S}{T} f g = Sg S \ s -> f s == g s

with the fst projection sending Q f g into S.

What it says: an element of Q f g is an element s of the source type, together with a proof that f s == g s. But is this an equaliser? Let's try to make it so.

To say what an equaliser is, I should define function composition.

_o_ : {R S T : Set} -> (S -> T) -> (R -> S) -> R -> T
(f o g) x = f (g x)

So now I need to show that any h : R -> S which identifies f o h and g o h must factor through the candidate fst : Q f g -> S. I need to deliver both the other component, u : R -> Q f g and the proof that indeed h factors as fst o u. Here's the picture: (Q f g , fst) is an equalizer if whenever the diagram commutes without u, there is a unique way to add u with the diagram still commuting.

Here goes existence of the mediating u.

mediator : {R S T : Set}(f g : S -> T)(h : R -> S) ->
           (q : (f o h) == (g o h)) ->
           Sg (R -> Q f g) \ u -> h == (fst o u)

Clearly, I should pick the same element of S that h picks.

mediator f g h q = (\ r -> (h r , ?0)) , ?1

leaving me with two proof obligations

?0 : f (h r) == g (h r)
?1 : h == (\ r -> h r)

Now, ?1 can just be refl as Agda's definitional equality has the eta-law for functions. For ?0, we are blessed by q. Equal functions respect application

funq : {S T : Set}{f g : S -> T} -> f == g -> (s : S) -> f s == g s
funq refl s = refl

so we may take ?0 = funq q r.

But let us not celebrate prematurely, for the existence of a mediating morphism is not sufficient. We require also its uniqueness. And here the wheel is likely to go wonky, because == is intensional, so uniqueness means there's only ever one way to implement the mediating map. But then, our assumptions are also intensional...

Here's our proof obligation. We must show that any other mediating morphism is equal to the one chosen by mediator.

mediatorUnique :
  {R S T : Set}(f g : S -> T)(h : R -> S) ->
  (qh : (f o h) == (g o h)) ->
  (m : R -> Q f g) ->
  (qm : h == (fst o m)) ->
  m == fst (mediator f g h qh)

We can immediately substitute via qm and get

mediatorUnique f g .(fst o m) qh m refl = ?

? :  m == (\ r -> (fst (m r) , funq qh r))

which looks good, because Agda has eta laws for records, so we know that

m == (\ r -> (fst (m r) , snd (m r)))

but when we try to make ? = refl, we get the complaint

snd (m _) != funq qh _ of type f (fst (m _)) == g (fst (m _))

which is annoying, because identity proofs are unique (in the standard configuration). Now, you can get out of this by postulating extensionality and using a few other facts about equality

postulate ext : {S T : Set}{f g : S -> T} -> ((s : S) -> f s == g s) -> f == g

sndq : {S : Set}{T : S -> Set}{s : S}{t t' : T s} ->
       t == t' -> _==_ {Sg S T} (s , t) (s , t')
sndq refl = refl

uip : {X : Set}{x y : X}{q q' : x == y} -> q == q'
uip {q = refl}{q' = refl} = refl

? = ext (\ s -> sndq uip)

but that's overkill, because the only problem is the annoying equality proof mismatch: the computable parts of the implementations match on the nose. So the fix is to work with irrelevance. I replace Sg by the Existential quantifier, whose second component is marked as irrelevant with a dot. Now it matters not which proof we use that the witness is good.

record Ex (S : Set)(T : S -> Set) : Set where
  constructor _,_
  field
    fst : S
    .snd : T fst
open Ex

and the new candidate equaliser is

Q : {S T : Set}(f g : S -> T) -> Set
Q {S}{T} f g = Ex S \ s -> f s == g s

The entire construction goes through as before, except that in the last obligation

? = refl

is accepted!

So yes, even in the intensional setting, eta laws and the ability to mark fields as irrelevant give us equalisers.

No undecidable typechecking was involved in this construction.

Answer 2

Hask

Hask doesn't have equalizers. An important thing to remember is that thinking about a type (or the objects in any category) and their isomorphism classes really requires thinking about the arrows. What you say about the underlying sets is true, but types with isomorphic underlying sets certainly aren't necessarily isomorphic. One difference between Hask and Set as that Hask's arrows must be computable, and in fact for idealized Hask, they must be total.

I spent a while trying to come up with a real defensible counterexample, and found some references suggesting it cannot be done, but without proofs. However, I do have some "moral" counterexamples if you will; I cannot prove that no equalizer exists in Haskell, but it certainly seems impossible!

Example 1

f, g: ([Int], Int) -> Int

f (p,v) = treat p as a polynomial with given coefficients, and evaluate p(v).
g _ = 0

The equalizer "should" be the type of all pairs (p,n) where p(n) = 0, along with a function injecting these pairs into ([Int], Int). By Hilbert's 10th problem, this set is undecidable. It seems to me that this should exclude the possibility of it being a Haskell type, but I can't prove that (is it possible that there's some bizarre way to construct this type that nobody has discovered?). It maybe I haven't connected a dot or two -- perhaps proving this is impossible isn't hard?

Example 2

Say you have a programing language. You have a compiler that takes the source code and an input and produces a function, for which the fixed point of the function is the output. (While we don't have compilers like this, specifying semantics sort of like this isn't unheard of). So, you have

compiler : String -> Int -> (Int -> Int)

(Un)curry that into a function

compiler' : (String, Int, Int) -> Int

and add a function

id' : (String, Int, Int) -> Int
id' (_,_,x) = x

Then the equalizer of compiler', id' would be the collection of triplets of source program, input, output -- and this is uncomputable because the programing language is fully general.

More Examples

Pick your favorite undecidable problem: it generally involves deciding if an object is the member of some set. You often have a total function that can be used to check this property for a particular object. You can use this function to create an equalizer where the type should be all the items in your undecidable set. That's where the first two examples came from, and there are tons more.

Agda

I'm not as familiar with Agda. My intuition is that your sigma-type should be an equalizer: you can write the type down, along with the necessary injection function, and it looks like it satisfies the definition entirely. However, as someone who doesn't use Agda, I don't think I'm really qualified to check the details.

The real practical issue though is that typechecking that sigma type won't always be computable, so it's not always useful to do this. In all the examples above, you can write down the Sigma type you provided, but you won't be able to readily check if something is a member of that type without a proof.

Incidentally, this is why Haskell shouldn't be able to have equalizers: if it did, the typechecking would be undecidable! Dependent types is what makes everything tick. They should be able to express interesting mathematical structures in its types, while Haskell can't since its typesystem is decideable. So, I would naturally expect idealized Agda to have all finite limits (I would be disappointed otherwise). The same goes for other dependently typed languages; Coq, for example, should definitely have all limits.