<p>At the level of precision used in the nlab page, values are <a href="https://en.wikipedia.org/wiki/Global_element" rel="noreferrer"><em>global elements</em></a> -- i.e., a value of type $A$ corresponds to a morphism $1 \to A$.  </p>

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

<ol>
<li><p>First, actual Haskell does not actually form a category in the sense that we would hope -- the <code>seq</code> 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). </p></li>
<li><p>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. </p>

<p>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 <a href="https://www.cs.bham.ac.uk/~pbl/papers/hosc05.pdf" rel="noreferrer"><em>call-by-push-value</em></a>. </p>

<p>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.</p></li>
</ol>

CC BY-SA 4.0
2018-05-06T09:14:36.777Z
Are you lamenting about "Hask" or about "global element"? Global element makes perfect sense, if you think about programs geometrically.
Andrej Bauer
CC BY-SA 4.0
2018-05-06T19:54:18.590Z
Hask. I find it very twee.
Neel Krishnaswami
CC BY-SA 4.0
2018-05-06T23:55:17.697Z
Hasky would be worse.
Andrej Bauer
CC BY-SA 4.0
2018-05-03T10:29:16.123Z
2018-05-03T10:29:16.123Z
Neel Krishnaswami
<p>According to ncatlab's page on category theory and haskell, 
"<em>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.</em>"</p>

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

CC BY-SA 4.0
2018-05-03T04:53:23.090Z
See this stack overflow post https://stackoverflow.com/q/17380379/6511076
Mark Schultz-Wu
CC BY-SA 4.0
2018-05-03T16:24:59.553Z
also worth reading: http://blog.sigfpe.com/2009/10/what-category-do-haskell-types-and.html
Noam Zeilberger
CC BY-SA 4.0
2018-05-04T14:45:29.100Z
This is not [the category you are looking for](http://math.andrej.com/2016/08/06/hask-is-not-a-category/).
Andrej Bauer
<ct.category-theory><haskell><monad>
What are values relative to Hask?
lightning
# What are values relative to Hask?

(Asked by: username_0 on 2018-05-03)

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

**Tags:** ct.category-theory, haskell, monad

> **Comments:**
> **username_1**: See this stack overflow post https://stackoverflow.com/q/17380379/6511076  
> **username_2**: also worth reading: http://blog.sigfpe.com/2009/10/what-category-do-haskell-types-and.html  
> **username_3**: This is not [the category you are looking for](http://math.andrej.com/2016/08/06/hask-is-not-a-category/).  

---

## 1 answers

### Answer by username_4 on 2018-05-03. Score: 6 | Accepted answer

At the level of precision used in the nlab page, values are [*global elements*](https://en.wikipedia.org/wiki/Global_element) -- 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*](https://www.cs.bham.ac.uk/~pbl/papers/hosc05.pdf).

   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.

> **Comments:**
> **username_3**: Are you lamenting about "Hask" or about "global element"? Global element makes perfect sense, if you think about programs geometrically.  
> **username_4**: Hask. I find it very twee.  
> **username_3**: Hasky would be worse.  

---

