EECS 662 Blog

Notes From State

As promised here are my notes from class covering mutable state through the end of the semester. I have not edited or otherwise tried to clean them up, but they do represent what we covered in class. For other topics the online text is far better prepared and much preferable.

There are a few topics - sums and products, errors, loops - that I removed from the end of these notes. Those topics are not on the exam. The exam topics end where these notes end.

Mutable State

The big difference between Haskell and C

... x=x+3 ; y=x++ ...

• What does the “;” do?
• What does the "=" do?

New Operations for Sequencing

bind x=(f a) in
  (g 3)
== ((lambda _ in (g 3)) (f a))

What’s happening besides substitution?

do { l’ <- eval l ;
     r’ <- eval r ;
     return (op l’ r’) }

What’s happening besides binding?

Order!

We tend to think of two programming paradigms:

• functional - ordering is achieved via calling convention
  • Identifiers get their values from parameter passing
  • Haskell, Scheme, OCaml, ML, Common Lisp
• imperative - ordering is achieved via sequencing mutable state
  • C, C++, Java, Ada, JavaScript
  • Identifiers get there values from a shared, global state

What’s happening in this sequence? Where does x get a value?

x := 1; x := x + 1; x := x + 1; ...

:= (the walrus) is an assignment that updates a variable in the next state

x := x+1  ==  x’ = x+1

• The tick notation traditionally means next.
• The next x is the current x plus 1

Adding State to FBAE

How is state different than environment?

1. A Seq sequence operator
2. Define a store
3. Update eval to maintain state in addition to environment

New concrete syntax: t ; t

New abstract syntax: Seq::FBAE->FBAE->FBAE

Define sequence by elaboration: Seq l r == (App (Lambda x r) l)

eval e s Seq l r = do { s' <- eval e s l; eval e s' r }

Is state updated differently than environment?

Interesting syntax!

We’re being sloppy anyway, we’ll skip typing for now.

New operations and types for state

FBAE := new FBAE | deref FBAE | set loc FBAE

• loc - new type of value for locations - where’s loc in the syntax?
• new t - creates a new location, puts eval t there, returns the location
• deref l - retrieves a value from l and returns it
• set l t - stores eval t in location l and returns l

deref (new 5)
== 5

deref (set (new 5) 6)
== 6

bind l = new 2+3 in deref l [(l,->5)]
== (deref l) [(l,->5)]
== (deref ->5)
== 5

bind l = new 2+3 in                 [(l,->5)]
  set l ((deref l) + 1) ; (deref l) [(l,->5)]
== (set l 6) ; (deref l)
== (deref l)       [(l,->6)]
== 6

• A new derived form for := (sort of)?

l := r == (set l (deref r))

l := l + 1

• Not really. This is not completely correct. Any idea why?

bind m = new 5 in      [(m,->5)]
  bind n = m in        [(n,->^)]
    set m 6 ; deref n  [()]
== 6

bind m = new 5 in
  bind n = m in
    bind n = new 5 in
      set m 6 ; deref n
== 5

bind inc = (lambda l in (set l ((deref l) + 1)))
  bind n = new 5
    inc n ; deref n
==

Announcements

• Modal Crash Types for Intermittent Computing, Myra Dotzel November 22 at 1:30pm in Nichols Hall Apollo Room.
  • Myra is a former KU student now at CMU
  • Researcher in Languages and Types
  • 5 bonus points on the final for those who attend

    Implementing State

Store as a function with location as a number

We could use an array or a sequence, but let’s try a technique commonly used in formal modeling.

type Sto = Loc -> Maybe FBAEVal

type Loc = Int

Sto is the store and is a function from Loc to Maybe FBAEVal.

Why a Maybe?

• Just x - a good location is accessed.
• Nothing - a bad location is accessed.

What are good and bad memory locations?

What does this have to do with language design?

Memory contains FBAEVal. What does this imply?

• How is this different from a C pointer?
• How is this different from a Java reference?

What does this have to do with language design?

Dereferencing is just using the store as a function:

derefSto s l = (s l)

The initial store is a store with nothing in it.

initSto :: Sto
initSto x = Nothing

• What is initSto 3?
• What is initSto for any value?

Updating the store is a bit trickier…

• Add 1 to location 3: m0 = \l -> if l=3 then 1 else (initSto l)

m0 is the new store using if

• Return (m0 3) = 1 using then when l=3

• Return initSto l using else when l<>3

• Add 2 to m0 at location 1: m1 = \l -> if l=1 then 2 else (m0 l)

m1 is the new store again using if

• Return (m1 1) = 2 using then when l=1
• Return (m0 l) using else when l<>1
• What is (m1 3)?

• What is (m1 2)?

• And 0 to location 2: m2 = \l -> if l=2 then 0 else (m1 l)

m2 is the new store yet again using if

• Return (m2 2) = 0 using then when l=2
• Return (m1 l) using else when l<>2
• What is (m1 3)?

• What is (m1 2)?

• Replace the value in location 3: m3 = \l -> if l=3 then 4 else (m2 l)

m3 is the new store yet again using if

• Return (m3 3) = 4 using then when l=3
• Return (m2 l) using else when l<>3
• What is (m1 3)?

• What happened to the old (m1 3)

• Is this really updating the store?

… if it walks like a duck and quacks like a duck …

setSto :: Sto -> Loc -> FBAEVal -> Sto
setSto s l v = \m -> if m==l then (Just v) else (s m)

• \x -> t is lambda x in t in Haskell
• Given that, how does this work?
• Why would I ever do this?

The store becomes a collection of nested if statements. Not the most efficient, but it does what it’s supposed to for our purposes.

Putting things together to model memory:

type Store (Loc,Sto)

A location, store pair.

• loc is the next memory element
• sto is the current memory

derefStore (_,s) l = (s l)

Dereferencing is accessing the memory location

initStore = (0,initSto)

Initialize memory is the initial, empty memory with a next value of 0.

setStore (m,s) l v = (m,setSto s l v)

Storing a new value

newStore (l,s) = (l+1,s)

Uh, we’re not storing anything are we?

Allocating memory location.

• Now we know what l is for
• Keep track of where the next memory location should be.

Integrating Mutable Store

How does store differ from environment?

• Changes to store persist across scopes
• Locations are values

Let’s add a constructor for locations

data FBAEVal =
  ...
  Loc :: Int -> FBAEVal

And a constructor in FBAE?

Seems simple enough

• eval can return a location
• Locations can be calculated? Maybe?
• Locations can be stored? Maybe?

Our choices are important. Even the tiny ones.

How to implement mutability of Store??

Start with a new return value:

type Retval = (FBAEVal,Store)

Retval is the return value for our interpreter

• A value from FBAE
• The resulting store

What’s this for??

eval :: Env -> Store -> FBAE -> Maybe Retval

eval now takes an environment and a store.

• Env - identifiers and values in scope
• Store - contents and current location in memory.

What should an initial call to eval look like?

• environment
• store
• term

x:=x+1 ; x:=x+1

eval e s (Seq l r) = do {(v,s') <- (eval e s l) ;
                         (v',s'') <- (eval e s' r) ;
                         return (v',s'')}

• Notice what v is doing
• One thing, then the other….

eval e s (Set l t) = do {(v,s') <- (eval e s t) ;
						 (setStore s' l v)}

• All that work finally pays off - Set calls setStore

• What is the pattern matching in the do clause doing?

eval e s (Plus l r) = do {((NumV l'),s') <- (eval e s l) ;
                          ((NumV r'),s'') <- (eval e s' r) ;
                          return ((NumV l'+r'),s'')}

This passing of state is the new idiom:

eval e s (Deref t) = do {((Loc l'),s') <- (eval e s t) ;
                         (derefStore (Loc l') s'}

Let’s unpack New and figure out what’s going on:

eval e s (New t) = do { (v’,(l,s’)) <- eval e s t ;
                        return ((Loc l+1),(setStore (newStore (l,s’)) s' v’)) }

Wow. What the heck?

• (v',(l,s')) - v' value to be stored in s' at location l+1
• (Loc l+1) - next location after l the location value is the return value.
• (newStore (l,s')) - new store with l allocated
• (setStore ...) - stores v' `

  Variables and Assignment

Let’s do this together…

What is the difference between a variable and an identifier?

We have utilities for mutable store that we should be able to use.

What things do we need to define?

• Variable declaration
• Variable dereference
• Variable assignment

We want to control the way that memory gets accessed.

• No more set, deref, new

Variable Declaration

• What tools might we have?

var x:=t1 in t2 == bind x=new t1 in t2

var x:=0 in
var y:=1 in
var z:=3 in x+y+z

• Defines x, y and z in a style like OCaml
• Nothing prevents shadowing variables
• Alternative syntax might be `var x:=0 ; var y:=1 ; var z:=2 ; x+y+z

  Variable Dereference

• It would be nice to just say x+1 rather than `(deref x) + 1
• Is that possible if x is a variable?

(deref (lookup x e) s) - value stored in the location stored in x

• Find the variable location using lookup
• Dereference the location using deref

Variable Assignment

• What tools might we have?

`x := v == (set x v)

• We only store values v not general terms
• Any requirements for x?

Asn :: string -> FBAE -> FBAE

For example:

x := x+y+z

• Evaluate the right side as normal to get a value
• Store the value in variable x
• Variable - Identifier whose value can be changed
  • Are there requirements on this variable thing?
  • Are there requirements on the right side value?

(set x v)

• set works if x is a location and v is a value resulting from evaluating the right side.

In many languages we will remove all location manipulating functions and just use var and assignment. Any reason for that?

Project 2 Posted

Project 2 is now available. We will talk about the due date in class on Tuesday, but I believe you can complete the entire project now. There may be just a couple of things remaining to be covered, but you can certainly get started if you would like.

Lambda Examples From Class

Following are examples using lambda from class. Note that I’ve done no proofreading, so the notes reflect the state they were in when my lecture ended.

(lambda x in x)
== (lambda x in x)

• lambda is a value - what does that actually mean?

((lambda x in x) 5)
== [x->5]x
== 5

app evaluates a lambda applied to an expression

((lambda z in z) (lambda x in x))
== [z->(lambda x in x)] z
== (lambda x in x)

What function is this?

(((lambda x in (lambda y in x+y)) 3) 2)
== [x->3](lambda y in x+y)
== ((lambda y in 3+y) 2)
== [y->2]3+y
== 3+2
== 5

(lambda x y z ...) == (lambda x in (lambda y in (lambda z in ...)))

(((lambda x in (lambda y in x+y)) 1)
== (lambda y in 1+y)

Signatures?

((lambda x in (x 3)) (lambda z in z))
== [x->(lambda z in z)](x 3)
== ((lambda z in z) 3)
== 3

Functions as parameters. What’s this?

bind inc=(lambda x in x+1) in (inc 3) [(inc,(lambda x in x+1))]
== (inc 3)                            [(inc,(lambda x in x+1))]
== ((lambda x in x+1) 3)
== 3+1
== 4

Named lambda values are just like any other value.

                                  []
bind inc=(lambda x in x+1) in     [(inc,(lambda x in x+1))]
  bind dec=(lambda x in x-1) in   [(dec,(lambda x in x-1)),(inc,(lambda x in x+1))]
    bind sqr=(lambda x in x*x) in [(sqr,(lambda x in x*x)),(dec,(lambda x in x-1)),(inc,(lambda x in x+1))]
      (inc (sqr (sqr 3)))
== ((lambda x in x+1) (sqr (sqr 3)))
== ((lambda x in x+1) ((lambda x in x*x) (sqr 3)))
== ((lamdba x in x+1) ((lambda x in x*x) ((lambda x i x*x) 3)))
== ((lamdba x in x+1) ((lambda x in x*x) (3*3)
== ((lamdba x in x+1) 9*9
== 1+81
== 82

More using $\lambda$-calculus:

(lambda y in y)(lambda x in x)
== [y->(lambda x in x)]y
== (lambda x in x)

f==(lambda y in y)
s==y
i==y
va == a==(lambda x in x)

(lambda x in x x) 3
== [x->3](x x)
== (3 3)

(lambda x in x x)(lambda y in y)
== [x->(lambda y in y)](x x)
== ((lambda y in y)(lambda y in y))
== [y->(lambda y in y)]y
== (lambda y in y)

(lambda x in x x)(lambda y in y y)
== [x->(lambda y in y y)](x x)
== (lambda y in y y) (lambda y in y y)
== [y->(lambda y in y y)](y y)
== (lambda y in y y) (lambda y in y y)

More examples using abstract syntax. Note that a few are not worked - I will do them in class.

((Lambda i s) a) == bind i a s

bind f = (lambda x in x) in
  (f 2)
== [f->(lambda x in x)](f 2)
== ((lambda x in x) 2)
== 2

bind n = 1 in
  bind f = (lambda x in x + n) in
    bind n = 2 in
      f 1
== bind f = (lambda x in x + 1) in
    bind n = 2 in
      f 1
== bind n = 2 in
      (lambda x in x + 1) 1
==  (lambda x in x + 1) 1
== 1+1
== 2

(f a) -> (App f a)

f(x)=x+1 == bind f = (lambda x in x+1) 
f(x,y)=x+y == bind f = (lambda x in (lambda y in x+y))
== f(x)=(lambda y in x+y)

Same problem as before - inefficient and kind of clumsy

Try again with environments:

Env = [(string,FBAE)]

eval e (Lambda i s) = 
eval e (App f a) = do {  }

eval e (Id i) = 

Same technique as bind - save the value and substitute later.

bind f = (lambda x in x) in      []
  (f f)                          
== 

Seems to work quite nicely.

bind n = 1 in                     []
  bind f = (lambda x in x + n) in []
    bind n = 2 in                 []
      f 1
== 

Oops… What happened here?

Bind Examples From Class

Following are examples using bind from class. Note that I’ve done no proofreading, so the notes reflect the state they were in when my lecture ended.

bind x=5 in x+x
== 5+5
== 10

bind x=5 in
  bind y=6 in x+y
== bind y=6 in 5+y
== 5+6
== 11

bind x=5 in
  bind x=6 in x+x
== bind x=6 in x+x
== 6+6
== 12

bind x=5 in
  bind x=6+x in x+x
== bind x=6+5 in x+x
== 11+11
== 22

bind x=5 in
  x + bind y=6 in x+y
== 5 + bind y=6 in 5+y
== 5 + 5 + 6
== 5 + 11
== 16

bind x=5 in
  x + bind x=6 in x+x
== 5 + bind x=6 in x+x
== 5 + 6 + 6
== 5 + 12
== 17

bind x=5 in
  x + y
== 5 + y
== !

bind x=x+1 in x
== !

Examples using abstract syntax.

eval (Bind “x” (Num 5)
		(Bind “y” (Num 6)
			(Plus (Id “x”) (Id “y”))))
== (Bind "y" (Num 6)
      (Plus (Num 5) (Id "y")))
== (Plus (Num 5) (Num 6))
== (Num 11)

eval (Bind “x” (Num 5) (Plus (Id “x”) (Id “x”))))
== (Plus (Num 5) (Num 5))
== (Num 10)

eval (Bind “x” (Num 5)
       (Bind “x” (um 6)
         (Plus (Id “x”) (Id “x”))))
== (Bind "x" (Num 6)
      (Plus (Id "x") (Id "x")))
== (Plus (Num 6) (Num 6))
== 12

eval (Bind “x” (Num 5)
       (Bind “y” (Num 5)
         (Bind “x” (Num 6)
           (Bind “y” (Num 4)
             (Bind “z” (Num 7)
               (Id “z”))))))
==

Examples using deferred substitution.

eval (Bind “x” (Num 5)               [("x",(Num 5))]
       (Bind “y” (Num 6)             [("y",(Num 6)),("x",(Num 5))]
         (Plus (Id "x") (Id "y"))))  [("y",(Num 6)),("x",(Num 5))]
== (Plus (Num 5) (Nun 6))
== 5+6
== 11

eval (Bind “x” (Num 5)               [("x",(Num 5))] -- Environment
       (Bind “x” (Num 6)             [("x",(Num 6)),("x",(Num 5))] -- Shadowing "x"
		 (Plus (Id "x") (Id "x")))   [("x",(Num 6)),("x",(Num 5))]
== (Plus (Num 6) (Num 6))
== 6+6
== 12

eval (Bind “x” (Num 5)               [("x",(Num 5))]
       (Bind “x” (Num 6)             [("x",(Num 6)),("x",(Num 5))]
		 (Plus (Num 6) (Id "y"))))   [("x",(Num 6)),("x",(Num 5))]
== (Plus (Num 6)) ????
== Nothing

eval (Bind “x” (Num 5)                     [("x",(Num 5))]
	   (Plus (Num 5)                       [("x",(Num 5))]
         (Bind “x” (Num 6)                 [("x",(Num 6)),("x",(Num 5))]
		   (Plus (Id "x") (Id "x"))))      []
== (Plus (Num 5) (Plus (Num 6) (Num 6)))
== 5 + 12
== 17

eval (Bind “x” (Num 5)                     [("x",(Num 5))]
       (Plus 
         (Bind “x” (Num 6)                 [("x",(Num 6)),("x",(Num 5))]
		   (Plus 6 6))                     []
	     (Id "x")))                        []
==

No Class September 24

I am cancelling class on September 24 due to required personal travel. I’m not sure how we’ll make up the time, but I will let you know later in the semester.

TA Office Hours

Just updated the office ours for our TA. They are now 3-4 MW in his office Eaton 2011. You can reach him via email at connor.sullivan13@ku.edu.

Project 1 Posted

I just updated the Project 1 description on the class website to include a due date of October 3.

Project 0 Posted

I just pushed the Project 0 description to our class website. You should be able to work all the exercises based on material presented in class. Make sure that you look at the utilities file before you start working on the project. There is some useful stuff in there that will make your life simpler. I will set a due date tomorrow in class.

Welcome!

Welcome to the website for EECS 662 - Programming Languages at the University of Kansas. Contents of this blog are available via an Atom feed that can be viewed using any RSS reader. Use this url. Please check here frequently for breaking news and information about projects and exams.

This site is hosted on GitHub and constructed using GitHub Pages, Jekyll and Liquid Tags.