*

- 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