Programming Languages, Fall 2014
HW10 - References

Due electronically on Blackboard on Monday November 24, 11:59pm.

1. Why the new E-AppAbs rule 

      (\x:T.t) v | m -> [x -> v] t | m

   does *not* change the memory state m?
   (i.e., function application, *in itself*, has no side effect).
   
   How about the following function application?
       (\x:Unit. ref 0) unit
       (\x:Unit. ref 0 := 5) unit

   Now do you understand the "in itself" part above?

   Note: the fact that function application has no side effect is 
   the essential motivation for functional programming.

2. The following function
       
       incc = \c: Ref Nat. (c := succ (!c); !c)

   implements "++c" for input variable c in C.
   What's the type of incc?

   Also, show two implementations of "c++".

3. In the update function (on slide 12), after x updates,
   what are the best-case and worst-case time complexities of a lookup?
   
   In the current implementation, repeated updates on the same index 
   result in redundant if statements (e.g., update a 5 2; update a 5 3). 
   Can you write an improved update function that eliminate those redundancies?
   Or, can you at least eliminate repeated updates on the same index for the same value?
   
4. In the preservation theorem, what does Sigma' \supseteq Sigma mean? Why is it the case?
   How about the memory states mu and mu'? When you say mu \supseteq mu'? Do a case analysis.

5. 13.1.3 (having two types for the same storage cell violates type safety).

6. Show the typing derivation tree for term

   ref 0 := !(ref 1)

   show its single-step evaluation sequence all the way to a value,
   and show the typing derivation for each term in this sequence.

   Now do you understand why T-REF rule does not change store typing?
   (page 165, "Notice that we do not need to extend the store typing here, 
   since the name of the new location will not be determined until run time, 
   while Sigma records only the association between already-allocated storage 
   cells and their types.")
   
   What are those "already-allocated storage cells"?

7. There are two ways of memory management: garbage collection (Java/Python), or user deallocation (C/C++).
   (a) C/C++ let users to "free" memory cells.
       Complete Problem 2 in http://www.seas.upenn.edu/~cis500/cis500-f06/hw/hw07.pdf.

   (b) 13.3.1 (optional, modeling garbage collection)

   
   

Debriefing (required!): --------------------------

1. Approximately how many hours did you spend on this assignment?
2. Would you rate it as easy, moderate, or difficult?
3. Did you work on it mostly alone, or mostly with other people?
4. How deeply do you feel you understand the material it covers (0%–100%)? 
5. Any other comments?

This section is intended to help us calibrate the homework assignments. 
Your answers to this section will *not* affect your grade; however, skipping it
will certainly do.