Skip to content
GitLab
Projects
Groups
Snippets
Help
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Open sidebar
curry
report
Commits
b1e9dd5a
Commit
b1e9dd5a
authored
May 21, 2000
by
Michael Hanus
Browse files
Type synonyms added, prelude extended by enumFrom... and print
parent
95127c31
Changes
1
Hide whitespace changes
Inline
Side-by-side
Showing
1 changed file
with
104 additions
and
9 deletions
+104
-9
report.tex
report.tex
+104
-9
No files found.
report.tex
View file @
b1e9dd5a
% $Id: report.tex,v 1.
7
2000/02/
02 15:08:05
mh Exp mh $
% $Id: report.tex,v 1.
8
2000/02/
16 14:33:51
mh Exp mh $
% $Log: report.tex,v $
% Revision 1.8 2000/02/16 14:33:51 mh
% concatMap added in prelude
%
% Revision 1.7 2000/02/02 15:08:05 mh
% This is the official version 0.7 of the Curry report.
%
...
...
@@ -111,7 +114,7 @@
\begin{center}
\vspace
{
10ex
}
{
\Huge\bf
Curry
}
\\
[4ex]
{
\LARGE\bf
An Integrated Functional Logic Language
}
\\
[5ex]
{
\large\bf
Version 0.7
}
\\
[1ex]
{
\large\bf
Version 0.7
.1
}
\\
[1ex]
{
\large
\today
}
\\
[8ex]
\Large
Michael Hanus
$^
1
$
[editor]
\\
[3ex]
...
...
@@ -267,6 +270,50 @@ Note that traditional functional languages compute on ground expressions,
whereas logic languages also allow non-ground expressions.
\subsection
{
Type Synonym Declarations
}
\label
{
sec-typesyns
}
To make type definitions more readable, it is possible
to specify new names for type expressions by a
\emph
{
type synonym declaration
}
.
\index
{
type synonym declaration
}
\index
{
type!synonym declaration
}
\index
{
declaration!type synonym
}
Such a declaration has the general form
\startprog
type
$
T
$
$
\alpha
_
1
$
\ldots
$
\alpha
_
n
$
=
$
\tau
$
\stopprog
which introduces a new
$
n
$
-ary type constructor
\index
{
type constructor
}
$
T
$
.
$
\alpha
_
1
,
\ldots
,
\alpha
_
n
$
are pairwise distinct type variables
and
$
\tau
$
is a type expressions built from type constructors
and the type variables
$
\alpha
_
1
,
\ldots
,
\alpha
_
n
$
.
The type
\pr
{
(
$
T
$
$
\tau
_
1
\ldots
\tau
_
n
$
)
}
is equivalent to the
type
$
\{\alpha
_
1
\mapsto
\tau
_
1
,
\ldots
,
\alpha
_
n
\mapsto\tau
_
n
\}
(
\tau
)
$
,
i.e., the type expression
$
\tau
$
where each
$
\alpha
_
i
$
is replaced
by
$
\tau
_
i
$
. Thus, a type synonym and its definition
are always interchangeable and have no influence on the
typing of a program. For example, we can provide an alternative
notation for list types and strings by the following
type synonym declarations:
\startprog
type List a = [a]
type Name = [Char]
\stopprog
Since a type synonym introduces just another name for a type
expression, recursive or mutually dependent type synonym declarations
are not allowed. Therefore, the following declarations are
\emph
{
invalid
}
:
\startprog
type RecF a = a -> RecF a -- recursive definitions not allowed
type Place = [Addr] -- mutually recursive definitions not allowed
type Addr = [Place]
\stopprog
However, recursive definitions with an intervening datatype are allowed,
since recursive datatype definitions are also allowed.
For instance, the following definitions are valid:
\startprog
type Place = [Addr]
data Addr = Tag [Place]
\stopprog
\subsection
{
Function Declarations
}
\label
{
sec-funcdecl
}
...
...
@@ -1309,7 +1356,10 @@ basic type like \pr{Bool}, \pr{Success}, \pr{Int}, \pr{Float},
\pr
{
Char
}
(or any other type constructor of arity 0),
or a type constructor application of the form
\pr
{
(
$
T
\,\tau
_
1
\ldots\tau
_
n
$
)
}
where
$
T
$
is a type constructor of arity
$
n
$
,
as defined by a datatype declaration (cf.
\
Section~
\ref
{
sec-datatypes
}
),
as defined by a datatype declaration
(cf.
\
Section~
\ref
{
sec-datatypes
}
),
\footnote
{
We assume here that
all type constructors introduced by type synonyms
(cf.
\
Section~
\ref
{
sec-typesyns
}
) are replaced by their definitions.
}
and
$
\tau
_
1
,
\ldots
,
\tau
_
n
$
are type expressions
(note that list, tuple and function types have the
special syntax
\pr
{
[
$
\cdot
$
]
}
,
...
...
@@ -1339,8 +1389,12 @@ and an assignment of types for some local variables.
An expression
$
e
$
is
\emph
{
well-typed
}
\index
{
well-typed
}
and has type
$
\tau
$
w.r.t.
\
a type environment
$
\Ac
$
if
$
\Ac
\vdash
e::
\tau
$
is derivable according to the
following inference rules:
\[
inference rules shown in Figure~
\ref
{
fig-typing-rules
}
.
\begin{figure*}
[t]
\begin{center}
\fbox
{
$
\begin
{
array
}{
@
{}
ll
}
\mbox
{
Axiom:
}
&
\infrule
{}
...
...
@@ -1366,7 +1420,12 @@ following inference rules:
{
\Ac
\vdash
\pr
{
if
\,
}
e
_
1
\pr
{
\,
then
\,
}
e
_
2
\pr
{
\,
else
\,
}
e
_
3
::
\tau
}
\\
[
3
ex
]
\end
{
array
}
\]
$
}
% fbox
\end{center}
\vspace
{
-3ex
}
\caption
{
Typing rules for Curry programs
\label
{
fig-typing-rules
}}
\end{figure*}
A defining equation
\pr
{
~
$
f~t
_
1
\ldots
t
_
n
$
=
$
e
$
$
[
$
where
$
x
$
free
$
]
$
~
}
is well-typed
w.r.t.
\
a type environment
$
\Ac
$
if
...
...
@@ -2832,12 +2891,19 @@ data () = () \pindex{()}
~
data [a] = [] | a : [a]
\pindex
{
[]
}
\pindex
{
:
}
\pindex
{
[a]
}
\index
{
lists
}
~
-- First element of a list
head :: [a] -> a
\pindex
{
head
}
head (x:
_
) = x
~
-- Remaining elements of a list
tail :: [a] -> [a]
\pindex
{
tail
}
tail (
_
:xs) = xs
~
-- Is a list empty?
null :: [
_
] -> Bool
\pindex
{
null
}
null [] = True
null (
_
:
_
) = False
~
-- Concatenation
(++) :: [a] -> [a] -> [a]
\pindex
{
++
}
[] ++ ys = ys
...
...
@@ -2973,6 +3039,26 @@ unlines :: [String] -> String \pindex{unlines}
unlines ls = concatMap (++"
\ttbs
{}
n") ls
~
~
-- generating arithmetic enumeration lists:
enumFrom :: Int -> [Int] -- [n..]
\pindex
{
enumFrom
}
enumFrom n = n : enumFrom (n+1)
~
enumFromThen :: Int -> Int -> [Int] -- [n1,n2..]
\pindex
{
enumFromThen
}
enumFromThen n1 n2 = iterate ((n2-n1)+) n1
~
enumFromTo :: Int -> Int -> [Int] -- [n..m]
\pindex
{
enumFromTo
}
enumFromTo n m = if n>m then [] else n : enumFromTo (n+1) m
~
enumFromThenTo :: Int -> Int -> Int -> [Int] -- [n1,n2..m]
\pindex
{
enumFromThenTo
}
enumFromThenTo n1 n2 m = takeWhile p (enumFromThen n1 n2)
where p x | n2 >= n1 = (x <= m)
| otherwise = (x >= m)
~
~
-- Conversion functions between characters and their ASCII values
~
ord :: Char -> Int
\pindex
{
ord
}
...
...
@@ -3057,6 +3143,10 @@ getLine = getChar >>= \ttbs{}c ->
if c=='
\ttbs
{}
n' then return []
else getLine >>=
\ttbs
{}
cs -> return (c:cs)
~
-- Convert a term into a string and print it
print ::
_
-> IO ()
\pindex
{
print
}
print t = putStrLn (show t)
~
~
-- Encapsulated search
~
...
...
@@ -3299,13 +3389,18 @@ end
end
\production
BlockDeclaration
DataDeclaration
\por
FunctionDeclaration
TypeSynonymDecl
\por
DataDeclaration
\por
FunctionDeclaration
end
\production
TypeSynonymDecl
\term
{
type
}
TypeConstrID
\seq
{
TypeVarID
}{}{
n
}
\marg
{
n
\geqslant
0
}
\next
\term
{
=
}
TypeExpr
end
\production
DataDeclaration
\term
{
data
}
TypeDeclaration
% \offside{TypeDeclaration}{;}{n}
% \marg{n > 0}
end
\production
TypeDeclaration
...
...
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