What's Next? (EECS490Lec17)

Last time, we covered working with memory in our language, and made it into an imperative programing language.

Cyrus then goes through a bunch of the previous examples once again. If need be I’ll type them up, but since they’re the same principles it seems a bit excessive.

When we did all of that, we fundamentally changed how we reason about programs.

Reasoning Principles

Before we talked about memory, we were forced to reason about properties of functions equationally. So, for example, Cyrus could have asked us to prove that, for all functions f: int → int:

let x = f 1 in
 let y = f 2 in 
   x + y

is equivalent to

let x = f 2 in 
  let y = f 1 in
    x + y

And we could have done it through our logic of substitution.

However, this is simply not true for imperative programming languages, where even properties like map fusion:

map f ( map g xs ) === map (f%g) xs

fail, due to this added mutability.

Cyrus makes a note here that requiring immutability does allow us to easily parallelize our computations. If we do parallelize everything, we can have essentially free speedups, which wouldn’t be as possible in imperative programming language

So, our goal is to have a language that allows us to still reason equationally, but has access to mutability, as side effects are what we use to interact with the outside world (pure programs, while great, can’t do much alone. They NEED interaction to be useful)

To do so, we can use “Encapsulated Commands”

Encapsulated Commands

Like stated in the last set of notes, instead of adding the mutability judgement and complicating our judgement semantics, what we can do is separate the mutable and immutable parts of our language.

To do that, we’ll create an expression language, which contains the evaluation judgement we’re all used to and the value judgement. This’ll serve as the base for our functional part of the language, where we can preserve all of this simplicity.

We’ll also, however, create a command-oriented language, which serves to take state, command pairs and translate to state command pairs through a similar evaluation judgement. Here is the imperative part of our program, where we can work with memory only when it’s necessary, and even then still reason about the expression language functionally.

So, when we execute an impure program, we’ll create a list of commands through the work in our pure language. Then, we’ll simply execute the reads/writes afterwards.

Evaluate the expressions first to a value, which can be a command, then we execute the command that results from the evaluation (i.e. make the side-effects)

Let’s see how this works in the real world through the language Haskell’s I/O syntax.

Haskell I/O

Haskell actually uses encapsulated commands through something called the I/O monad. What is a monad?

NOTE: The rest of this is some rudimentary mathematical explanation for what a monad is. This is NOT in the lecture materials, but I felt like including it as it helps me understand what’s going on under the hood in Haskell. FEEL FREE TO SKIP TO THE NEXT YELLOW LINE

The idea of a monad refers to this idea of encapsulating the reasoning we hold in functional languages, but change one tiny thing about them. So, let’s say you had the following two functions, not and id :

let not input = match input with
    | True -> False
    | False -> True

let id inputa = match inputa with
    | True -> True
    | False -> False

Now, however, let’s say you wanted to define the optional type maybe:

type 'a t = 'a my_option = 
  | None
  | Some of 'a

And wanted to define new functions, maybe_id and maybe_not , which would work with maybe values instead, allowing us to use maybe values instead for these functions, perhaps if we’re writing some form of low-level network interface.

To do so, we could very much define the functions again, but let’s say we had many such functions, to the point where that really is not an option. (For example, this could be because you’re trying to integrate your new data analysis tool that handles N/As with scikit learn…).

So - how do we solve this issue? Well, let’s reason about this some more. What we really want is some way to turn functions that take in type Bool and return type Bool, into functions that take in type Bool Option and return Type Bool Option.

So - perhaps what we really want instead are two functions: A function called return, which encapsulates our bool into an optional type:

let return (x : bool) : bool my_option = 
   Some x

and a bind function, which takes in a bool option, and a function that takes in a bool and returns a bool option, and returns a bool option:

let bind (x: bool my_option) (operation: bool -> bool my_option) : bool my_option = 
   match x with 
   | None -> None
   | Some a -> operation a

Thus, we can now turn our functions from those that take bool and return bool into functions that take an encapsulated bool option and return an encapsulated bool option:

let maybe_id a = bind a (id%return)
let maybe_not a = bind a (id%return)

and, with that, we’ve managed to upgrade our list of functions really quickly into encapsulated functions, and this process of encapsulation is known as a monad.

The idea here is we can take our ordinary functions, and expand the type space, so long as we now give functions that let us move from that new type space into our old one and back. By doing so, we’re able to model many, many more imperative constructs, such as I/O, in a pure functional sense, and we could even redefine the function composition operator to make this process easier in that case, but the idea is really simple in the high-level.

For more information, this webpage has a great explanation that I really just paraphrased:

U-M Weblogin

And, for the category theory definition of monads as “a monoid in the category of endofunctors”, please refer to the book “Category Theory for Programmers”, where the subject is given the treatment it deserves, but requires a few weeks to digest.

RANT OVER. RESUMING LECTURE MATERIALS

So - Haskell allows you to use encapsulated commands for I/O. To do so, it defines the new type IO:

Type: IO t, which encapsulates I/O commands, 
ultimately producing a value of type tau

In Haskell, then, main is a value of type IO (), which then will print out IO of some kind.

So, in Haskell, what are the introductory and elimination forms of IO?

For example, we have putChar and getChar

putChar : Char -> IO ()
getChar : IO Char 

As putChar takes in a character and prints it to IO, its type makes sense, as we need to give it a Char, and it needs to return something so we make it return an IO () type to tell the compiler that. For getChar, as we don’t supply it a value on our side, it simply refers to IO Char, which is an encapsulated char taken from IO, that we can then use in our program hopefully.

So, for example, if we had the following program:

main = putChar "a"  (main is a value here, so don't forget!)

When we evaluate the command, we get a value of type IO () , that is an encapsulated command, which then, once the expression evaluates in the first stage, will run the commands in the second stage, printing a to the terminal.

Binding it all up

Now that’s all fine and dandy, but what happens when we want to string together input and output? We can’t use the sequencing operator we used earlier, as that takes a function, evaluates it, and ignores everything that function returns. What we want is some way to glue these values together, so later on we can worry about side-effects.

How? We’ll use a new primitive called bind , which has the following type:

bind : (IO 'a) -> ('a -> IO 'b) -> (IO 'b) 

The idea here is that, instead of sequencing the commands together, we’ll take in our input, and a function that takes a normal input and returns an IO output, and the return that new IO command. So, informally, here’s how we would take a character from the user and return it to them, as a sorta “echo test” program:

main = bind getChar putChar

Here, what we’re doing is we’re taking the value we get from getChar / the user, getting the character from it, and then returning it to the user via putChar, which takes in a character and returns an IO type.

Again, we’re not running the IO commands in the evaluation stage. When we execute it, the commands themselves run in a second stage of execution; we simply work with this new type programmatically in the first stage to create that string of commands for I/O

Do Notation

Now, you can imagine, that this sort of bind construct would be really, really, tedious for programmers in Haskell to write out every time. (That, and it’s a bit ugly as we’ve defined it as a normal function and not as an infix operator). What Haskell does to make this easier is introduce a bit of syntactic sugar known as a “do notation”, which looks like the following:

main = do putStr "?"
       c <- getStr
       if isEmpty c then
          putStr("Error")
       else 
         putStr("Hello, " ^ c)

Now, this looks a lot like an imperative programming language, butt this is just syntactic sugar for the bind notation. Thus, Haskell manages to maintain its functional nature while also allowing imperative constructs to do what they do best: write I/O code where thinking about stuff functionally can get a bit complicated.

Closing Thoughts About Encapsulated Commands

With this construct, we gain a lot of power:

• Simpler reasoning for pure functions

• Can treat commands as data

  • Allows for command transformations
  • Run them transactionally, so if there is a failure stop execution
  • Run them in different environments
  • Send command lists to other people to execute them

But we lost the following:

• No benign effects during evaluation, such as caching/memoization

• Haskell has an “escape hatch” (unsafe PerformIO : IO tau → tau)

  • Where you trust the programmer that the IO effect is benign
  • (i.e. Logging)
  • Still apply the same transformations, but we have to make sure the effect is benign for us to do anything
• IO tends to consume programs if you aren’t careful with how you do things.