[dr0wsy]

> So if you want your programming to reap the benefits of (others', mostly) mathematical reasoning--use a functional language that is all about expressing the ways in which things compose!

I do prefer using functional language over imperative ones, but I don't understand that is connected to model software on paper?

> IO is modelled pretty well through monads. As are many other things, like nondeterministic processes, exceptions, state, etc.

Isn't there any easier way to describe I/O than with category theory? I understand that it's _possible_ to model IO with monads, but how would I communicate it with colleagues that doesn't have a background in category theory (or myself for that matter)?

Part of the benefits with modelling a program on paper should be to make communication easier. And to require people you communicate with to have knowledge in category theory to understand your design fells silly.

I probably misinterpret you, so could you please give a more detailed explanation or example?

[naturlich]

You don't need to know category theory. You just need to understand a few things that came from it, like `Maybe`, which is the most obviously useful and trivially easy monad. Just forget about the fact that it's a monad and any general rules about monads and just learn how to use `Maybe`.

From there, input handling is just a state machine. Easy to draw on paper as a graph.

> Part of the benefits with modelling a program on paper should be to make communication easier. And to require people you communicate with to have knowledge in category theory to understand your design fells silly.

This is an odd complaint, because you can also say: requiring people you communicate with to have knowledge in (state machines | graphs | `if` statements | ...) to understand your design feel silly.

[dr0wsy]

> You don't need to know category theory. You just need to understand a few things that came from it, like `Maybe`, which is the most obviously useful and trivially easy monad. Just forget about the fact that it's a monad and any general rules about monads and just learn how to use `Maybe`.

I didn't convey my question clearly. What I'm wondering is how I should express programs, or part of them, using mathematical notation when I don't see them being mathematical in nature to begin with?

An example:

  def hello(name):
      if (name == "Bob"):
          print("Hello, " + name)
      else:
          print("Hello, World!")

How could I express this easily using mathematical notation?

It just feels weird that to convey this simple program on paper both I and the person I try to communicate with needs to have a grounding in category theory.

Hope you're able to understand my question. :)

[naturlich]

That was the second part of my answer: a graph on paper. Draw nodes of execution and represent the branch as two arrows coming from the node and heading to new nodes. Label the arrows with the predicates of the branch.

This is both definitely useful and definitely math.

[dr0wsy]

> That was the second part of my answer: a graph on paper. Draw nodes of execution and represent the branch as two arrows coming from the node and heading to new nodes. Label the arrows with the predicates of the branch.

Thanks! You don't happen to have some learning resources for modelling programs as state machines? I can't find anything when I search.

[naturlich]

This is more of a practical writeup on state machines than a theoretical one: http://gameprogrammingpatterns.com/state.html

You might also know these as flowcharts when applied to program flow control.

I don't think I answered the original question well. I just wanted to point out that math is more than just equations. Others have done a much better job in this thread.

[jcora]

This isn't about modelling rather a programming technique, but check out Idris for its dependent typing. It lets you encode state machines in types, which means your programs literally will not typecheck if you try for example to withdraw money from an unauthorized ATM, or candy from an empty store. You can make verified network protocols and drivers like this.

[jcora]

> because you can also say

I don't think you can actually:D

I mean for each category of programmer there is a pretty clear line separating common knowledge from things you can't expect people to know. And for pretty much every category of programmer, if statements and category theory are the opposite ends of that line.

I mean I feel like you agree with this based on your first paragraph, his complaint isn't odd because it's saying you can't expect people to know category theory, it's because he thinks that category theory is necessary here.

[jcora]

> but I don't understand that is connected to model software on paper

I was talking more generally about techniques that allow for sneaking in mathematical thinking in various stages of development, not just modelling. Largely because of the very precise types which make a large part of your program verifiable (and force you to think about a lot of things you wouldn't have if you were using, say, JavaScript).

I was recently making a script engine for a game. It was really neat to realize that the "runScript" method was literally just a mapping between two monads. No special state inbetween, no complex logic, no file lookup or anything like that. These types of insight accumulate, and there's really a tonne of stuff to learn (this potential for learning the language itself feels much greater in functional programming for me).

> Isn't there any easier way to describe I/O than with category theory?

This isn't category theory! Do you really think every working Haskell programmer is some mathematician? No. Look at this random image I googled, you think Haskell programmers understand this? https://i.stack.imgur.com/4IzGk.png Most mathematicians don't!

The notion of a monad in functional programming might be inspired by category theory, but you're really better of not taking that connection too seriously. Functors, applicatives, and monads are all very simple notions that should be understood as programming constructs, not arcane math. If you want an area of math to research to most benefit your functional programming, that is undoubtedly mathematical logic and/or intro-level type theory, and not category theory. (This should take you in the direction of dependent types.)

Really, types are the key. The notion of a monad is best understood not through vague real-world analogies with sandwiches, but through the type and implementation of its >>= method. The reason for that is that the point of monads is in composition. And basic linear algebra is enough to understand the importance of composition, not category theory. Just look at the Maybe monad to immediately understand it: Nothing >>= f = Nothing, Just x >>= f = f x, where f : a -> Maybe b. Isn't this a really clear, intuitive way of composing operations which might fail?

Same goes for IO. The only thing you're doing is composing some values. When you compose an IO Int with some function of the type Int -> IO (), you get back a value of type IO () (which your runtime executes if you bind it to main). All of this is right in the type, and it's just as intuitive a way of composing IO values as Maybe ones, IMO.

You get the added benefit of execution becoming not a side-effect, but a first-class member. Evaluation of IO programs is not their execution, you could evaluate putStrLn "asdf" a million times without it being executed. You can literally store those programs (values) somewhere and execute them later.