4 ms·

The type structure of call-by-value languages is inherently monadic. The monad in question is the identity functor iff the language is pure and terminating. Giv

The type structure of call-by-value languages is inherently monadic. The monad in question is the identity functor iff the language is pure and terminating. Given the predominance of call-by-value languages, I'd expect every programmer to have a modicum of understanding of monads, if only to have the faintest idea how popular languages (yes, popular languages, not Haskell) work.

Smaug123 10y ago
But I argue that this is not the place to do it (since it requires more ink and motivation than there is space left in the article). Anyway, you might as well say that every programmer should have a modicum of understanding of chip design, since every language is run on chips; but while it may make one a better programmer, it's not necessary in many higher-level languages.
Smaug123 10y ago
By the way, it's very early on the morning after Christmas Day for me, so I'm struggling to load the structures into my mind properly. What category is the functor going from and to? The Precise Monadicity Theorem states that a functor G is monadic iff it has a left adjoint and it creates coequalizers of G-split pairs; what is the left adjoint of this functor? What does a coequalizer look like in the category? (I suspect I can work these out myself given a good statement of what the category is.)
- catnaroek 10y ago
  If I understand correctly, the category in question can be characterized as follows: (0) For every type X in the language, there is an object X of values (not arbitrary terms!) of that type. (1) For every type X in the language, there is an object TX of closed programs (containing no free variables) of type X. T is the monad in question. (2) A morphism “f : X -> TY” is an arbitrary program of type Y containing a single free variable of type X. (3) (This is the part where I'm the least sure!) A morphism “f : X -> Y” is a pure terminating program containing a single free variable of type X. Also, I should've been more careful. If the language is pure and terminating, the monad in question is an equivalence of the category in question with itself. Not necessarily the identity functor.
- Roboprog 10y ago
  Holy crap. This. To paraphrase: "English, mofo. Do you speak it?!?" :-) I have been programming for over 30 years (which I suppose means nothing if it's just doing the same year over 30 times, but bear with me). Every other language (at the risk of being largely self selected, I know) I have ever worked on seems to incrementally add things or shift ideas around a little bit. Some communities might try to helpfully explain things to newcomers. But the perception of the Haskell community is that they revel in being as cryptic as possible in their purity. I'm not even sure if the above comment was serious (it was probably deadly serious), or absolute troll fodder nonsense. I know (more or less???) what a functor is, and I know what IFF means. Unfortunately, most of what I remember from mathematics comes down to a function has a domain of inputs and a range of outputs, and being a function implies you can predict the output from the input; a "type" is a rule for describing a set, possibly infinite (not much use for computing), of values; values can be "scalar", or multidimensional such as a vector/matrix/tensor. I know that "category" means something very specific to you guys, but not what. You lost me.
  - Smaug123 10y ago
    It was intended seriously, as a question between mathematicians, though I realise the language looks pretty intimidating :)
  - dllthomas 10y ago
    A category is a set of objects and a set of arrows between those objects, and an operator that composes those arrows associatively. For much, much more, this might be a good fit for you: https://bartoszmilewski.com/2014/10/28/category-theory-for-programmers-the-preface/ https://bartoszmilewski.com/2014/10/28/category-theory-for-p...

Smaug123 10y ago

But I argue that this is not the place to do it (since it requires more ink and motivation than there is space left in the article). Anyway, you might as well say that every programmer should have a modicum of understanding of chip design, since every language is run on chips; but while it may make one a better programmer, it's not necessary in many higher-level languages.

Smaug123 10y ago

By the way, it's very early on the morning after Christmas Day for me, so I'm struggling to load the structures into my mind properly. What category is the functor going from and to? The Precise Monadicity Theorem states that a functor G is monadic iff it has a left adjoint and it creates coequalizers of G-split pairs; what is the left adjoint of this functor? What does a coequalizer look like in the category? (I suspect I can work these out myself given a good statement of what the category is.)

catnaroek 10y ago
If I understand correctly, the category in question can be characterized as follows: (0) For every type X in the language, there is an object X of values (not arbitrary terms!) of that type. (1) For every type X in the language, there is an object TX of closed programs (containing no free variables) of type X. T is the monad in question. (2) A morphism “f : X -> TY” is an arbitrary program of type Y containing a single free variable of type X. (3) (This is the part where I'm the least sure!) A morphism “f : X -> Y” is a pure terminating program containing a single free variable of type X. Also, I should've been more careful. If the language is pure and terminating, the monad in question is an equivalence of the category in question with itself. Not necessarily the identity functor.
Roboprog 10y ago
Holy crap. This. To paraphrase: "English, mofo. Do you speak it?!?" :-) I have been programming for over 30 years (which I suppose means nothing if it's just doing the same year over 30 times, but bear with me). Every other language (at the risk of being largely self selected, I know) I have ever worked on seems to incrementally add things or shift ideas around a little bit. Some communities might try to helpfully explain things to newcomers. But the perception of the Haskell community is that they revel in being as cryptic as possible in their purity. I'm not even sure if the above comment was serious (it was probably deadly serious), or absolute troll fodder nonsense. I know (more or less???) what a functor is, and I know what IFF means. Unfortunately, most of what I remember from mathematics comes down to a function has a domain of inputs and a range of outputs, and being a function implies you can predict the output from the input; a "type" is a rule for describing a set, possibly infinite (not much use for computing), of values; values can be "scalar", or multidimensional such as a vector/matrix/tensor. I know that "category" means something very specific to you guys, but not what. You lost me.
- Smaug123 10y ago
  It was intended seriously, as a question between mathematicians, though I realise the language looks pretty intimidating :)
- dllthomas 10y ago
  A category is a set of objects and a set of arrows between those objects, and an operator that composes those arrows associatively. For much, much more, this might be a good fit for you: https://bartoszmilewski.com/2014/10/28/category-theory-for-programmers-the-preface/ https://bartoszmilewski.com/2014/10/28/category-theory-for-p...