Take the 2-minute tour ×
Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. It's 100% free, no registration required.

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$.

enter image description here

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?

share|improve this question
    
As for the first one, I think perhaps Identity of Indiscernibles might be the right term. At least, in a course on the lambda calculus and type theory that I once took, the lecturers (Henk Barendregt and Freek Wiedijk) called it that. –  tci Sep 17 at 23:46
    
@tci: Thanks, this looks like it. –  NikolajK Sep 18 at 7:59

Your Answer

 
discard

By posting your answer, you agree to the privacy policy and terms of service.

Browse other questions tagged or ask your own question.