Commit 212a5b59 authored by Pietro Abate's avatar Pietro Abate
Browse files

[r2003-05-21 19:14:36 by cvscast] Manual

Original author: cvscast
Date: 2003-05-21 19:14:36+00:00
parent 516f1de3
......@@ -26,7 +26,7 @@ or as a pair pattern of two type constraints.
In this page, we present all the types and patterns that CDuce recognize.
In this page, we present all the types and patterns that CDuce recognizes.
It is also the occasion to present the CDuce values themselves, the
corresponding expression constructions, and fundamental operations on them.
......@@ -35,7 +35,8 @@ corresponding expression constructions, and fundamental operations on them.
<box title="Boolean connectives" link="bool">
CDuce recognize the full set of boolean connectives.
CDuce recognize the full set of boolean connectives, whose
interpretation is purely set-theoretic.
<li><code>Empty</code> denotes the empty type (no value).</li>
......@@ -83,11 +84,18 @@ works for recursive patterns (for which there is no toplevel declarations).
There is an important restriction concerning recursive types:
any cycle must cross
any cycle must cross a <em>type constructor</em> (pairs, records, XML
elements, arrows). Boolean connectives do <em>not</em> count as type
constructors ! The code sample above is a correct definition.
The one below is invalid, because there is an unguarded cycle
between <code>T</code> and <code>S</code>.
type T = S | (S,S);; (* INVALID ! *)
type S = T;;
......@@ -191,7 +199,7 @@ Tuples are syntactic sugar for pairs. For instance,
<box title="Sequences" link="seq">
<section title="Expressions">
<section title="Values and expressions">
Sequences are fundamental in CDuce. They represents
......@@ -210,6 +218,8 @@ E.g.: <code>[ 1 2 3 4 ]</code>.
The binary operator <code>@</code> denotes sequence concatenation.
E.g.: <code>[ 1 2 3 ] @ [ 4 5 6 ]</code> evaluates to
<code>[ 1 2 3 4 5 6 ]</code>.
......@@ -286,6 +296,77 @@ in a pattern, e.g.: <code>[ x::Int* ; _ ]</code>.
<box title="Strings" link="string">
In CDuce, character strings are nothing but sequences of characters.
The type <code>String</code> is pre-defined as <code>[ Char* ]</code>.
This allows to use the full power of regular expression
pattern matching with strings.
Inside a regular expression type or pattern, it is possible
to use <code>PCDATA</code> instead of <code>Char*</code>
(note that both are not types on their own, they only make sense
inside square brackets, contrary to <code>String</code>).
<box title="Records" link="record">
Records are set of finite (name,value) bindings. They are used
in particular to represent XML attribute sets.
The syntax of a record expression is
<code>{ %%l1%% = %%e1%%; %%...%%; %%ln%% = %%en%% }</code>
where the <code>%%li%%</code> are label names (same lexical
conventions as for identifiers), and the <code>%%vi%%</code>
are expressions.
They are two kinds of record types. Open record types
are written <code>{ %%l1%% = %%t1%%; %%...%%; %%ln%% = %%tn%%
}</code>, and closed record types are written
<code>{ %%l1%% = %%t1%%; %%...%%; %%ln%% = %%tn%%
Both denote all the record values where
the labels <code>%%li%%</code> are present and the associated values
are in the corresponding type. The distinction is that that open
type allow extra fields, whereas the closed type gives a strict
enumeration of the possible fields.
Additionally, both for open and close record types,
it is possible to specify optional fields by using <code>=?</code>
instead of <code>=</code> between a label and a type.
For instance, <code>{| x = Int; y =? Bool |}</code>
represents records with an <code>x</code> field of type
<code>Int</code>, an optional field <code>y</code> (when it is
present, it has type <code>Bool</code>), and no other field.
Note that the value <code>{ x = 1; y = 2 }</code>
has actually the type <code>{| x = 1; y = 2 |}</code>
which is more precise than <code>{ x = 1; y = 2 }</code>. This is
the only situation where the singleton type corresponding to a constructed
value is not syntactically equal to this value.
The syntax is the same for patterns. Note that capture variables
cannot appear in an optional field.
<box title="XML elements" link="xml">
......@@ -317,6 +398,62 @@ can be written:
<code>&lt;a href=String>[]</code>.
The following sample shows several way to write XML types.
type A = <a x = String; y = String>[ A* ];;
type B = <(`x | `y)>[ ];;
type C = <c {| x = String; y = String |}>[ ];;
type U = { x = String; y =? String };;
type V = [ W* ];;
type W = <v (U)>V;;
<box title="Functions" link="fun">
CDuce is an higher-order functional languages: functions are
first-class citizen values, and can be passed as argument or returned
as result, stored in data structure, etc...
A functional type has the form <code>%%t%% -> %%s%%</code>
where <code>%%t%%</code> and <code>%%s%%</code> are types.
Intuitively, this type corresponds to functions that accept
(at least) any argument of type <code>%%t%%</code>, and for
such an argument, returns a value of type <code>%%s%%</code>.
For instance, the type <code>(Int,Int) -> Int &amp; (Char,Char) -> Char</code>
denotes functions that maps any pair of integer to an integer,
and any pair of characters to a character.
The explanation above gives the intuition behind the interpretation
of functional types. It is sufficient to understand which
subtyping relations and equivalences hold between (boolean
combination) of functional types. For instance,
<code>Int -> Int &amp; Char -> Char</code> is a subtype
of <code>(Int|Char) -> (Int|Char)</code> because
with the intuition above, a function of the first type,
when given a value of type <code>Int|Char</code> returns
a value of type <code>Int</code> or of type <code>Char</code>
(depending on the argument).
Formally, the type <code>%%t%% -> %%s%%</code> denotes
CDuce abstractions
<code>fun (%%t1%% -> %%s1%%; %%...%%; %%tn%% -> %%sn%%)...</code>
such that <code>%%t1%% -> %%s1%% &amp; %%...%% &amp; %%tn%% ->
%%sn%%</code> is a subtype of <code>%%t%% -> %%s%%</code>.
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment