Skip to content

Commit

Permalink
Alter the manual to speak of pure functions instead of predicate func…
Browse files Browse the repository at this point in the history
…tions.

Since the typestate system is gone, this makes more sense now.
  • Loading branch information
alexrp committed Aug 8, 2012
1 parent 52c5173 commit 81aef34
Showing 1 changed file with 12 additions and 19 deletions.
31 changes: 12 additions & 19 deletions doc/rust.md
Expand Up @@ -899,58 +899,51 @@ express that `f` requires no explicit `return`, as if it returns
control to the caller, it returns a value (true because it never returns
control).

#### Predicate functions
#### Pure functions

Any pure boolean function is called a *predicate function*, and may be used in
a [constraint](#constraints), as part of the static [typestate
system](#typestate-system). A predicate declaration is identical to a function
declaration, except that it is declared with the additional keyword `pure`. In
addition, the typechecker checks the body of a predicate with a restricted set
of typechecking rules. A predicate
A pure function declaration is identical to a function declaration, except that
it is declared with the additional keyword `pure`. In addition, the typechecker
checks the body of a pure function with a restricted set of typechecking rules.
A pure function

* may not contain an assignment or self-call expression; and
* may only call other predicates, not general functions.
* may only call other pure functions, not general functions.

An example of a predicate:
An example of a pure function:

~~~~
pure fn lt_42(x: int) -> bool {
return (x < 42);
}
~~~~

A non-boolean function may also be declared with `pure fn`. This allows
predicates to call non-boolean functions as long as they are pure. For example:
Pure functions may call other pure functions:

~~~~{.xfail-test}
pure fn pure_length<T>(ls: list<T>) -> uint { /* ... */ }
pure fn nonempty_list<T>(ls: list<T>) -> bool { pure_length(ls) > 0u }
~~~~

In this example, `nonempty_list` is a predicate---it can be used in a
typestate constraint---but the auxiliary function `pure_length` is
not.

*TODO:* should actually define referential transparency.

The effect checking rules previously enumerated are a restricted set of
typechecking rules meant to approximate the universe of observably
referentially transparent Rust procedures conservatively. Sometimes, these
rules are *too* restrictive. Rust allows programmers to violate these rules by
writing predicates that the compiler cannot prove to be referentially
writing pure functions that the compiler cannot prove to be referentially
transparent, using an escape-hatch feature called "unchecked blocks". When
writing code that uses unchecked blocks, programmers should always be aware
that they have an obligation to show that the code *behaves* referentially
transparently at all times, even if the compiler cannot *prove* automatically
that the code is referentially transparent. In the presence of unchecked
blocks, the compiler provides no static guarantee that the code will behave as
expected at runtime. Rather, the programmer has an independent obligation to
verify the semantics of the predicates they write.
verify the semantics of the pure functions they write.

*TODO:* last two sentences are vague.

An example of a predicate that uses an unchecked block:
An example of a pure function that uses an unchecked block:

~~~~
# import std::list::*;
Expand All @@ -972,7 +965,7 @@ pure fn pure_length<T>(ls: list<T>) -> uint {

Despite its name, `pure_foldl` is a `fn`, not a `pure fn`, because there is no
way in Rust to specify that the higher-order function argument `f` is a pure
function. So, to use `foldl` in a pure list length function that a predicate
function. So, to use `foldl` in a pure list length function that a pure function
could then use, we must use an `unchecked` block wrapped around the call to
`pure_foldl` in the definition of `pure_length`.

Expand Down

0 comments on commit 81aef34

Please sign in to comment.