My question is which functions can not be allowed in a statically typed programming language, so that the "canonical" category is less coarse than what you get if you define it's arrows to be extensionally identified functions in the language. (More concrete question at the bottom after I say what I want to get at.)
I contrast this with Haskell, where the code sees quite a bit more than the category $\mathrm{Hask}$, with objects being the languages types. This category is known to have some unnice features. Quick example: With $\to$ and $\times$ etc., Hask is just almost Cartesian closed. A particular problem is the polymorphic term $\text{undefined}$, which is defined to be term of every type. So for exampel $\text{Int}$ has some numbers as terms, but also has an $\text{undefined}$ term, written $(\text{undefined}::\mathrm{Int})$. This prevents, for example, that the category has initial objects (i.e. there no analog to the "empty set"). Or when it comes to setting up the categorical product, the projections $\pi_1,\pi_2$ couldn't distinguish between the terms $(\langle\text{undefined},\text{undefined}\rangle::\mathrm{Int}\times\mathrm{Int})$ or $(\text{undefined}::\mathrm{Int}\times\mathrm{Int})$. Applying a projector on either will result in the value $(\text{undefined}::\mathrm{Int})$, spoiling uniqueness. People also set up smaller categories, e.g. by dropping undefined, to get the good categorical features back.
On the haskell.org page linked above, there is a motivation why the arrows are taken to be extensionally identified codable functions. It's implied that another language could have nicer hom-classes. I thought about it and here I asked for the specifics. The language on the haskell.org page is pretty sloppy, so I'm gonna summarize what I understand:
The identity for a type $a$ is the given by the code $(\mathrm{id} :: a\to a)$ and concatenation $f . g$, defined $\\x \mapsto f\, (g\, x)$. So
$(\mathrm{undefined} :: \mathrm{Int} \to \mathrm{Char})\,.\mathrm{id}$
is
$\\x\mapsto(\mathrm{undefined} :: \mathrm{Int} \to \mathrm{Char})\ x.$
When we want to set up hom-classes for $\bf{Hask}$, then we must have
$f\ \ =_{\bf{Hask}}\ \ f.\mathrm{id}\ \ =_\mathrm{Haskell}\ \ x\mapsto f(x)$.
But now Haskell is such that there are functions which can detect the non-extensive property of $(\mathrm{undefined} :: \mathrm{Int} \to \mathrm{Char})$ being the $\mathrm{undefined}$-term for the type $\mathrm{Int} \to \mathrm{Char}$. In particular, the function $\mathrm{seq}$ (which is implemented to make enforcement of strict evaluation possible) takes two arguments, "checks if the first is undefined", and if not then it returns the second argument. As implemented, it will return a different result when passed the extensionally equal functions $\mathrm{undefined} :: \mathrm{Int} \to \mathrm{Char}$ (which is the undefined term for $\mathrm{Int} \to \mathrm{Char}$) and $\\x \mapsto (\mathrm{undefined} :: \mathrm{Int} \to \mathrm{Char})\ x$.
So people define morphisms of $\bf{Hask}$ to be extensionally identified functions
$\forall x. f(x)=_\mathrm{Haskell} g(x)\implies f\ =_{\bf{Hask}}\ g.$
Questions:
- What would be the nicer equality? Given functions are first-class. Is it identification by value?
$\forall h. h(f)=_\mathrm{program} h(g)\implies f=_{\bf{semantics}}g,$
where $h$ are suitably typed functions.
I made that formula "$\forall h. h(f)=\dots$" just now. Does this proposition have a name?
the above suggests that enforcing strict evaluation might be to blame here - is this true? Would things be nicer without? If yes, is this a general deciding factor (not Haskell specific) when reasoning about the hom-classes?
We see that when it comes to passing functions as arguments, Haskell sees more than just Hask morphisms. Is there any way to make a programming language with categorical interpretation where programs and arrows are one-one?