Skip to content
GitLab
Menu
Projects
Groups
Snippets
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
cduce
cduce
Commits
03628a23
Commit
03628a23
authored
Jul 10, 2007
by
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
4c388a8e
Changes
1
Hide whitespace changes
Inline
Side-by-side
web/manual/types_patterns.xml
View file @
03628a23
...
@@ -26,7 +26,7 @@ or as a pair pattern of two type constraints.
...
@@ -26,7 +26,7 @@ or as a pair pattern of two type constraints.
</p>
</p>
<p>
<p>
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 recognize
s
.
It is also the occasion to present the CDuce values themselves, the
It is also the occasion to present the CDuce values themselves, the
corresponding expression constructions, and fundamental operations on them.
corresponding expression constructions, and fundamental operations on them.
</p>
</p>
...
@@ -35,7 +35,8 @@ 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"
>
<box
title=
"Boolean connectives"
link=
"bool"
>
<p>
<p>
CDuce recognize the full set of boolean connectives.
CDuce recognize the full set of boolean connectives, whose
interpretation is purely set-theoretic.
</p>
</p>
<ul>
<ul>
<li><code>
Empty
</code>
denotes the empty type (no value).
</li>
<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).
...
@@ -83,11 +84,18 @@ works for recursive patterns (for which there is no toplevel declarations).
<p>
<p>
There is an important restriction concerning recursive types:
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>
.
</p>
</p>
<sample>
<![CDATA[
type T = S | (S,S);; (* INVALID ! *)
type S = T;;
]]>
</sample>
</box>
</box>
...
@@ -191,7 +199,7 @@ Tuples are syntactic sugar for pairs. For instance,
...
@@ -191,7 +199,7 @@ Tuples are syntactic sugar for pairs. For instance,
<box
title=
"Sequences"
link=
"seq"
>
<box
title=
"Sequences"
link=
"seq"
>
<section
title=
"
E
xpressions"
>
<section
title=
"
Values and e
xpressions"
>
<p>
<p>
Sequences are fundamental in CDuce. They represents
Sequences are fundamental in CDuce. They represents
...
@@ -210,6 +218,8 @@ E.g.: <code>[ 1 2 3 4 ]</code>.
...
@@ -210,6 +218,8 @@ E.g.: <code>[ 1 2 3 4 ]</code>.
<p>
<p>
The binary operator
<code>
@
</code>
denotes sequence concatenation.
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>
.
</p>
</p>
<p>
<p>
...
@@ -286,6 +296,77 @@ in a pattern, e.g.: <code>[ x::Int* ; _ ]</code>.
...
@@ -286,6 +296,77 @@ in a pattern, e.g.: <code>[ x::Int* ; _ ]</code>.
</box>
</box>
<box
title=
"Strings"
link=
"string"
>
<p>
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.
</p>
<p>
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>
).
</p>
</box>
<box
title=
"Records"
link=
"record"
>
<p>
Records are set of finite (name,value) bindings. They are used
in particular to represent XML attribute sets.
</p>
<p>
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.
</p>
<p>
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%%
}
</code>
.
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.
</p>
<p>
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.
</p>
<p>
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.
</p>
<p>
The syntax is the same for patterns. Note that capture variables
cannot appear in an optional field.
</p>
</box>
<box
title=
"XML elements"
link=
"xml"
>
<box
title=
"XML elements"
link=
"xml"
>
<p>
<p>
...
@@ -317,6 +398,62 @@ can be written:
...
@@ -317,6 +398,62 @@ can be written:
<code>
<
a href=String>[]
</code>
.
<code>
<
a href=String>[]
</code>
.
</p>
</p>
<p>
The following sample shows several way to write XML types.
</p>
<sample>
<![CDATA[
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;;
]]>
</sample>
</box>
<box
title=
"Functions"
link=
"fun"
>
<p>
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...
</p>
<p>
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
&
(Char,Char) -> Char
</code>
denotes functions that maps any pair of integer to an integer,
and any pair of characters to a character.
</p>
<p>
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
&
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).
</p>
<p>
Formally, the type
<code>
%%t%% -> %%s%%
</code>
denotes
CDuce abstractions
<code>
fun (%%t1%% -> %%s1%%; %%...%%; %%tn%% -> %%sn%%)...
</code>
such that
<code>
%%t1%% -> %%s1%%
&
%%...%%
&
%%tn%% ->
%%sn%%
</code>
is a subtype of
<code>
%%t%% -> %%s%%
</code>
.
</p>
</box>
</box>
...
...
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment