14 Syntax and Semantics of Refs

References & Location

• Syntax: ref e
• Evaluation:
  • Evaluate e to a value v
  • Allocate a new location loc in memory to hold v
  • Store v in loc
  • Return loc
• Type checking
  • New type constructor: t ref where t is a type.
    • Note: ref is used as a keyword in type and as a keyword in value
  • ref e : t ref if e : t.

Locations are values, but they are not expressions (No pointer arithmetic 😭). We cannot directly write a value

Assignment

• Syntax e1 := e2
• Evaluation
  • Evaluate e2 to v2
  • Evaluate e1 to location loc
  • Store v2 in loc
  • Return ()
• Type checking:
  • If e2 : t
  • and e1 : t ref
  • then e1 := e2 : unit

The type of a location cannot change

Unit

• unit is a type.
  • It's only value is (), pronounced "unit"
  • There are no interesting operations on unit.
• Analogy: Booleans
  • bool is a type.
  • it has two values, true and false
  • unit is like bool but with one fewer type
• Analogy: void
  • When a procedure in Java or C has no type to return, it's return type is void
  • Similar with print and assert in OCaml:
    • print_string : string -> unit
    • assert b : unit (assuming b : bool).

Dereference

• Syntax: !e
  • note: not negation!
• Evaluation
  • evaluate e to loc
  • return contents of loc
• Type checking
  • if e has type t ref, then !e has type t.