Curry Howard correspondence and equality

2
votes

A while ago I read that the function type a -> b corresponds to the relation a ≤ b, or is it a ≥ b? This makes sense to me because two types are isomorphic if we have a bijection between them (i.e. (a ≈ b) ≡ (a -> b, b -> a)). Similarly, (a = b) ≡ (a ≤ b) ∧ (a ≥ b).

I know that this is not the Curry-Howard-Lambek correspondence (i.e. the correspondence between type theory, logic and category theory). It's the correspondence between type theory and something else. I want to know learn more about this correspondence. Could somebody point me in the right direction?

I know that this doesn't seem like a programming question but it is related to programming and I'm hoping that some functional programmer knows more about it and can point me in the right direction.

2
haskellloginfunctional-programmingtype-theorycurry-howard
The "type system" (i.e., types with their proof semantics given by the CH isomorphism) can be described by several mathematical structures, for example a Cartesian closed category or a distributive lattice. In this case you are taking the preorder formed by (Type, ->), ie, for all types x,y we say that x is less than or equal y iff there exists a function of type x -> y. You also use that , corresponds to logical and (this comes from the lattice structure). - user2407038

2 Answers

9
votes

Every pre-ordered set forms a category. Let (S, «) be a pre-ordered set. Define a category C whose objects are the elements of S and with Hom(a, b) inhabited by (a, b) if a « b and uninhabited otherwise. Define composition the only way you possibly can. The category laws follow immediately from the transitivity and reflexivity of the pre-order.

A lattice, in particular, will form a category admitting finite products and coproducts. A bounded lattice will form one with initial and final objects.

Types and functions in a sufficiently well-behaved functional language also form a category with finite products and coproducts, and initial and final objects. So if you squint out to a categorical blur, these things will start to look vaguely similar.

3
votes

(This is more a comment than an answer, but I need more space.)

The type a -> b corresponds to a <= b. This is useful, e.g., to speak about fixed points at the type level, which are needed to properly define recursive types (lists, trees, ...).

Recall how recursion is solved, without categories. In domain theory, given a function f :: a -> a we look for a least x satisfying f x = x (least fixed point). This turns out to also be the least x satisfying f x <= x (least prefixed point). We then get the induction principle

f y <= y  ==> fix f <= y

which basically states that, if we have any prefixed point y, then the least (pre)fixed point fix f must be less than y -- indeed, it is the least!

Now, let's sprinkle some category powder over that. Implication becomes a -> arrow, and <= also becomes ->. We get

(f y -> y) -> fix f -> y

Looks familiar, where did I see that...? Ah!

newtype Fix f = Fix { unFix :: f (Fix f) }
cata :: Functor f => (f y -> y) -> Fix f -> y
cata g = g . fmap (cata g) . unFix

Hence, the cata general eliminator/catamorphism is just a category-empowered version of the good old induction principle.

Note how domain points y are now object in our category (i.e. types). Also, functions f must be applicable to y, so these are not morphisms in our category (which would be function values :: A -> B, from some type to some type), but correspond to functors int the category of types (mapping types to types :: * -> *).