<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd"><html xmlns="http://www.w3.org/1999/xhtml"><head><title>CDuce: References</title><meta content="text/html; charset=iso-8859-1" http-equiv="Content-Type"/><link type="text/css" rel="stylesheet" href="cduce.css"/></head><body style="margin: 0; padding : 0;"><table border="0" width="100%" cellspacing="10" cellpadding="0"><tr><td valign="top" align="left" style="width:20%;"><div class="leftbar" id="leftbar"><div class="smallbox"><ul><li><a href="#introduction">Introduction</a></li><li><a href="#adv">Advanced programming</a></li><li><a href="#empty">'ref Empty' is not Empty?!</a></li></ul><p>
You can cut and paste the code on this page and
test it on the <a href="http://reglisse.ens.fr/cgi-bin/cduce">online interpreter</a>.
</p></div></div></td><td><h1>References</h1><div class="mainpanel"><div class="smallbox"><p><a href="index.html">CDuce: documentation</a>: <a href="tutorial.html">Tutorial</a>: References</p><p><a href="tutorial_errors.html"><img class="icon" width="16" alt="Previous page:" height="16" src="img/left.gif"/> Error messages and Warnings</a> <a href="tutorial_queries.html"><img class="icon" width="16" alt="Next page:" height="16" src="img/right.gif"/> Queries</a></p></div><div><h2><a name="introduction">Introduction</a></h2><b style="color:#FF0080">TO BE DONE (for the moment please consult the user manual)</b></div><div><h2><a name="adv">Advanced programming</a></h2><p>
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 <b><tt>get</tt></b> and <b><tt>set</tt></b> 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.
</p><p>
For instance the following template program, shows a way to define an integer reference <b><tt>x</tt></b> that whenever it is read executes some extra code, while whenever it is written performs some checks and possibly raises an exception:
</p><div class="code"><pre>
let x : ref Int =
let hidden = ref Int 0 in
{ get = (<i>some_extra_code</i>; hidden . get) ;
set = fun (x :Int):[] =
if <i>some_condition</i>
then hidden . set(x)
else raise "Invalid assignment"
}
</pre></div><p>
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 <b><tt>fun ( x :{ get = []-><i>T</i> ; ..} )...</tt></b>. In this case the function can accept as argument any reference of type <b><tt>ref <i>S</i></tt></b>, with <b><tt><i>S</i></tt></b> subtype of <b><tt><i>T</i></tt></b>.
</p></div><div><h2><a name="empty">'ref Empty' is not Empty?!</a></h2><p>
However the use of the encoding also causes some weirdness. For instance a
consequence of the encoding is that the type <b><tt>ref Empty</tt></b> 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 <b><tt>ref
Empty</tt></b>.
</p><p>
The key observation to define a value of <b><tt>ref Empty</tt></b> is that for every type <b><tt><i>T</i></tt></b> the type
<b><tt><i>T</i> -> Empty</tt></b> 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 <b><tt>Empty</tt></b>). But, for instance, <b><tt> fun f(x :<i>T</i>):Empty = f x</tt></b> is a value of type <b><tt><i>T</i> -> Empty</tt></b>.
</p><p>
By using the observation above it is then easy to explicitly define a reference <b><tt>y</tt></b> of type <b><tt>ref Empty</tt></b>, as follows:
</p><div class="code"><pre>
let y : ref Empty =
let fun f (x :[]):Empty = f x in
{ get = f ;
set = fun (x :Empty):[] = []}
</pre></div><p>
Of course such a reference is completely useless, but its existence
yields some unexpected behavior when matching reference types. Consider
the following function:
</p><b style="color:#FF0080">TO BE DONE</b><div class="code"><pre/></div><p>
The matching expression is not exhaustive since it does not deal with the case where the argument is of type <b><tt>ref (Int & Bool)</tt></b> that is <b><tt>ref Empty</tt></b></p></div><div class="meta"><p><a href="sitemap.html">Site map</a></p></div><div class="smallbox"><p><a href="index.html">CDuce: documentation</a>: <a href="tutorial.html">Tutorial</a>: References</p><p><a href="tutorial_errors.html"><img class="icon" width="16" alt="Previous page:" height="16" src="img/left.gif"/> Error messages and Warnings</a> <a href="tutorial_queries.html"><img class="icon" width="16" alt="Next page:" height="16" src="img/right.gif"/> Queries</a></p></div></div></td></tr></table></body></html>
distrib
>
Mandriva
>
2010.0
>
i586
>
media
>
contrib-release
>
by-pkgid
>
a2da5eab8fb68605fe995d94e514eeb0
>
files
>
38
