Introduction

TO BE DONE (for the moment please consult the user manual)

Advanced programming

The fact that reference types are encoded, rather than primitive, brings some advantages. Among these it is noteworthy that, thanks to the encoding, the default behavior of the get and set functions can be modified. So a programmer can define a reference that whenever is read, records the access in a log file, or it performs some sanity checks before performing a writing.

For instance the following template program, shows a way to define an integer reference x that whenever it is read executes some extra code, while whenever it is written performs some checks and possibly raises an exception:

let x : ref Int = 
   let hidden = ref Int 0 in
     { get = (some_extra_code; hidden . get) ;
       set = fun (x :Int):[] =
               if some_condition 
                  then hidden . set(x)
                  else raise "Invalid assignment"
     }

Another advantage is that it is possible to define the types for read only and write only channels, which can be specialized respectively in a covariant and contravariant way. For instance if the body of a function performs on some integer reference passed as argument only read operations, then it can specify its input type as fun ( x :{ get = []->T ; ..} ).... In this case the function can accept as argument any reference of type ref S, with S subtype of T.

'ref Empty' is not Empty?!

However the use of the encoding also causes some weirdness. For instance a consequence of the encoding is that the type ref Empty is inhabited (that is there exists some value of this type). We invite the reader to stop reading the rest of this section and try as an exercise to define a value of type ref Empty.

The key observation to define a value of ref Empty is that for every type T the type T -> Empty is inhabited. Of course it is inhabited only by functions that loop forever (since if such a function returned a value this value would be of type Empty). But, for instance, fun f(x :T):Empty = f x is a value of type T -> Empty.

By using the observation above it is then easy to explicitly define a reference y of type ref Empty, as follows:

let y : ref Empty = 
  let fun f (x :[]):Empty = f x in
    { get = f ;
      set = fun (x :Empty):[] = []}

Of course such a reference is completely useless, but its existence yields some unexpected behavior when matching reference types. Consider the following function:

TO BE DONE

The matching expression is not exhaustive since it does not deal with the case where the argument is of type ref (Int & Bool) that is ref Empty

You can cut and paste the code on this page and test it on the online interpreter.