Cartesian closed category

  ____    _    ____ _____ _____ ____ ___    _    _   _
 / ___|  / \  |  _ \_   _| ____/ ___|_ _|  / \  | \ | |
| |     / _ \ | |_) || | |  _| \___ \| |  / _ \ |  \| |
| |___ / ___ \|  _ < | | | |___ ___) | | / ___ \| |\  |
 \____/_/   \_\_| \_\|_|_|_____|____/___/_/   \_\_| \_|
 / ___| |   / _ \/ ___|| ____|  _ \
| |   | |  | | | \___ \|  _| | | | |
| |___| |__| |_| |___) | |___| |_| |
 \____|_____\___/|____/|_____|____/ ____  ___ _____ ____
 / ___|  / \|_   _| ____/ ___|/ _ \|  _ \|_ _| ____/ ___|
| |     / _ \ | | |  _|| |  _| | | | |_) || ||  _| \___ \
| |___ / ___ \| | | |__| |_| | |_| |  _ < | || |___ ___) |
 \____/_/   \_\_| |_____\____|\___/|_| \_\___|_____|____/

Categories come in all shapes and sizes. Among the most important and practically useful categories are Cartesian Closed Categories (CCCs), which provide the mathematical foundation for functional programming languages and lambda calculus. While basic categories give us objects and morphisms, Cartesian Closed Categories add crucial structure that allows us to work with products, exponentials, and higher-order functions in a formally rigorous way.

A Cartesian Closed Category extends the basic category structure with three fundamental capabilities that mirror the building blocks of computation:

1. Terminal Object - A unique unit object that serves as the categorical analogue of the unit type () in programming
2. Binary Products - Objects that represent pairs A x B, corresponding to tuple types in programming languages
3. Exponential Objects - Objects that represent function spaces B^A, corresponding to function types A -> B in programming

What makes these categories particularly powerful is that they provide a complete model for simply-typed lambda calculus. Every well-typed lambda expression can be interpreted as a morphism in a Cartesian Closed Category, and conversely, every morphism corresponds to a computable function.

The closed property is what enables higher-order functions - the ability to treat functions as first-class values that can be passed as arguments and returned as results. This closure property ensures that the category contains not just functions between objects, but also functions between function spaces themselves, creating the rich compositional structures.

Formal definition #

A Cartesian Closed Category (CCC) is a category C that has:

1. Terminal Object 1
2. Binary Products for all objects
3. Exponential Objects for all pairs of objects

Terminal Object #

An object 1 in category C is terminal if for every object A in C, there exists exactly one morphism from A to 1:

∀A ∈ Ob(C), ∃! !_A ∈ Hom(A, 1)

The morphism !_A: A -> 1 is called the unique morphism or terminal morphism from A to 1.

Universal Property: The terminal object is the unique (up to isomorphism) object that receives exactly one morphism from every object in the category.

Mathematical Notation #

Formally, a Cartesian Closed Category C satisfies:

∀A, B, X ∈ Ob(C):

1. Terminal Object: ∃! !_A: A -> 1

2. Products: ∃! ⟨f, g⟩: X -> A x B such that:

   • π₁ ∘ ⟨f, g⟩ = f
   • π₂ ∘ ⟨f, g⟩ = g

3. Exponentials: ∃! curry(f): X -> B^A such that:

• eval ∘ (curry(f) × id_A) = f (β-law)
• (Uniqueness) If h: X -> B^A and eval ∘ (h × id_A) = f then h = curry(f)

Category Laws #

A Cartesian Closed Category must satisfy several coherence conditions:

Terminal Object Laws:

• Uniqueness: If f: A -> 1 and g: A -> 1, then f = g

  This law ensures that the terminal object truly acts as a "unit" - there can be only one way to map any object to it. In programming terms, this means there's exactly one value of the unit type (), and every function that returns unit must return that same value.

• Identity: !₁ = id₁

  The unique morphism from the terminal object to itself is just the identity morphism. This is a consistency condition that ensures the terminal object behaves properly with respect to composition - the "do nothing" function from unit to unit is indeed the identity.

Product Laws:

• Pairing Identity (η-law for products): ⟨π₁, π₂⟩ = id_{A×B}

  This fundamental law states that if you take a product A x B, extract its components with the projections π₁ and π₂, and then pair them back together with ⟨π₁, π₂⟩, you get back exactly what you started with. In programming terms:

  (fst(pair), snd(pair)) == pair

  This law ensures that products don't lose information - they are lossless containers for their components.

• Fusion: ⟨f, g⟩ ∘ h = ⟨f ∘ h, g ∘ h⟩

  This law governs how pairing interacts with composition. It says that if you first apply some function h and then pair the results of f and g, that's the same as pairing the compositions f ∘ h and g ∘ h. In code:

  (f(h(x)), g(h(x))) == let y = h(x) in (f(y), g(y))

  This enables important optimizations and reasoning principles about data flow.

Exponential Laws:

• η-law (Eta): curry(eval) = id_{B^A}

  This law captures the essence of function spaces. The evaluation morphism eval takes a function and an argument and applies the function to the argument. When you curry this evaluation (treating the argument as a parameter), you get back the identity on the function space. In programming: curry(eval) = λf. f, meaning that λf. λx. f(x) is the same as λf. f.

  Functions are completely determined by their behavior on arguments.

• β-law (Beta): eval ∘ (curry(f) × id_A) = f

  This is the fundamental computation law for exponentials. It says that if you curry a function f and then evaluate it (by pairing with an argument), you get back the original function f. In programming:

  if g = curry(f), then g(a)(b) = f(a,b)

  This law ensures that currying and evaluation are true inverses, making the exponential a proper internal hom.

• Curry Fusion: curry(f ∘ (g × id_A)) = curry(f) ∘ g

  This law shows how currying distributes over composition. If you have a function f that operates on pairs where the first component has been transformed by g, currying this is the same as first currying f and then composing with g. In programming terms:

  curry(λ(x,y). f(g(x), y)) = λx. curry(f)(g(x))

  This enables powerful reasoning about partial application and function transformation.

Examples of Cartesian Closed Categories #

• Set (category of sets and functions)
• Types (the pure, total fragment of typed functional programming languages)

Programming Examples #

The pure, total subcategory of types and functions in a (pure) functional language forms a Cartesian Closed Category. (Effects like partiality, state, or IO generally break CCC structure unless modeled separately.) Here are detailed examples showing how the three fundamental constructions work in practice:

{-# LANGUAGE ExplicitForAll #-}

-- Terminal Object: Unit type ()
terminal :: ()
terminal = ()

-- Every type has exactly one morphism to the terminal object
toTerminal :: forall a. a -> ()
toTerminal _ = ()

-- Binary Products: Tuples (A, B)
type Product a b = (a, b)

-- Product construction and projections
makePair :: a -> b -> Product a b
makePair x y = (x, y)

firstProj :: Product a b -> a
firstProj (x, _) = x

secondProj :: Product a b -> b
secondProj (_, y) = y

-- Universal property of products: pairing morphism
pairing :: (x -> a) -> (x -> b) -> (x -> Product a b)
pairing f g = \x -> (f x, g x)

-- Exponential Objects: Function types A -> B
type Exponential a b = a -> b

-- Evaluation morphism
eval :: (Exponential a b, a) -> b
eval (f, x) = f x

-- Currying / Uncurrying
curry' :: (Product a b -> c) -> (a -> b -> c)
curry' f = \x y -> f (x, y)

uncurry' :: (a -> b -> c) -> (Product a b -> c)
uncurry' f = \(x, y) -> f x y

-- Composition (demonstrates exponential structure)
compose :: Exponential b c -> Exponential a b -> Exponential a c
compose f g x = f (g x)

addThree :: Int -> Int -> Int -> Int
addThree x y z = x + y + z

add5and7 :: Int -> Int
add5and7 = addThree 5 7

pipeline :: Int -> String
pipeline = show . (* 2) . (+ 1)

main :: IO ()
main = do
  putStrLn "=== Cartesian Closed Category Basic Constructions ==="
  putStrLn $ "terminal: " ++ show terminal
  putStrLn $ "toTerminal 42: " ++ show (toTerminal (42 :: Int))
  -- Explicit type annotations below avoid GHC -Wtype-defaults warnings
  let p :: (Int, Char)
      p = makePair (3 :: Int) 'a'
  putStrLn $ "makePair 3 'a': " ++ show p
  putStrLn $ "firstProj p: " ++ show (firstProj p)
  putStrLn $ "secondProj p: " ++ show (secondProj p)
  putStrLn $ "pairing (+1) (*2) 5: " ++ show (pairing ((+1) :: Int -> Int) ((*2) :: Int -> Int) (5 :: Int))
  putStrLn $ "eval ((+10),5): " ++ show (eval ((+10), 5 :: Int))
  putStrLn $ "curry'/uncurry' round trip (multiply): " ++
    let multiply :: (Int, Int) -> Int
        multiply (x,y) = x * y
        r = uncurry' (curry' multiply) (6 :: Int, 7 :: Int)
    in show r
  putStrLn $ "compose show (*2) 7: " ++ compose (show :: Int -> String) ((*2) :: Int -> Int) (7 :: Int)
  putStrLn $ "addThree 1 2 3: " ++ show (addThree (1 :: Int) (2 :: Int) (3 :: Int))
  putStrLn $ "add5and7 9: " ++ show (add5and7 (9 :: Int))
  putStrLn $ "pipeline 5: " ++ pipeline (5 :: Int)

// Terminal Object: void/undefined (unit type)
type Terminal = void;
const terminal: Terminal = undefined;

// Currying: ((A × B) => C) → (A => (B => C))
const curry = <A, B, C>(f: (pair: Product<A, B>) => C): (x: A) => (y: B) => C =>
  (x: A) => (y: B) => f([x, y]);

// Uncurrying: (A => (B => C)) → ((A × B) => C)
const uncurry = <A, B, C>(f: (x: A) => (y: B) => C): (pair: Product<A, B>) => C =>
  ([x, y]: Product<A, B>) => f(x)(y);

// Every type has exactly one function to terminal
const toTerminal = <A>(x: A): Terminal => undefined;

// Binary Products: Tuple types [A, B]
type Product<A, B> = [A, B];

// Product construction and projections
const makePair = <A, B>(x: A, y: B): Product<A, B> => [x, y];

const fst = <A, B>([x, _]: Product<A, B>): A => x;
const snd = <A, B>([_, y]: Product<A, B>): B => y;

// Universal property: pairing morphism
const pairing = <X, A, B>(
  f: (x: X) => A,
  g: (x: X) => B
): (x: X) => Product<A, B> =>
  (x: X) => [f(x), g(x)];

// Exponential Objects: Function types (A) => B
type Exponential<A, B> = (x: A) => B;

// Evaluation morphism
const evalMorphism = <A, B>(func: Exponential<A, B>, arg: A): B => func(arg);

// Alternative eval that takes a product
const evalProduct = <A, B>([func, arg]: Product<Exponential<A, B>, A>): B =>
  func(arg);

// Example 1: Terminal object and product projections
function example1() {
  const unitResult: Terminal = terminal;               // unique inhabitant
  const dropped: Terminal = toTerminal("anything");   // morphism to 1
  const pairAB = makePair<number, string>(42, "answer");
  const firstOfPair = fst(pairAB);                     // π₁
  const secondOfPair = snd(pairAB);                    // π₂
  console.log("Example 1 (terminal, products):", { unitResult, dropped, pairAB, firstOfPair, secondOfPair });
}

// Example 2: Universal property of products (pairing) + evaluation
function example2() {
  const build = pairing((x: number) => x + 1, (x: number) => x * 2); // ⟨f,g⟩
  const from5 = build(5); // [6,10]
  const incr: Exponential<number, number> = x => x + 1;
  const evaluated = evalMorphism(incr, 10);                 // eval(f, a)
  const evaluatedViaProduct = evalProduct([incr, 10]);      // eval ∘ pairing
  console.log("Example 2 (pairing, eval):", { from5, evaluated, evaluatedViaProduct });
}

// Example 3: Currying/Uncurrying isomorphism (exponential structure)
function example3() {
  const addPair = ([a,b]: Product<number, number>) => a + b;          // (A × B) → C
  const curried = curry(addPair);                                     // A → (B → C)
  const uncurried = uncurry(curried);                                 // round trip
  const roundTrip = uncurried([3,4]);                                 // 7
  // Partial application exhibits internal hom
  const add10 = curried(10);                                          // B → C
  const fifteen = add10(5);                                           // 15
  console.log("Example 3 (curry/uncurry):", { roundTrip, fifteen });
}

// Example 4: Higher-order functions and composition (exponential structure)
const compose = <A, B, C>(
  f: Exponential<B, C>,
  g: Exponential<A, B>
): Exponential<A, C> =>
  (x: A) => f(g(x));

function example4() {
  const processNumber: Exponential<number, string> = compose(
    compose(String, (x: number) => x * 2), // (*2) then to string
    (x: number) => x + 1                   // (+1) first
  );
  const result = processNumber(5); // "12"
  console.log("Example 4 (composition / pipeline):", { result });
}

// Example 5: Familiar higher-order operations as exponentials
function example5() {
  const numbers = [1, 2, 3, 4, 5];
  const doubled = numbers.map((x: number) => x * 2);        // map: functorial action
  const evens = numbers.filter((x: number) => x % 2 === 0); // predicate as exponential
  const sum = numbers.reduce((acc: number, x: number) => acc + x, 0); // fold uses evaluation repeatedly
  console.log("Example 5 (arrays & exponentials):", { doubled, evens, sum });
}

// Driver to run all examples in order
function runAllExamples() {
  example1();
  example2();
  example3();
  example4();
  example5();
}

runAllExamples();

C# (using generics and delegates)

using System;

// Terminal Object: Unit struct (equivalent to Haskell's ())
public struct Unit
{
    public static readonly Unit Value = new Unit();

    // Every type has exactly one function to Unit
    public static Unit ToTerminal<T>(T value) => Value;
}

// Binary Products: Generic tuple
public struct Product<A, B>
{
    public A First { get; }
    public B Second { get; }

    public Product(A first, B second)
    {
        First = first;
        Second = second;
    }

    // Projections
    public static A Fst(Product<A, B> product) => product.First;
    public static B Snd(Product<A, B> product) => product.Second;
}

// Exponential Objects: Generic delegates
public delegate TResult Exponential<T, TResult>(T input);

public static class CartesianClosedCategory
{
    // Product construction
    public static Product<A, B> MakePair<A, B>(A first, B second) =>
        new Product<A, B>(first, second);

    // Universal property: pairing morphism
    public static Func<X, Product<A, B>> Pairing<X, A, B>(
        Func<X, A> f,
        Func<X, B> g) =>
        x => new Product<A, B>(f(x), g(x));

    // Evaluation morphism
    public static TResult Eval<T, TResult>(
        Exponential<T, TResult> func,
        T argument) =>
        func(argument);

    // Alternative eval that takes a product
    public static TResult EvalProduct<T, TResult>(
        Product<Exponential<T, TResult>, T> pair) =>
        pair.First(pair.Second);

    // Currying: ((A × B) → C) → (A → (B → C))
    public static Func<A, Func<B, C>> Curry<A, B, C>(
        Func<Product<A, B>, C> f) =>
        a => b => f(new Product<A, B>(a, b));

    // Uncurrying: (A → (B → C)) → ((A × B) → C)
    public static Func<Product<A, B>, C> Uncurry<A, B, C>(
        Func<A, Func<B, C>> f) =>
        pair => f(pair.First)(pair.Second);

    // Function composition
    public static Exponential<A, C> Compose<A, B, C>(
        Exponential<B, C> f,
        Exponential<A, B> g) =>
        x => f(g(x));
}

class Program
{
    static void Main()
    {
        // Original function: Product<int, int> -> int
        Func<Product<int, int>, int> multiply =
            pair => pair.First * pair.Second;

        // Curry it: int -> (int -> int)
        var curriedMultiply = CartesianClosedCategory.Curry(multiply);

        // Uncurry it back: Product<int, int> -> int
        var uncurriedMultiply = CartesianClosedCategory.Uncurry(curriedMultiply);

        // Test the isomorphism
        var testPair = new Product<int, int>(6, 7);

        Console.WriteLine($"Original: {multiply(testPair)}");           // 42
        Console.WriteLine($"Curried: {curriedMultiply(6)(7)}");        // 42
        Console.WriteLine($"Uncurried: {uncurriedMultiply(testPair)}"); // 42

        // Partial application demonstrates exponential objects
        var multiplyBy5 = curriedMultiply(5);
        Console.WriteLine($"5 × 8 = {multiplyBy5(8)}"); // 40

        // Higher-order functions
        Exponential<int, int> addOne = x => x + 1;
        Exponential<int, int> double_ = x => x * 2;
        Exponential<int, string> toString = x => x.ToString();

        // Function composition
        var pipeline = CartesianClosedCategory.Compose(
            toString,
            CartesianClosedCategory.Compose(double_, addOne)
        );

        Console.WriteLine($"Pipeline(5) = {pipeline(5)}"); // "12"

        // Evaluation morphism
        Console.WriteLine($"Eval(addOne, 10) = {CartesianClosedCategory.Eval(addOne, 10)}"); // 11

        // Using pairing morphism
        var coordPairing = CartesianClosedCategory.Pairing<int, int, int>(
            x => x + 1,    // f: int -> int
            x => x * 2     // g: int -> int
        );

        var coords = coordPairing(5);
        Console.WriteLine($"Pairing(5) = ({coords.First}, {coords.Second})"); // (6, 10)
    }
}

Programming languages naturally form Cartesian Closed Categories:

1. Terminal Object: Unit types ((), void, Unit) that every type maps to uniquely
2. Products: Tuples, pairs, records that combine multiple values
3. Exponentials: Function types that enable higher-order programming
4. Universal Properties: Currying/uncurrying isomorphisms work perfectly

Formal implementation #

While the previous examples show how CCCs work in practice through ordinary programming, we can also implement the formal categorical structure using Haskell category theory libraries that provide these abstractions. Here's how the same concepts look using the established CCC typeclass:

{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeFamilyDependencies #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE ScopedTypeVariables #-}

import Control.Category
import Prelude hiding ((.), id, curry, uncurry)
import Data.Kind (Type)

-- Cartesian structure (products)
class Category k => Cartesian k where
  -- Injective associated type: the product object uniquely determines its factors
  type Product k a b = p | p -> a b
  exl   :: k (Product k a b) a
  exr   :: k (Product k a b) b
  (&&&) :: k x a -> k x b -> k x (Product k a b)
  infixr 3 &&&

-- Exponentials / CCC structure
class Cartesian k => CCC k where
  type Exp k :: Type -> Type -> Type
  apply   :: k (Product k (Exp k a b) a) b                 -- eval
  curryC  :: k (Product k a b) c -> k a (Exp k b c)         -- curry
  uncurryC :: k a (Exp k b c) -> k (Product k a b) c        -- uncurry

-- Instance for ordinary functions ----------------------------------
instance Cartesian (->) where
  type Product (->) a b = (a, b)
  exl = fst
  exr = snd
  (f &&& g) x = (f x, g x)

instance CCC (->) where
  type Exp (->) = (->)
  apply (f, a) = f a
  curryC f a b = f (a, b)
  uncurryC f (a, b) = f a b

-- Example usage with the standard interface ------------------------
libraryExample :: IO ()
libraryExample = do
  putStrLn "=== Using Simple CCC Interface ==="
  let combine :: (Int, String) -> String
      combine (n, s) = s ++ " " ++ show n
  let curriedCombine = curryC combine           -- Int -> String -> String
  let testFunc = curriedCombine 42              -- String -> String
  let result = apply (testFunc, "Answer:")
  putStrLn $ "apply (curryC combine 42, \"Answer:\") = " ++ result
  let uncurriedBack = uncurryC curriedCombine   -- (Int,String) -> String
  putStrLn $ "uncurryC (curryC combine) (100, \"Count:\") = " ++ uncurriedBack (100, "Count:")
  -- Demonstrate product projections & pairing with explicit types to avoid defaulting warnings
  let samplePair :: (Int, String)
      samplePair = (10 :: Int, "ten")
  putStrLn $ "exl (10,\"ten\") = " ++ show (exl samplePair)
  putStrLn $ "exr (10,\"ten\") = " ++ show (exr samplePair)
  let paired :: (Int, String)
      paired = ((+1) &&& show) (7 :: Int)
  putStrLn $ "((+1) &&& show) 7 = " ++ show paired

-- Abstract composition using ordinary categorical composition ------
abstractCCCLibrary :: (CCC k) => (a `k` b) -> (b `k` c) -> (a `k` c)
abstractCCCLibrary f g = g . f

-- Advantages --------------------------------------------------------
exampleAdvantages :: IO ()
exampleAdvantages = do
  putStrLn "\n=== CCC Advantages ==="
  putStrLn "• Functions as exponentials (internal homs)"
  putStrLn "• Products + exponentials model simply typed lambda calculus"
  putStrLn "• Currying / uncurrying"
  -- Simple arithmetic example
  let simple = curryC (\(x,y) -> x + y) :: Int -> Int -> Int
  putStrLn $ "curryC (\\(x,y)->x+y) 3 4 = " ++ show (simple 3 4)

main :: IO ()
main = do
  libraryExample
  exampleAdvantages
  putStrLn "\nComposition example: (show . (+1)) 5 ="
  let comp :: Int -> String
      comp = abstractCCCLibrary (+1) show
  putStrLn (comp 5)

Hom-sets Connection to Cartesian Closed Categories #

Hom-sets become especially powerful in Cartesian Closed Categories, where they are related to exponential objects through the internal-hom adjunction.

In a CCC, exponentials internalize morphisms.

The fundamental connection is the natural bijection Hom(X × A, B) ≅ Hom(X, B^A).

Specializing to the terminal object gives Hom(A, B) ≅ Hom(1, B^A), so ordinary morphisms A -> B correspond to global elements of the exponential object B^A.

{-# LANGUAGE RankNTypes #-}

-- The Hom-set Hom(A, B) is represented externally by the function type A -> B
type Hom a b = a -> b

-- In Haskell, A -> B is also the exponential object B^A
-- The key CCC statement is the currying bijection below

-- The currying isomorphism: Hom(A × B, C) ≅ Hom(A, C^B)
-- In Haskell types: ((A, B) -> C) ≅ (A -> (B -> C))

-- Higher-order functions work with Hom-sets as first-class objects
mapHom :: Hom b c -> [Hom a b] -> [Hom a c]
mapHom f functions = map (f .) functions  -- Function composition

-- Natural transformations between Hom-sets
-- Example: pre-composition with a function g :: A -> B
-- gives a natural transformation: Hom(B, C) -> Hom(A, C)
preCompose :: (a -> b) -> (b -> c) -> (a -> c)
preCompose g f = f . g

-- Example: post-composition with a function f :: B -> C
-- gives a natural transformation: Hom(A, B) -> Hom(A, C)
postCompose :: (b -> c) -> (a -> b) -> (a -> c)
postCompose f g = f . g

-- Comprehensive demonstration of Hom-sets in Cartesian Closed Categories
main :: IO ()
main = do
  putStrLn "=== Hom-sets in Cartesian Closed Categories ==="
  putStrLn ""

  -- 1. Currying isomorphism demonstration
  putStrLn "1. Currying Isomorphism: Hom(A × B, C) ≅ Hom(A, C^B)"
  -- Left side: Hom(A × B, C) - functions from pairs to C
  let addPair :: (Int, Int) -> Int
      addPair (x, y) = x + y

  -- Right side: Hom(A, C^B) - functions from A to functions (B -> C)
  let addCurried :: Int -> (Int -> Int)
      addCurried = curry addPair

  -- They represent the same mathematical relationship
  print $ addPair (5, 3)        -- 8
  print $ addCurried 5 3        -- 8
  -- The isomorphism is witnessed by curry/uncurry
  print $ uncurry addCurried (5, 3)  -- 8
  putStrLn ""

  -- 2. Higher-order function manipulation
  putStrLn "2. Higher-order Function Manipulation"
  let functions :: [Int -> Int]
      functions = [(+1), (*2), (\x -> x*x)]  -- List of Hom(Int, Int)

  let showFunction :: Int -> String
      showFunction = show  -- Hom(Int, String)

  -- Apply showFunction after each function: [Hom(Int, String)]
  let stringFunctions = mapHom showFunction functions

  -- Test the transformed functions
  putStrLn "Transformed functions applied to 5:"
  mapM_ (\f -> print (f 5)) stringFunctions  -- "6", "10", "25"
  putStrLn ""

  -- 3. Exponential objects as function spaces
  putStrLn "3. Exponential Objects as Function Spaces"
  -- B^A represents the space of all functions A -> B
  let intToString :: [Int -> String]  -- Some functions in String^Int
      intToString = [show, \x -> "num: " ++ show x, \x -> replicate x 'x']

  -- Functions can be manipulated like any other data
  let selectedFunction = head intToString  -- Pick a function
  putStrLn $ "Selected function(42) = " ++ selectedFunction 42  -- "42"

  -- Composition creates new functions in the space
  let composed = map (("Result: " ++) .) intToString  -- [String^Int]
  putStrLn $ "Composed function(7) = " ++ head composed 7  -- "Result: 7"
  putStrLn ""

  -- 4. Natural transformations demonstration
  putStrLn "4. Natural Transformations Between Hom-sets"
  let doubleIt :: Int -> Int
      doubleIt = (*2)

  let originalFunc :: Int -> String
      originalFunc = \x -> "Value: " ++ show x

  -- Pre-composition: apply doubleIt before originalFunc
  let preComposed = preCompose doubleIt originalFunc
  putStrLn $ "Original function(5) = " ++ originalFunc 5      -- "Value: 5"
  putStrLn $ "Pre-composed function(5) = " ++ preComposed 5   -- "Value: 10"

  -- Post-composition: apply show after (+1)
  let addOne :: Int -> Int
      addOne = (+1)
  let postComposed = postCompose show addOne
  putStrLn $ "Post-composed function(5) = " ++ postComposed 5  -- "6"
  putStrLn ""

  -- 5. The key CCC bijection
  putStrLn "5. Key CCC Bijection: Hom(X × A, B) ≅ Hom(X, B^A)"
  putStrLn "In Haskell (a Cartesian Closed Category):"
  putStrLn "- Types are objects"
  putStrLn "- Functions (A -> B) are morphisms in Hom(A,B)"
  putStrLn "- Function types (A -> B) are also objects (exponentials B^A)"
  putStrLn "- Specializing X = 1 gives Hom(A,B) ≅ Hom((), B^A)"
  putStrLn "- This makes functions first-class: they can be arguments and results"
  putStrLn ""

  -- 6. Demonstrating functions as both morphisms and objects
  putStrLn "6. Functions as Both Morphisms and Objects"
  let functionAsMorphism :: Int -> String
      functionAsMorphism = show  -- This is a morphism in Hom(Int, String)

  -- The same function type as objects that can be manipulated
  let functionsAsObjects :: [Int -> String]
      functionsAsObjects = [functionAsMorphism, \x -> "Num: " ++ show x]

  -- Higher-order function that processes functions (treating them as objects)
  let testAllFunctions :: [Int -> String] -> Int -> [String]
      testAllFunctions funcs x = map ($ x) funcs

  let results = testAllFunctions functionsAsObjects 42
  putStrLn $ "Testing functions as objects with 42: " ++ show results
  -- ["42", "Num: 42"]

// The Hom-set Hom(A, B) corresponds to function type (A) => B
type Hom<A, B> = (a: A) => B;

// In a CCC, exponentials are characterized by the natural bijection
// Hom(X × A, B) ≅ Hom(X, B^A)
type Exponential<A, B> = Hom<A, B>;  // They're the same!

// The currying isomorphism: Hom(A × B, C) ≅ Hom(A, Hom(B, C))
type Product<A, B> = [A, B];
type CurryingIsomorphism<A, B, C> = {
  left: Hom<Product<A, B>, C>;      // Functions from pairs
  right: Hom<A, Hom<B, C>>;         // Curried functions
};

// Demonstrating the isomorphism
const curryingDemo = () => {
  // Left side: Hom([number, number], number)
  const multiply: Hom<Product<number, number>, number> =
    ([x, y]) => x * y;

  // Right side: Hom(number, Hom(number, number))
  const curryMultiply: Hom<number, Hom<number, number>> =
    (x) => (y) => x * y;

  // The isomorphism in action
  console.log(multiply([6, 7]));      // 42
  console.log(curryMultiply(6)(7));   // 42

  // curry/uncurry witness the isomorphism
  const curry = <A, B, C>(f: Hom<Product<A, B>, C>): Hom<A, Hom<B, C>> =>
    (a) => (b) => f([a, b]);

  const uncurry = <A, B, C>(f: Hom<A, Hom<B, C>>): Hom<Product<A, B>, C> =>
    ([a, b]) => f(a)(b);

  const curried = curry(multiply);
  const uncurried = uncurry(curryMultiply);

  console.log(curried(6)(7));        // 42
  console.log(uncurried([6, 7]));    // 42
};

// Higher-order functions manipulate Hom-sets
const mapHom = <A, B, C>(
  f: Hom<B, C>,
  functions: Hom<A, B>[]
): Hom<A, C>[] =>
  functions.map(g => (x: A) => f(g(x)));  // Function composition

// Example: Working with collections of functions
const functionManipulation = () => {
  // A collection of functions (elements of Hom(number, number))
  const numberFunctions: Hom<number, number>[] = [
    x => x + 1,
    x => x * 2,
    x => x * x
  ];

  // Transform them with another function (Hom(number, string))
  const toString: Hom<number, string> = x => `Result: ${x}`;

  // Get new functions (elements of Hom(number, string))
  const stringFunctions = mapHom(toString, numberFunctions);

  // Test the transformed functions
  stringFunctions.forEach((f, i) => {
    console.log(`Function ${i}(5) = ${f(5)}`);
    // "Function 0(5) = Result: 6"
    // "Function 1(5) = Result: 10"
    // "Function 2(5) = Result: 25"
  });
};

// Exponential objects as function spaces
const exponentialObjects = () => {
  // String^number represents all functions from number to string
  const stringFromNumber: Hom<number, string>[] = [
    x => x.toString(),
    x => `The number ${x}`,
    x => "*".repeat(x),
    x => x < 0 ? "negative" : x > 0 ? "positive" : "zero"
  ];

  // Functions are first-class - can be stored, passed, returned
  const selectFunction = (index: number): Hom<number, string> =>
    stringFromNumber[index] || (x => `Unknown: ${x}`);

  const selectedFunc = selectFunction(2);
  console.log(selectedFunc(5)); // "*****"

  // Function composition creates new exponential objects
  const addPrefix: Hom<string, string> = s => `Output: ${s}`;
  const composedFunctions = stringFromNumber.map(f =>
    (x: number) => addPrefix(f(x))
  );

  console.log(composedFunctions[1](42)); // "Output: The number 42"
};


// Demonstrating hom-functor behavior via precomposition
const homCategory = () => {
  // Fixing the codomain and varying the domain gives a contravariant hom-functor.
  // Precomposition is a natural way to move between the resulting hom-sets.

  // Identity natural transformation: Hom(A,B) -> Hom(A,B)
  const idHom = <A, B>(f: Hom<A, B>): Hom<A, B> => f;

  // Example natural transformation: pre-composition
  // Given g: A -> B, get natural transformation Hom(B,C) -> Hom(A,C)
  const preComposition = <A, B, C>(g: Hom<A, B>) =>
    (f: Hom<B, C>): Hom<A, C> => (x: A) => f(g(x));

  // Example usage
  const double: Hom<number, number> = x => x * 2;
  const toString: Hom<number, string> = x => `Value: ${x}`;
  const preComposeWithDouble = preComposition(double);
  const composedFunction = preComposeWithDouble(toString);
  console.log(`Pre-composed function(5) = ${composedFunction(5)}`); // "Value: 10"

  console.log("Hom-functors fit into functor categories, where natural transformations compare them");
};

// The fundamental insight: exponentials internalize morphisms via a natural bijection
const fundamentalTheorem = () => {
  console.log("=== Key CCC Bijection: Hom(X × A, B) ≅ Hom(X, B^A) ===");
  console.log("In TypeScript (modeling a Cartesian Closed Category):");
  console.log("- Types are objects");
  console.log("- Function types (A) => B are morphisms in Hom(A,B)");
  console.log("- Function types (A) => B are also objects (exponentials B^A)");
  console.log("- Setting X to the unit object recovers Hom(A,B) ≅ Hom(1, B^A)\n");

  // Demonstrate that function types are both morphisms AND objects
  const functionAsMorphism: Hom<number, string> = x => x.toString();  // Morphism in Hom(number, string)

  // The same function type as objects that can be manipulated
  const functionsAsObjects: Hom<number, string>[] = [
    functionAsMorphism,  // Our function is now data!
    x => `Number: ${x}`,
    x => "*".repeat(Math.max(0, x)),
    x => x < 0 ? "negative" : x > 0 ? "positive" : "zero"
  ];

  console.log("Functions as objects - stored in an array:");
  functionsAsObjects.forEach((func, index) => {
    console.log(`  Function ${index}(3) = "${func(3)}"`);
  });

  // Higher-order function that takes functions as arguments (objects)
  // and returns a function (object). In a CCC, exponentials are what
  // internalize these function spaces as objects.
  const testFunction: Hom<Hom<number, string>, string> = f => f(42);

  console.log("\nHigher-order function applying each function to 42:");
  functionsAsObjects.forEach((func, index) => {
    console.log(`  Testing function ${index}: "${testFunction(func)}"`);
  });

  // Functions can be returned from other functions (function factories)
  const createFormatter = (prefix: string): Hom<number, string> =>
    x => `${prefix}: ${x}`;

  const errorFormatter = createFormatter("ERROR");
  const infoFormatter = createFormatter("INFO");

  console.log("\nFunction factories creating new functions:");
  console.log(`  ${errorFormatter(404)}`);  // "ERROR: 404"
  console.log(`  ${infoFormatter(200)}`);   // "INFO: 200"

  // The key insight: functions are simultaneously structure and data
  console.log("\n🔑 Key Insight:");
  console.log("Functions are simultaneously:");
  console.log("- MORPHISMS: They represent computational relationships");
  console.log("- OBJECTS: They can be manipulated as first-class data");
  console.log("This dual nature is what makes functional programming powerful!");
};

curryingDemo();
functionManipulation();
exponentialObjects();
homCategory();
fundamentalTheorem();

using System;
using System.Collections.Generic;
using System.Linq;

// The Hom-set Hom(A, B) corresponds to delegate types
public delegate TResult Hom<T, TResult>(T input);

// In a CCC, exponentials are characterized by the natural bijection
// Hom(X × A, B) ≅ Hom(X, B^A)
public delegate TResult Exponential<T, TResult>(T input);

// Product type for demonstrating currying
public struct Product<A, B>
{
    public A First { get; }
    public B Second { get; }

    public Product(A first, B second)
    {
        First = first;
        Second = second;
    }
}

public static class HomSetExamples
{
    // The currying isomorphism: Hom(A × B, C) ≅ Hom(A, Hom(B, C))
    public static void CurryingIsomorphism()
    {
        Console.WriteLine("=== Currying Isomorphism ===");

        // Left side: Hom(Product<int, int>, int)
        Hom<Product<int, int>, int> multiply =
            pair => pair.First * pair.Second;

        // Right side: Hom(int, Hom(int, int))
        Hom<int, Hom<int, int>> curryMultiply =
            x => y => x * y;

        // Demonstrate the isomorphism
        var testPair = new Product<int, int>(6, 7);
        Console.WriteLine($"multiply(6,7) = {multiply(testPair)}");           // 42
        Console.WriteLine($"curryMultiply(6)(7) = {curryMultiply(6)(7)}");   // 42

        // curry/uncurry witness the isomorphism
        var curried = Curry(multiply);
        var uncurried = Uncurry(curryMultiply);

        Console.WriteLine($"curried(6)(7) = {curried(6)(7)}");               // 42
        Console.WriteLine($"uncurried(6,7) = {uncurried(testPair)}");        // 42
    }

    // Curry: Hom(A × B, C) -> Hom(A, Hom(B, C))
    public static Hom<A, Hom<B, C>> Curry<A, B, C>(Hom<Product<A, B>, C> f) =>
        a => b => f(new Product<A, B>(a, b));

    // Uncurry: Hom(A, Hom(B, C)) -> Hom(A × B, C)
    public static Hom<Product<A, B>, C> Uncurry<A, B, C>(Hom<A, Hom<B, C>> f) =>
        pair => f(pair.First)(pair.Second);

    // Higher-order functions manipulate Hom-sets
    public static IEnumerable<Hom<A, C>> MapHom<A, B, C>(
        Hom<B, C> f,
        IEnumerable<Hom<A, B>> functions) =>
        functions.Select(g => new Hom<A, C>(x => f(g(x))));

    // Example: Working with collections of functions
    public static void FunctionManipulation()
    {
        Console.WriteLine("\n=== Function Manipulation ===");

        // Collection of functions (elements of Hom(int, int))
        var numberFunctions = new List<Hom<int, int>>
        {
            x => x + 1,
            x => x * 2,
            x => x * x
        };

        // Transform with another function (Hom(int, string))
        Hom<int, string> toString = x => $"Result: {x}";

        // Get new functions (elements of Hom(int, string))
        var stringFunctions = MapHom(toString, numberFunctions).ToList();

        // Test the transformed functions
        for (int i = 0; i < stringFunctions.Count; i++)
        {
            Console.WriteLine($"Function {i}(5) = {stringFunctions[i](5)}");
        }
    }

    // Exponential objects as function spaces
    public static void ExponentialObjects()
    {
        Console.WriteLine("\n=== Exponential Objects ===");

        // string^int represents all functions from int to string
        var stringFromInt = new List<Exponential<int, string>>
        {
            x => x.ToString(),
            x => $"The number {x}",
            x => new string('*', Math.Max(0, x)),
            x => x < 0 ? "negative" : x > 0 ? "positive" : "zero"
        };

        // Functions are first-class - can be stored, passed, returned
        Hom<int, Exponential<int, string>> selectFunction =
            index => index < stringFromInt.Count ? stringFromInt[index] :
                     (x => $"Unknown: {x}");

        var selectedFunc = selectFunction(2);
        Console.WriteLine($"Selected function(5) = {selectedFunc(5)}"); // *****

        // Function composition creates new exponential objects
        Hom<string, string> addPrefix = s => $"Output: {s}";
        var composedFunctions = stringFromInt
            .Select(f => new Exponential<int, string>(x => addPrefix(f(x))))
            .ToList();

        Console.WriteLine($"Composed function(3) = {composedFunctions[1](3)}");
        // "Output: The number 3"
    }

    // Natural transformations between Hom-sets
    // eta: ∀A,B. A -> Hom(B, A)  (constant function)
    public static Hom<B, A> Eta<A, B>(A value) => _ => value;

    // Demonstrating hom-functor behavior via precomposition
    public static void HomCategory()
    {
        Console.WriteLine("\n=== Hom-functor Action by Precomposition ===");

        // Identity natural transformation: Hom(A,B) -> Hom(A,B)
        Hom<Hom<int, string>, Hom<int, string>> idHom = f => f;

        // Example of natural transformation: pre-composition
        // Given g: A -> B, get (g*): Hom(B,C) -> Hom(A,C)
        // where (g*)(f) = f ∘ g
        Hom<int, int> doubleIt = x => x * 2;
        Hom<Hom<int, string>, Hom<int, string>> preCompose =
            f => x => f(doubleIt(x));

        Hom<int, string> originalFunction = x => $"Value: {x}";
        var transformedFunction = preCompose(originalFunction);

        Console.WriteLine($"Original(5) = {originalFunction(5)}");      // "Value: 5"
        Console.WriteLine($"Transformed(5) = {transformedFunction(5)}"); // "Value: 10"

        Console.WriteLine("Hom-functors fit into functor categories, where natural transformations compare them");
    }

    // The fundamental insight: exponentials internalize morphisms via a natural bijection
    public static void FundamentalTheorem()
    {
        // Demonstrate that function types are both morphisms AND objects
        Hom<int, string> functionAsMorphism = x => x.ToString();  // Morphism in Hom(int, string)

        // The same function type as an object that can be manipulated
        var functionsAsObjects = new List<Hom<int, string>>
        {
            functionAsMorphism,  // Our function is now data!
            x => $"Number: {x}",
            x => new string('X', x)
        };

        // Higher-order function that takes functions as arguments (objects)
        // and returns a function (object) - this is only possible because
        // In a CCC, exponentials internalize these function spaces as objects
        Hom<Hom<int, string>, string> testFunction = f => f(42);

        foreach (var func in functionsAsObjects)
        {
            Console.WriteLine($"Testing function: {testFunction(func)}");
        }
    }
}

class Program
{
    static void Main()
    {
        Console.WriteLine("Hom-sets Connection to Cartesian Closed Categories\n");

        HomSetExamples.CurryingIsomorphism();
        HomSetExamples.FunctionManipulation();
        HomSetExamples.ExponentialObjects();
        HomSetExamples.HomCategory();
        HomSetExamples.FundamentalTheorem();
    }
}

Key Insights #

These examples demonstrate the profound connection between Hom-sets and Cartesian Closed Categories:

1. Internalization: Exponential objects B^A internalize morphisms through the natural bijection Hom(X × A, B) ≅ Hom(X, B^A)
2. First-Class Functions: Functions are both morphisms (structure) and objects (data)
3. Currying Isomorphism: Hom(A × B, C) ≅ Hom(A, C^B) enables partial application and higher-order programming
4. Function Spaces: Exponential objects represent entire "spaces" of functions that can be manipulated computationally
5. Natural Transformations: Systematic ways to transform between hom-functors while preserving structure

This connection is what makes functional programming possible - it allows us to treat functions as data while maintaining their computational meaning.

Visualizing Cartesian Closed Categories #

1. TERMINAL OBJECT (1)
   Every object has exactly one morphism to terminal

     A --- !_A ---> 1 <----- !_B ---- B
                    │
                    │ !_C
                    │
                    C

2. BINARY PRODUCTS (A × B)
   Universal property: unique pairing morphism

            f │          │ g
              ▼          ▼
         X -- ⟨f,g⟩ --> A × B
              ╱           │ │
           π₁╱            │ │π₂
           ╱              │ │
          ▼               ▼ ▼
         A               A   B

     Laws: π₁ ∘ ⟨f,g⟩ = f  and  π₂ ∘ ⟨f,g⟩ = g

3. EXPONENTIAL OBJECTS (B^A)
   Function spaces as objects with evaluation morphism

     curry(f) │
              ▼
         X ------------> B^A
         │                │
      f  │              eval
         │                │
         ▼                ▼
         C <--------- B^A × A

     Law: eval ∘ (curry(f) × id_A) = f

4. CURRYING ISOMORPHISM - The Heart of CCCs

     Hom(A × B, C) ≅ Hom(A, C^B)

       f: A×B → C
           ↕ curry/uncurry
       g: A → C^B

     This makes functions first-class!

5. FUNCTION COMPOSITION AND HIGHER-ORDER STRUCTURE

     A -- f --> B --g --> C   ≡   A --- g∘f ---> C

     Composition as exponential object:
     compose: C^B × B^A → C^A

 6. TYPICAL PROGRAMMING CONSTRUCTS

     Terminal:     () or Unit
     Products:     (A, B), tuples, records
     Exponentials: A → B, function types

     map: (A → B) → ([A] → [B])

         f
    A ------> B
    │         │
    │list     │list
    ▼         ▼
   [A] ─map(f)─> [B]

Conclusion #

Cartesian Closed Categories provide the theoretical foundation for functional programming and lambda calculus. Through our exploration, we've seen how three simple requirements—terminal objects, binary products, and exponential objects—create a rich framework that directly corresponds to the core features of modern programming languages.

The power of CCCs lies in their universal properties, which ensure that:

• Terminal objects provide a canonical "unit" that every other object can map to uniquely
• Products give us a systematic way to combine data while preserving all information through projections
• Exponentials elevate functions to first-class status as objects in their own right

CCCs translate directly into the programming constructs we use daily: unit types, tuples, and function types.

The fundamental isomorphism Hom(A × B, C) ≅ Hom(A, C^B) is perhaps the most important insight CCCs offer. This equivalence:

• Explains why currying "just works" in functional languages
• Reveals the deep connection between function arguments and function spaces
• Demonstrates that multi-argument functions are really single-argument functions returning functions

CCCs resolve the apparent paradox of functions in programming: they are simultaneously computational processes (morphisms) and manipulable data (objects). This duality enables:

• Higher-order programming - functions that operate on other functions
• Function composition - building complex operations from simple ones
• Meta-programming - programs that generate and transform other programs
• Functional abstractions - patterns like map, filter, and fold

Source code #

Reference implementation (opens in a new tab)

References

1. Cartesian closed category (Wikipedia) (opens in a new tab)
2. Cartesian closed category (nLab) (opens in a new tab)

Continue exploring

• Product, coproduct & exponential Type constructs formation Shared tags: currying, category-theory · Same collection · Same subsection
• Applicative functor Applying functions inside a context Shared tags: category-theory, functional-programming · Same collection
• Category Category as a primary building block Shared tags: category-theory · Same collection · Same subsection