In Felix, pointers have an associated access mode, these are called cv-qualifiers in C++. The original modes are shown in the diagram below:

    N
   / \
  R   W
  \  /
   RW

The lower modes are submodes of the higher modes, and pointers to the same type are subtypes if their modes are submodes. The abbreviations mean:

N	No access
R	Read only
W	Write only
RW	Read and write

The type and expression annotations are illustrated below:

  var x : int = 1;
  var rwp : &int = &x; // read write pointer
  var rp : &<int = &<x; // read only pointer
  var wp : &>nt = &>x; // write only pointer
  // currently N mode has no syntax

We need to recall for pointers:

  var x = 1;
  var p = &x;
  var q = *p;  // fetch operation
  p <- 2;      // store operation

The * operator is called dereference from C, however in Felix it does not create a reference or lvalue, it just fetches a value. The only references in Felix are variables.

Although in principle R pointers are covariant in their target, and W pointers contravariant (making RW pointers invariant), Felix current only supports invariant targets.

There is a well known problem with read-only pointers: the read only attribute only applies to the pointed at object. If you consider a list in which nodes contain a value and a pointer to the next node, a read only pointer to a node does not prevent writing to the next node if the next pointer is read-write. That is, the read-only property only has a shallow effect when we really wanted a deep impact. Here's an example:

  var x   : int      = 1;
  var p   : &int     = &x;   // read write pointer to int
  var rpp : &<(&int) = &<p;  // read only pointer to read-write pointer to int
  var rwp : &int     = *rpp; // read write pointer to int
  rwp <- 2;                  // write to x
  println$ x;                // x is 2 now

Given a pointer p. we define the data structure associated with p as the set of all the objects reachable from p.

A functional view of a data structure is a read only view of the whole data structure. A view pointer mode, abbreviated V, also called propagating const in C++, is a pointer mode with the semantics that ensure that no object of the data structure is writable (via that pointer), and thus provides the required deep effect.

We use the following annotation for view mode pointers:

  var x : T;
  var vp : &<<T = &<<x;

To see how these work, we repeat the previous example but using a view:

  var x   : int        = 1;
  var p   : &int       = &x;    // read write pointer to int
  var vpp : &<<(&int)  = &<<p;  // view pointer to read-write pointer to int
  var vp  : &<<int     = *vpp;  // view pointer to int
  // rwp <- 2;                  // TYPE ERROR

In this example, the propagation of the view mode occurs when the view pointer is dereferenced: type usual fetched type &int is hacked with a reinterpret cast, in effect, to have type &<<int instead, this preventing any write derived from the view pointer by fetch operation.

The implementation is not entirely straight forward. The coercion is entirely at the type level and does not impact values: it is called viewification.

3.1 Viewifying a pointer type

V -> V
R -> V
RW -> V
W -> N
N -> N

3.2 Viewifying a primitive type

3.3 Viewifying a structural type

3.4 Viewifying a type variable

3.5 Viewifying a structured nominal type

Here is an example:

  begin
    // option type
    variant opt[T] = | None | Some of T ;
  
    // list node type
    struct Node { a:int; next: opt[&Node]; }
  
    // construct a sample list
    var px = unbox (new Node (1, None[&Node] ));
    px = unbox (new Node (2, Some (px)));
    px = unbox (new Node (3, Some (px)));
  
    // a pretty printer for the list
    // which proves the list is not changed
    fun pNode (var px:&<<Node) =>
      (px*.a).str + ", " +
      match  px*.next with
      | None => ";"
      | Some px => pNode px
      endmatch
    ;
  
    println$ px.pNode;
  end

Notice the node type uses a RW pointer, but the print routine uses a V pointer. The routine is recursive, and the view mode propagates through the recursion.

The node type is a nominal product, and the option type is a nominal variant, the same as the one in the standard library, and involves a type variable.

The critical point is that *px is a viewified version of Node, and so the projection next applied to it is a viewified version of opt[&Node] which if populated has the Some constructor with argument of type viewified &Node which is type &<<Node as required for the recursion to go through.

I note finally that these rules could easily be applied in C++ by adding a "propagating const" cv-qualifier, in fact the implementation would actually be simpler because C++ does not support type checked polymorphism, so there is no need to mark type variables (that is; none of the rules are needed until after template instantiation). C++ also has no write only mode, and no proper no-access mode: a void* may suffice, however in Felix N mode pointers, whilst not supporting access to the target, do support address calculations.

As a final note, the existence of these 5 modes in Felix would mean that generalised pointer projections would be impossible to express; for example given a pointer into one data structure, you might want to find a corresponding pointer into another, with the same mode. To do that you'd actually need to write the algorithm out 5 times. To fix that, we'd need mode polymorphism!