- Introduction
- Advanced programming
- 'ref Empty' is not Empty?!

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

# References

CDuce: documentation: Tutorial: References

Error messages and Warnings Queries

## 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`

Site map

CDuce: documentation: Tutorial: References

Error messages and Warnings Queries