References

extend with #references;

A reference variable is a pointer to a mutable area in memory. Interally, it stores a memory address and is used to refer to the data in that memory location.

Memory address

A memory address is a reference to a specific memory location at runtime where an object is stored. A reference variable stores such a memory address, and the typical way of obtaining such data type is through referencing other variables. A memory address literal looks like <0xaddress>, where address is an integer literal specified in hexadecimal (ex: <0x0BEEF123>).

Reference type

A reference type is the type of a variable that refers to another variable. It is written as &Type, where Type is the type of the other variable to which the reference will refer. For example, &Nat is the type of a variable that stores the memory address of a Nat variable.

Note that the type being referred to can be a reference type itself, meaning that &&Nat is the type of a pointer to a pointer to a Nat.

Referencing

To create a reference, simply use the new function with the initial value. For example, new(0) creates a new reference of type &Nat whose starting value is 0. The reference is created with a copy of the value, so new(var) does not create a reference to the memory address of var, but instead creates a new memory address and copies the contents of var to it, returning the reference to that memory address.

Dereferencing

The opposite of the referencing operator, the dereferencing operator (denoted using *) gets the value from the memory address pointed at by the reference. So, if ref has type &Nat, then *ref is the value referred to by ref and has the type Nat.

Assignment

The assignment operator := is used to modify the value in the memory address pointed at by the reference object. It follows the syntax expr1 := expr2, where expr1 is a reference type and expr2 is a value type (which is referred to by the type of expr1).

As an expression, the value of the assignment operation is unit.

Full example:

language core;

extend with
  #unit-types,
  #references,
  #let-bindings,
  #sequencing;

fn inc_ref(ref : &Nat) -> Unit {
  return
    ref := succ(*ref)
}

fn inc3(ref : &Nat) -> Nat {
  return
    inc_ref(ref);
    inc_ref(ref);
    inc_ref(ref);
    *ref
}

fn main(n : Nat) -> Nat {
  return let ref = new(n) in inc3(ref)
}

Note that in the above example, the value of n does not change. This means that in the following example, the value given to input will be exactly the value returned by main:

language core;

extend with #references, #sequencing, #unit-types;

fn inc(ref : &Nat) -> Unit {
    return ref := succ(*ref)
}

fn main(input : Nat) -> Nat {
    // Wrong: not the output you might expect
    return inc(new(input)); input
}