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