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


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.

  • $\begingroup$ Are you lamenting about "Hask" or about "global element"? Global element makes perfect sense, if you think about programs geometrically. $\endgroup$ – Andrej Bauer May 6 '18 at 9:14
  • $\begingroup$ Hask. I find it very twee. $\endgroup$ – Neel Krishnaswami May 6 '18 at 19:54
  • $\begingroup$ Hasky would be worse. $\endgroup$ – Andrej Bauer May 6 '18 at 23:55

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.