What are values relative to Hask?

Question

According to ncatlab's page on category theory and haskell, "we can identify a subset of Haskell called Hask that is often used to identify concepts used in basic category theory. One considers Haskell types as objects of a category whose morphisms are extensionally identified Haskell functions."

So types are objects, and functions are morphisms. How, then, does a value, such as the list [1,2,3] or the boolean "true", fit into a category-theoretic definition of Haskell? (I realize that lists, as monads, are presumably different in any category theoretical representation than booleans, which could be described as a coproduct, but I don't understand how the actual values in either case are related to the definition of Hask).

Answer 1

At the level of precision used in the nlab page, values are global elements -- i.e., a value of type $A$ corresponds to a morphism $1 \to A$.

If you want to be serious about this, there are some technicalities to account for:

1. First, actual Haskell does not actually form a category in the sense that we would hope -- the seq operator breaks a lot of the program equivalences we need. However, if it were removed, then the pure fragment of Haskell would form a category (basically corresponding to the category of domains and continuous functions).

2. However, global elements in "Hask" (how I hate this terminology!) are not precisely values, since the nonterminating computation is an inhabitant of every type, and so for every type $A$ there is a map $\mathsf{loop}_A : 1 \to A$ which just runs forever.

   If you want to distinguish between values and nonterminating computations, then you need a somewhat more complicated setup, corresponding to the models of Paul Blain Levy's call-by-push-value.

   There, you work with two categories -- one, a category of values, and the other, a category of computations, with an adjunction which gives you two functors, one embedding values into computations and the other embedding computations into values.