This is mercury_ref.info, produced by makeinfo version 4.11 from
reference_manual.texi_pp.

INFO-DIR-SECTION The Mercury Programming Language
START-INFO-DIR-ENTRY
* Mercury Language: (mercury_ref).  The Mercury Language Reference Manual.
END-INFO-DIR-ENTRY

   This file documents the Mercury programming language, version 11.07.

   Copyright (C) 1995-2011 The University of Melbourne.

   Permission is granted to make and distribute verbatim copies of this
manual provided the copyright notice and this permission notice are
preserved on all copies.

   Permission is granted to copy and distribute modified versions of
this manual under the conditions for verbatim copying, provided also
that the entire resulting derived work is distributed under the terms
of a permission notice identical to this one.

   Permission is granted to copy and distribute translations of this
manual into another language, under the above conditions for modified
versions.


File: mercury_ref.info,  Node: Top,  Up: (mercury)

The Mercury Language Reference Manual, version 11.07
****************************************************

* Menu:

* Introduction::      A brief introduction to Mercury.
* Syntax::            Mercury's syntax is similar to ISO Prolog.
* Types::             Mercury has a strong parametric polymorphic type system.
* Modes::             Modes allow you to specify the direction of data flow.
* Unique modes::      Unique modes allow you to specify when there is only one
                      reference to a particular value, so the compiler can
                      safely use destructive update to modify that value.
* Determinism::       Determinism declarations let you specify that a predicate
                      should never fail or should never succeed more than once.
* User-defined equality and comparison::
                      User-defined types can have user-defined equality and
                      comparison predicates.
* Higher-order::      Mercury supports higher-order predicates and functions,
                      with closures, lambda expressions, and currying.
* Modules::           Modules allow you to divide a program into smaller parts.
* Type classes::      Constrained polymorphism.
* Existential types:: Support for data abstraction and heterogeneous
                      collections.
* Exception handling:: Catching exceptions to recover from exceptional
                      situations.
* Semantics::         Declarative and operational semantics of Mercury
                      programs.
* Foreign language interface:: Calling code written in other programming
                      languages from Mercury code
* Impurity::          Users can write impure Mercury code.
* Solver types::      Support for constraint logic programming
* Trace goals::       Trace goals allow programmers to add debugging and
                      logging code to their programs.
* Pragmas::           Various compiler directives, used for example to
                      control optimization.
* Implementation-dependent extensions::
                      The University of Melbourne Mercury implementation
                      supports several extensions to the Mercury language.
* Bibliography::      References for further reading.


File: mercury_ref.info,  Node: Introduction,  Next: Syntax,  Prev: Top,  Up: Top

1 Introduction
**************

Mercury is a new general-purpose programming language, designed and
implemented by a small group of researchers at the University of
Melbourne, Australia.  Mercury is based on the paradigm of purely
declarative programming, and was designed to be useful for the
development of large and robust "real-world" applications.  It improves
on existing logic programming languages by providing increased
productivity, reliability and efficiency, and by avoiding the need for
non-logical program constructs.  Mercury provides the traditional logic
programming syntax, but also allows the syntactic convenience of
user-defined functions, smoothly integrating logic and functional
programming into a single paradigm.

   Mercury requires programmers to supply type, mode and determinism
declarations for the predicates and functions they write.  The compiler
checks these declarations, and rejects the program if it cannot prove
that every predicate or function satisfies its declarations.  This
improves reliability, since many kinds of errors simply cannot happen
in successfully compiled Mercury programs.  It also improves
productivity, since the compiler pinpoints many errors that would
otherwise require manual debugging to locate.  The fact that
declarations are checked by the compiler makes them much more useful
than comments to anyone who has to maintain the program.  The compiler
also exploits the guaranteed correctness of the declarations for
significantly improving the efficiency of the code it generates.

   To facilitate programming-in-the-large, to allow separate
compilation, and to support encapsulation, Mercury has a simple module
system.  Mercury's standard library has a variety of pre-defined modules
for common programming tasks -- see the Mercury Library Reference
Manual.


File: mercury_ref.info,  Node: Syntax,  Next: Types,  Prev: Introduction,  Up: Top

2 Syntax
********

* Menu:

* Syntax Overview::
* Tokens::
* Terms::
* Builtin Operators::
* Items::
* Declarations::
* Facts::
* Rules::
* Goals::
* State variables::
* DCG-rules::
* DCG-goals::
* Data-terms::
* Variable scoping::
* Implicit quantification::
* Elimination of double negation::


File: mercury_ref.info,  Node: Syntax Overview,  Next: Tokens,  Up: Syntax

2.1 Syntax overview
===================

Mercury's syntax is similar to the syntax of Prolog, with some
additional declarations for types, modes, determinism, the module
system, and pragmas, and with the distinction that function symbols may
stand also for invocations of user-defined functions as well as for
data constructors.

   A Mercury program consists of a set of modules.  Each module is a
file containing a sequence of items (declarations and clauses).  Each
item is a term followed by a period.  Each term is composed of a
sequence of tokens, and each token is composed of a sequence of
characters.  Like Prolog, Mercury has the Definite Clause Grammar (DCG)
notation for clauses.


File: mercury_ref.info,  Node: Tokens,  Next: Terms,  Prev: Syntax Overview,  Up: Syntax

2.2 Tokens
==========

Tokens in Mercury are the same as in ISO Prolog.  The only differences
are the `#LINE' token, which is used as a line number directive (see
below) and the backquote (``') token.

   The different tokens are as follows.  Tokens may be separated by
whitespace or line number directives.

_line number directive_
     A line number directive consists of the character `#', a positive
     integer specifying the line number, and then a newline.  A `#LINE'
     directive's only role is to specifying the line number; it is
     otherwise ignored by the syntax.  Line number directives may occur
     anywhere a token may occur.  They are used in conjunction with the
     `pragma source_file' declaration to indicate that the Mercury code
     following was generated by another tool; they serve to associate
     each line in the Mercury code with the source file name and line
     number of the original source from which the Mercury code was
     derived, so that the Mercury compiler can issue more informative
     error messages using the original source code locations.  A
     `#LINE' directive specifies the line number for the immediately
     following line.  Line numbers for lines after that are incremented
     as usual, so the second line after a `#100' directive would be
     considered to be line number 101.

_string_
     A string is a sequence of characters enclosed in double quotes
     (`"').

     Within a string, two adjacent double quotes stand for a single
     double quote.  For example, the string ` """" ' is a string of
     length one, containing a single double quote: the outermost pair
     of double quotes encloses the string, and the innermost pair stand
     for a single double quote.

     Strings may also contain backslash escapes.  `\a' stands for
     "alert" (a beep character), `\b' for backspace, `\r' for
     carriage-return, `\f' for form-feed, `\t' for tab, `\n' for
     newline, `\v' for vertical-tab.  An escaped backslash,
     single-quote, or double-quote stands for itself.

     The sequence `\x' introduces a hexadecimal escape; it must be
     followed by a sequence of hexadecimal digits and then a closing
     backslash.  It is replaced with the character whose character code
     is identified by the hexadecimal number.  Similarly, a backslash
     followed by an octal digit is the beginning of an octal escape; as
     with hexadecimal escapes, the sequence of octal digits must be
     terminated with a closing backslash.

     The sequence `\u' or `\U' can be used to escape Unicode characters.
     `\u' must be followed by the Unicode character code expressed as
     four hexadecimal digits.  `\U' must be followed by the Unicode
     character code expressed as eight hexadecimal digits.  The highest
     allowed value is `\U0010FFFF'.

     A backslash followed immediately by a newline is deleted; thus an
     escaped newline can be used to continue a string over more than one
     source line.  (String literals may also contain embedded newlines.)

_name_
     A name is either an unquoted name or a quoted name.  An unquoted
     name is a lowercase letter followed by zero or more letters,
     underscores, and digits.  A quoted name is any sequence of zero or
     more characters enclosed in single quotes (`'').  Within a quoted
     name, two adjacent single quotes stand for a single single quote.
     Quoted names can also contain backslash escapes of the same form
     as for strings.

_variable_
     A variable is an uppercase letter or underscore followed by zero or
     more letters, underscores, and digits.  A variable token
     consisting of single underscore is treated specially: each
     instance of `_' denotes a distinct variable.  (In addition,
     variables starting with an underscore are presumed to be
     "don't-care" variables; the compiler will issue a warning if a
     variable that does not start with an underscore occurs only once,
     or if a variable starting with an underscore occurs more than once
     in the same scope.)

_integer_
     An integer is either a decimal, binary, octal, hexadecimal, or
     character-code literal.  A decimal literal is any sequence of
     decimal digits.  A binary literal is `0b' followed by any sequence
     of binary digits.  An octal literal is `0o' followed by any
     sequence of octal digits.  A hexadecimal literal is `0x' followed
     by any sequence of hexadecimal digits.  A character-code literal
     is `0'' followed by any single character.

_float_
     A floating point literal consists of a sequence of decimal digits,
     a decimal point and a sequence of digits (the fraction part), and
     the letter `E' (or `e'), an optional sign (`+' or `-'), and then
     another sequence of decimal digits (the exponent).  The fraction
     part or the exponent (but not both) may be omitted.

_implementation_defined_literal_
     An implementation-defined literal consists of a dollar sign (`$')
     followed by an unquoted name.

_open_ct_
     A left parenthesis, `(', that is not preceded by whitespace.

_open_
     A left parenthesis, `(', that is preceded by whitespace.

_close_
     A right parenthesis, `)'.

_open_list_
     A left square bracket, `['.

_close_list_
     A right square bracket, `]'.

_open_curly_
     A left curly bracket, `{'.

_close_curly_
     A right curly bracket, `}'.

_ht_sep_
     A "head-tail separator", i.e. a vertical bar, `|'.

_comma_
     A comma, `,'.

_end_
     A full stop (period), `.'.

_eof_
     The end of file.



File: mercury_ref.info,  Node: Terms,  Next: Builtin Operators,  Prev: Tokens,  Up: Syntax

2.3 Terms
=========

Syntactically, terms in Mercury are exactly the same as in ISO Prolog,
except that as extensions we permit higher-order terms and the
introduction of infix operators by the use of grave accents
(backquotes), as described below, and we support an extended set of
builtin operators.  *Note Builtin Operators::.  Also, the constructor
for list terms in Mercury is `[|]/2', not `./2' as in Prolog.

   Note, however, that the meaning of some terms in Mercury is
different to that in Prolog.  *Note Data-terms::.

   A term is either a variable or a functor.

   A functor is an integer, a float, a string, a name, a compound term,
or a higher-order term.

   A compound term is a simple compound term, a list term, a tuple term,
an operator term, or a parenthesized term.

   A simple compound term is a name followed without any intervening
whitespace by an open parenthesis (i.e. an open_ct token), a sequence
of argument terms separated by commas, and a close parenthesis.

   A list term is an open square bracket (i.e. an open_list token)
followed by a sequence of argument terms separated by commas,
optionally followed by a vertical bar (i.e. a ht_sep token) followed by
a term, followed by a close square bracket (i.e. a close_list token).
An empty list term is an open_list token followed by a close_list
token.  List terms are parsed as follows:
     parse('[' ']') = [].
     parse('[' List) = parse_list(List).
     parse_list(Head ',' Tail) = '[|]'(parse_term(Head), parse_list(Tail)).
     parse_list(Head '|' Tail ']') = '[|]'(parse_term(Head), parse_term(Tail)).
     parse_list(Head ']') = '[|]'(parse_term(Head), []).

   The following terms are all equivalent:
     [1, 2, 3]
     [1, 2, 3 | []]
     [1, 2 | [3]]
     [1 | [2, 3]]
     '[|]'(1, '[|]'(2, '[|]'(3, [])))

   A tuple term is a left curly bracket (i.e. an open_curly token)
followed by a sequence of argument terms separated by commas, and a
right curly bracket.  For example, `{1, '2', "three"}' is a valid tuple
term.

   An operator term is a term specified using operator notation, as in
Prolog.  Operators can also be formed by enclosing a name, a module
qualified name (*note The module system::), or a variable between grave
accents (backquotes).  Any name or variable may be used as an operator
in this way.  If FUN is a variable or name, then a term of the form `X
`FUN` Y' is equivalent to `FUN(X, Y)'. The operator is left associative
and binds more tightly than every operator other than `^' (*note
Builtin Operators::).

   A parenthesized term is just an open parenthesis followed by a term
and a close parenthesis.

   A higher-order term is a "closure" term, which can be any term other
than a name or an operator term, followed without any intervening
whitespace by an open parenthesis (i.e. an open_ct token), a sequence
of argument terms separated by commas, and a close parenthesis.  A
higher-order term is equivalent to a simple compound term whose functor
is the empty name, and whose arguments are the closure term followed by
the argument terms of the higher-order term.  That is, a term such as
`Term(Arg1, ..., ArgN)' is parsed as `''(Term, Arg1, ..., ArgN)'.  Note
that the closure term can be a parenthesized term; for example, `(Term
^ FieldName)(Arg1, Arg2)' is a higher-order term, and so it gets parsed
as if it were `''((Term ^ FieldName), Arg1, Arg2)'.


File: mercury_ref.info,  Node: Builtin Operators,  Next: Items,  Prev: Terms,  Up: Syntax

2.4 Builtin Operators
=====================

The following table lists all of Mercury's builtin operators.
Operators with a low "Priority" bind more tightly than those with a
high "Priority". For example, given that `+' has priority 500 and `*'
has priority 400, the term `2 * X + Y' would parse as `(2 * X) + Y'.

   The "Specifier" field indicates what structure terms constructed
with an operator are allowed to take.  "f" represents the operator and
"x" and "y" represent arguments.  "x" represents an argument whose
priority must be strictly lower than that of the operator.  "y"
represents an argument whose priority is lower or equal to that of the
operator.  For example, "yfx" indicates a left-associative infix
operator, while "xfy" indicates a right-associative infix operator.


     Operator                        Specifier         Priority

     .                               yfx               10
     !                               fx                40
     !.                              fx                40
     !:                              fx                40
     @                               xfx               90
     ^                               xfy               99
     ^                               fx                100
     :                               yfx               120
     `OP`                      yfx               120       (1)
     **                              xfy               200
     -                               fx                200
     \\                              fx                200
     *                               yfx               400
     /                               yfx               400
     //                              yfx               400
     <<                              yfx               400
     >>                              yfx               400
     div                             yfx               400
     mod                             xfx               400
     rem                             xfx               400
     +                               fx                500
     +                               yfx               500
     ++                              xfy               500
     -                               yfx               500
     --                              yfx               500
     /\\                             yfx               500
     \\/                             yfx               500
     ..                              xfx               550
     :=                              xfx               650
     =^                              xfx               650
     <                               xfx               700
     =                               xfx               700
     =..                             xfx               700
     =:=                             xfx               700
     =<                              xfx               700
     ==                              xfx               700
     =\\=                            xfx               700
     >                               xfx               700
     >=                              xfx               700
     @<                              xfx               700
     @=<                             xfx               700
     @>                              xfx               700
     @>=                             xfx               700
     \\=                             xfx               700
     \\==                            xfx               700
     ~=                              xfx               700
     is                              xfx               701
     and                             xfy               720
     or                              xfy               740
     func                            fx                800
     impure                          fy                800
     pred                            fx                800
     semipure                        fy                800
     \\+                             fy                900
     not                             fy                900
     when                            xfx               900
     ~                               fy                900
     <=                              xfy               920
     <=>                             xfy               920
     =>                              xfy               920
     all                             fxy               950
     arbitrary                       fxy               950
     promise_equivalent_solutions    fxy               950
     promise_equivalent_solution_sets fxy              950
     promise_exclusive               fy                950
     promise_exclusive_exhaustive    fy                950
     promise_exhaustive              fy                950
     promise_impure                  fx                950
     promise_pure                    fx                950
     promise_semipure                fx                950
     require_complete_switch         fxy               950
     require_det                     fx                950
     require_semidet                 fx                950
     require_multi                   fx                950
     require_nondet                  fx                950
     require_cc_multi                fx                950
     require_cc_nondet               fx                950
     require_erroneous               fx                950
     require_failure                 fx                950
     some                            fxy               950
     ,                               xfy               1000
     &                               xfy               1025
     ->                              xfy               1050
     ;                               xfy               1100
     then                            xfx               1150
     if                              fx                1160
     else                            xfy               1170
     ::                              xfx               1175
     ==>                             xfx               1175
     where                           xfx               1175
     --->                            xfy               1179
     type                            fx                1180
     solver                          fy                1181
     end_module                      fx                1199
     import_module                   fx                1199
     include_module                  fx                1199
     initialise                      fx                1199
     initialize			fx		  1199
     finalise			fx		  1199
     finalize			fx		  1199
     inst                            fx                1199
     instance                        fx                1199
     mode                            fx                1199
     module                          fx                1199
     pragma                          fx                1199
     promise                         fx                1199
     rule                            fx                1199
     typeclass                       fx                1199
     use_module                      fx                1199
     -->                             xfx               1200
     :-                              fx                1200
     :-                              xfx               1200
     ?-                              fx                1200

   ---------- Footnotes ----------

   (1) Operator term (*note Terms::).


File: mercury_ref.info,  Node: Items,  Next: Declarations,  Prev: Builtin Operators,  Up: Syntax

2.5 Items
=========

Each item in a Mercury module is either a declaration or a clause.  If
the top-level functor of the term is `:-/1', the item is a declaration,
otherwise it is a clause.  There are three types of clauses.  If the
top-level functor of the item is `:-/2', the item is a rule.  If the
top-level functor is `-->/2', the item is a DCG rule.  Otherwise, the
item is a fact.  There are two types of rules and facts.  If the
top-level functor of the head of a rule is `=/2', the rule is a
function rule, otherwise it is a predicate rule.  If the top-level
functor of the head of a fact is `=/2', the fact is a function fact,
otherwise it is a predicate fact.


File: mercury_ref.info,  Node: Declarations,  Next: Facts,  Prev: Items,  Up: Syntax

2.6 Declarations
================

The allowed declarations are:

     :- type
     :- solver type
     :- pred
     :- func
     :- inst
     :- mode
     :- typeclass
     :- instance
     :- pragma
     :- promise
     :- initialise
     :- finalise
     :- mutable
     :- module
     :- interface
     :- implementation
     :- import_module
     :- use_module
     :- include_module
     :- end_module

   The `type', `pred' and `func' declarations are used for the type
system, the `inst' and `mode' declarations are for the mode system, the
`pragma' declarations are for the foreign language interface, and for
compiler hints about inlining, and the remainder are for the module
system.  They are described in more detail in their respective chapters.


File: mercury_ref.info,  Node: Facts,  Next: Rules,  Prev: Declarations,  Up: Syntax

2.7 Facts
=========

A function fact is an item of the form `HEAD = RESULT'.  A predicate
fact is an item of the form `HEAD', where the top-level functor of HEAD
is not `:-/1', `:-/2', `-->/2', or `=/2'.  In both cases, the HEAD term
must not be a variable.  The top-level functor of the HEAD determines
which predicate or function the fact belongs to; the predicate or
function must have been declared in a preceding `pred' or `func'
declaration in this module.  The RESULT (if any) and the arguments of
the HEAD must be valid data-terms (optionally annotated with a mode
qualifier; see *note Different clauses for different modes::).

   A fact is equivalent to a rule whose body is `true'.


File: mercury_ref.info,  Node: Rules,  Next: Goals,  Prev: Facts,  Up: Syntax

2.8 Rules
=========

A function rule is an item of the form `HEAD = RESULT :- BODY'.  A
predicate rule is an item of the form `HEAD :- BODY' where the top-level
functor of `Head' is not `=/2'.  In both cases, the HEAD term must not
be a variable.  The top-level functor of the HEAD determines which
predicate or function the clause belongs to; the predicate or function
must have been declared in a preceding `pred' or `func' declaration in
this module.  The RESULT and the arguments of the HEAD must be valid
data-terms (optionally annotated with a mode qualifier; see *note
Different clauses for different modes::).  The BODY must be a valid
goal.


File: mercury_ref.info,  Node: Goals,  Next: State variables,  Prev: Rules,  Up: Syntax

2.9 Goals
=========

A goal is a term of one of the following forms:

`some VARS GOAL'
     An existential quantification.  VARS must be a list of variables.
     GOAL must be a valid goal.

     Each existential quantification introduces a new scope.  The
     variables in VARS are local to the goal GOAL: for each variable
     named in VARS, any occurrences of variables with that name in GOAL
     are considered to name a different variable than any variables
     with the same name that occur outside of the existential
     quantification.

     Operationally, existential quantification has no effect, so apart
     from its effect on variable scoping, `some VARS GOAL' is the same
     as `GOAL'.

     Mercury's rules for implicit quantification (*note Implicit
     quantification::) mean that variables are often implicitly
     existentially quantified.  There is usually no need to write
     existential quantifiers explicitly.

`all VARS GOAL'
     A universal quantification.  VARS must be a list of variables.
     GOAL must be a valid goal.  This is an abbreviation for `not (some
     VARS not GOAL)'.

`GOAL1, GOAL2'
     A conjunction.  GOAL1 and GOAL2 must be valid goals.

`GOAL1 & GOAL2'
     A parallel conjunction.  This has the same declarative semantics
     as the normal conjunction.  Operationally, implementations may
     execute GOAL1 & GOAL2 in parallel.  The order in which parallel
     conjuncts begin execution is not fixed.  It is an error for GOAL1
     or GOAL2 to have a determinism other than `det' or `cc_multi'.
     *Note Determinism categories::.

`GOAL1 ; GOAL2'
     where GOAL1 is not of the form `Goal1a -> Goal1b': a disjunction.
     GOAL1 and GOAL2 must be valid goals.

`true'
     The empty conjunction.  Always succeeds.

`fail'
     The empty disjunction.  Always fails.

`not GOAL'
`\+ GOAL'
     A negation.  The two different syntaxes have identical semantics.
     GOAL must be a valid goal.  Both forms are equivalent to `if GOAL
     then fail else true'.

`GOAL1 => GOAL2'
     An implication.  This is an abbreviation for `not (GOAL1, not
     GOAL2)'.

`GOAL1 <= GOAL2'
     A reverse implication.  This is an abbreviation for `not (GOAL2,
     not GOAL1)'.

`GOAL1 <=> GOAL2'
     A logical equivalence.  This is an abbreviation for `(GOAL1 =>
     GOAL2), (GOAL1 <= GOAL2').

`if CONDGOAL then THENGOAL else ELSEGOAL'
`CONDGOAL -> THENGOAL ; ELSEGOAL'
     An if-then-else.  The two different syntaxes have identical
     semantics.  CONDGOAL, THENGOAL, and ELSEGOAL must be valid goals.
     Note that the "else" part is _not_ optional.

     The declarative semantics of an if-then-else is given by `(
     CONDGOAL, THENGOAL ; not(CONDGOAL), ELSEGOAL)', but the
     operational semantics are different, and it is treated differently
     for the purposes of determinism inference (*note Determinism::).
     Operationally, it executes the CONDGOAL, and if that succeeds, then
     execution continues with the THENGOAL; otherwise, i.e. if CONDGOAL
     fails, it executes the ELSEGOAL.  Note that CONDGOAL can be
     nondeterministic -- unlike Prolog, Mercury's if-then-else does not
     commit to the first solution of the condition if the condition
     succeeds.

     If CONDGOAL is an explicit existential quantification, `some VARS
     QUANTIFIEDCONDGOAL', then the variables VARS are existentially
     quantified over the conjunction of the goals QUANTIFIEDCONDGOAL
     and THENGOAL.  Explicit existential quantifications that occur as
     subgoals of CONDGOAL do _not_ affect the scope of variables in the
     "then" part.  For example, in
             ( if some [V] C then T else E )
     the variable V is quantified over the conjunction of the goals C
     and T because the top-level goal of the condition is an explicit
     existential quantification, but in
             ( if true, some [V] C then T else E )
     the variable V is only quantified over C because the top-level
     goal of the condition is not an explicit existential
     quantification.

`TERM1 = TERM2'
     A unification.  TERM1 and TERM2 must be valid data-terms.

`TERM1 \= TERM2'
     An inequality.  TERM1 and TERM2 must be valid data-terms.  This is
     an abbreviation for `not (TERM1 = TERM2)'.

`call(Closure)'
`call(Closure1, Arg1)'
`call(Closure2, Arg1, Arg2)'
`call(Closure3, Arg1, Arg2, Arg3)'
...
     A higher-order predicate call.  The closure and arguments must be
     valid data-terms.  `call(Closure)' just calls the specified
     closure.  The other forms append the specified arguments onto the
     argument list of the closure before calling it.  *Note
     Higher-order::.

`Var'
`Var(Arg1)'
`Var(Arg2)'
`Var(Arg2, Arg3)'
...
     A higher-order predicate call.  VAR must be a variable.  The
     semantics are exactly the same as for the corresponding
     higher-order call using the `call/N' syntax, i.e.  `call(Var)',
     `call(Var, Arg1)', etc.

`promise_pure GOAL'
     A purity cast.  GOAL must be a valid goal.  This goal promises
     that GOAL implements a pure interface, even though it may include
     impure and semipure components.

`promise_semipure GOAL'
     A purity cast.  GOAL must be a valid goal.  This goal promises
     that GOAL implements a semipure interface, even though it may
     include impure components.

`promise_impure GOAL'
     A purity cast.  GOAL must be a valid goal.  This goal instructs
     the compiler to treat GOAL as though it were impure, regardless of
     its actual purity.

`promise_equivalent_solutions VARS GOAL'
     A determinism cast.  VARS must be a list of variables.  GOAL must
     be a valid goal.  This goal promises that VARS is the set of
     variables bound by GOAL, and that while GOAL may have more than
     one solution, all of these solutions are equivalent with respect
     to the equality theories of the variables in VARS.  It is an error
     for VARS to include a variable not bound by GOAL or for GOAL to
     bind a non-local variable that is not listed in VARS (non-local
     variables with inst ANY are assumed to be further constrained by
     GOAL and must also be included in VARS).  If GOAL has determinism
     `multi' or `cc_multi' then `promise_equivalent_solutions VARS GOAL'
     has determinism `det'.  If GOAL has determinism `nondet' or
     `cc_nondet' then `promise_equivalent_solutions VARS GOAL' has
     determinism `semidet'.

`promise_equivalent_solution_sets VARS GOAL'
     A determinism cast, of the kind performed by
     `promise_equivalent_solutions', on any goals of the form
     `arbitrary ARBVARS ARBGOAL' inside GOAL, of which there should be
     at least one.  VARS and ARBVARS must be lists of variables, and
     GOAL and ARBGOAL must be valid goals.  VARS must be the set of
     variables bound by GOAL, and ARBVARS must be the set of variables
     bound by ARBGOAL, It is an error for VARS to include a variable
     not bound by GOAL or for GOAL to bind a non-local variable that is
     not listed in VARS, and similarly for ARBVARS and ARBGOAL.  The
     intersection of VARS and the ARBVARS list of any `arbitrary
     ARBVARS ARBGOAL' goal included inside GOAL must be empty.

     The overall PROMISE_EQUIVALENT_SOLUTION_SETS goal promises that
     the set of solutions computed for VARS by GOAL is not influenced
     by which of the possible solutions for ARBVARS is computed by each
     ARBGOAL; while different choices of solutions for some of the
     ARBGOALs may lead to syntactically different solutions for VARS
     for GOAL, all of these solutions are equivalent with respect to
     the equality theories of the variables in VARS.  If an ARBGOAL has
     determinism `multi' or `cc_multi' then `arbitrary ARBVARS ARBGOAL'
     has determinism `det'.  If ARBGOAL has determinism `nondet' or
     `cc_nondet' then `arbitrary ARBVARS ARBGOAL' has determinism
     `semidet'.  GOAL itself may have any determinism.

     There is no requirement that given one of the ARBGOALs, all its
     solutions must be equivalent with respect to the equality theories
     of the corresponding ARBVARS; in fact, in typical usage, this
     won't be the case.  The different solutions of the nested
     ARBITRARY goals are not required to be equivalent in any context
     except the PROMISE_EQUIVALENT_SOLUTION_SETS goal they are nested
     inside.

     Goals of the form `arbitrary ARBVARS ARBGOAL' are not allowed to
     occur outside `promise_equivalent_solution_sets VARS GOAL' goals.

`require_det GOAL'
`require_semidet GOAL'
`require_multi GOAL'
`require_nondet GOAL'
`require_cc_multi GOAL'
`require_cc_nondet GOAL'
`require_erroneous GOAL'
`require_failure GOAL'
     A determinism check, typically used to enhance the robustness of
     code.  GOAL must be a valid goal.  If GOAL is det, then
     `require_det GOAL' is equivalent to just GOAL.  If GOAL is not det,
     then the compiler is required to generate an error message.

     The `require_det' keyword may be replaced with `require_semidet',
     `require_multi', `require_nondet', `require_cc_multi',
     `require_cc_nondet', `require_erroneous' or `require_failure',
     each of which requires GOAL to have the named determinism.

`require_complete_switch [VAR] GOAL'
     A switch completeness check, typically used to enhance the
     robustness of code.  If GOAL is a complete switch on VAR, i.e. a
     switch that has an arm for all the function symbols in the type of
     VAR, then `require_complete_switch [VAR] GOAL' is equivalent to
     GOAL.  If GOAL is a switch on VAR but it is not a complete switch,
     i.e. it has no arm for at least one of the function symbols in the
     type of VAR, then the compiler is required to generate an error
     message.  If GOAL is not a switch on VAR, then
     `require_complete_switch [VAR] GOAL' is equivalent to GOAL.  This
     is intended to allow these scopes to be used even if VAR is input
     to the scope only in some but not all modes of the containing
     predicate.

`trace PARAMS GOAL'
     A trace goal, typically used for debugging or logging.  GOAL must
     be a valid goal; PARAMS must be a valid list of trace parameters.
     Some trace parameters specify compile time or run time conditions;
     if any of these conditions are false, GOAL will not be executed.
     Since in some program invocations GOAL may be replaced by `true'
     in this way, GOAL may not bind or change the instantiation state
     of any variables it shares with the surrounding context.  The
     things it may do are thus restricted to side effects; good
     programming style requires these side effects to not have any
     affect on the execution of the program itself, but to be confined
     to the provision of extra information for the user of the program.
     See *note Trace goals:: for the details.

`try PARAMS GOAL ... catch TERM -> CGOAL ...'
     A try goal. Exceptions thrown during the execution of GOAL may be
     caught and handled. A summary of the try goal syntax is:

              try PARAMS GOAL
              then THENGOAL
              else ELSEGOAL
              catch TERM -> CATCHGOAL
              ...
              catch_any CATCHANYVAR -> CATCHANYGOAL

     See *note Exception handling:: for the full details.

`event GOAL'
     An event goal.  GOAL must be a predicate call.  Event goals are an
     extension used by the Melbourne Mercury implementation to support
     user defined events in the Mercury debugger, `mdb'.  See the
     "Debugging" chapter of the Mercury User's Guide for further
     details.

`CALL'
     Any goal which does not match any of the above forms must be a
     predicate call.  The top-level functor of the term determines the
     predicate called; the predicate must be declared in a `pred'
     declaration in the module or in the interface of an imported
     module.  The arguments must be valid data-terms.



File: mercury_ref.info,  Node: State variables,  Next: DCG-rules,  Prev: Goals,  Up: Syntax

2.10 State variables
====================

Clauses may use `state variables' as a shorthand for naming
intermediate values in a sequence.  That is, where in the plain syntax
one might write
     	main(IO0, IO) :-
     		io.write_string("The answer is ", IO0, IO1),
     		io.write_int(calculate_answer(...), IO1, IO2),
     		io.nl(IO3, IO).
   using state variable syntax one could write
     	main(!IO) :-
     		io.write_string("The answer is ", !IO),
     		io.write_int(calculate_answer(...), !IO),
     		io.nl(!IO).

   A state variable is written `!.X' or `!:X', denoting the "current"
or "next" value of the sequence labelled X.  An argument `!X' is
shorthand for two state variable arguments `!.X, !:X'; that is, `p(...,
!X, ...)' is parsed as `p(..., !.X, !:X, ...)'.

   Within each clause, a transformation converts state variables into
sequences of ordinary logic variables.  The syntactic conversion is
described in terms of the notional `transform' function defined next.

   The transformation is applied once for each state variable X with
some fresh variables which we shall call THISX and NEXTX.

   The expression `substitute(TERM, X, THISX, NEXTX)' stands for a copy
of TERM with free occurrences of `!.X' replaced with THISX and free
occurrences of `!:X' replaced with NEXTX (a free occurrence is one not
bound by the head of a clause or lambda or by explicit quantification.)

   State variables obey the special scope rules.  A state variable X
must be explicitly introduced either in the head of the clause or
lambda (in which case it may appear as either or both of `!.X' or
`!:X') or in an explicit quantification (in which case it must appear
as `!X'.)  A state variable X in the enclosing scope of a lambda or
if-then-else expression may only be referred to as `!.X' (unless the
enclosing X is masked by a more local state variable of the same name.)

   For instance, the following clause employing a lambda expression
             p(A, B, !S) :-
                     F = (pred(C::in, D::out) is det :-
                             q(C, D, !S)
                     ),
                     ( F(A, E) ->
                             B = E
                     ;
                             B = A
                     ).
   is illegal because it implicitly refers to `!:S' inside the lambda
expression.  However
             p(A, B, !S) :-
                     F = (pred(C::in, D::out, !.S::in, !:S::out) is det :-
                             q(C, D, !S)
                     ),
                     ( F(A, E, !S) ->
                             B = E
                     ;
                             B = A
                     ).
   is acceptable because the state variable S accessed inside the
lambda expression is locally scoped to the lambda expression (shadowing
the state variable of the same name outside the lambda expression), and
the lambda expression may refer to the next version of a local state
variable.

   There are three restrictions concerning state variables in lambdas:
first, `!X' is not a legitimate function result, since it stands for two
arguments, rather than one; second, `!X' may not appear as a parameter
term in the head of a lambda since there is no syntax for specifying
the modes of the two implied parameters; third, `!X' may not appear as
an argument in a function application since this would not make sense
given the usual interpretation of state variables and functions.

`HEAD :- BODY'
          transform((HEAD :- BODY), X, THISX, NEXTX) =
          substitute(HEAD, X, THISX, NEXTX) :- transform(BODY, X, THISX, NEXTX)

`HEAD --> BODY'
          transform((HEAD --> BODY), X, THISX, NEXTX) =
          substitute(HEAD, X, THISX, NEXTX) :- transform(BODY, X, THISX, NEXTX)

`GOAL1, GOAL2'
          transform((GOAL1, GOAL2), X, THISX, NEXTX) =
          transform(GOAL1, X, THISX, TMPX), transform(GOAL2, X, TMPX, NEXTX)
     for some fresh variable TMPX.

`GOAL1 ; GOAL2'
          transform((GOAL1 ; GOAL2), X, THISX, NEXTX) =
          transform(GOAL1, X, THISX, NEXTX) ; transform(GOAL2, X, THISX, NEXTX)

`not GOAL'

`\+ GOAL'
     A negation.  The two different syntaxes have identical semantics.
          transform((not GOAL), X, THISX, NEXTX) =
          not transform(GOAL1, X, THISX, DUMMYX), NEXTX = THISX
     for some fresh variable DUMMYX.

`if GOAL1 then GOAL2 else GOAL3'

`GOAL1 -> GOAL2 ; GOAL3'
     An if-then-else.  The two different syntaxes have identical
     semantics.
          transform((if GOAL1 then GOAL2 else GOAL3), X, THISX, NEXTX) =
          if transform(GOAL1, X, THISX, TMPX) then transform(GOAL2, X, TMPX,  NEXTX)
                                              else transform(GOAL3, X, THISX, NEXTX)
     for some fresh variable TMPX.

`GOAL1 => GOAL2'

`GOAL2 <= GOAL1'
     An implication.  The two different syntaxes have identical
     semantics.
          transform((GOAL1 => GOAL2), X, THISX, NEXTX) =
          transform(GOAL1, X, THISX, TMPX) => transform(GOAL2, X, TMPX,  NEXTX),
          NEXTX = THISX
     for some fresh variable TMPX.

`all VARS GOAL'
          transform((all VARS GOAL), X, THISX, NEXTX) =
          all VARS transform(GOAL, X, THISX, DUMMYX), NEXTX = THISX
     for some fresh variable DUMMYX.

`some VARS GOAL'
          transform((some VARS GOAL), X, THISX, NEXTX) =
          some VARS transform(GOAL, X, THISX, NEXTX)

`!X ^ FIELD_LIST := TERM'
     A field update.  Replaces a field in the argument.  TERM must be a
     valid data-term.  FIELD_LIST must be a valid field list.  *Note
     Record syntax::.
          transform((!X ^ FIELD_LIST := TERM), X, THISX, NEXTX) =
          NextX = ThisX ^ field_list := Term

`CALL_OR_UNIFICATION'
     If `!:X' does not appear in CALL_OR_UNIFICATION then
          transform(CALL_OR_UNIFICATION, X, THISX, NEXTX) =
          substitute(CALL_OR_UNIFICATION, X, THISX, NEXTX), NEXTX = THISX
     If `!:X' does appear in CALL_OR_UNIFICATION then
          transform(CALL_OR_UNIFICATION, X, THISX, NEXTX) =
          substitute(CALL_OR_UNIFICATION, X, THISX, NEXTX)


   This transformation can lead to the introduction of chains of
unifications for variables that do not otherwise play a role in the
definition.  Such chains are removed transparently.

   The following code fragments illustrate appropriate use of state
variable syntax.

Threading the I/O state
          main(!IO) :-
          	io.write_string("The 100th prime is ", !IO),
          	X = prime(100),
          	io.write_int(X, !IO),
          	io.nl(!IO).

Handling accumulators (1)
          foldl2(_, [], !A, !B).

          foldl2(P, [X | Xs], !A, !B) :-
          	P(X, !A, !B),
          	foldl2(P, Xs, !A, !B).

Handling accumulators (2)
          iterate_while2(P, F, !A, !B) :-
          	( if P(!.A, !.B) then
          		F(!A, !B),
          		iterate_while2(P, F, !A, !B)
          	  else
          	  	true
          	).


File: mercury_ref.info,  Node: DCG-rules,  Next: DCG-goals,  Prev: State variables,  Up: Syntax

2.11 DCG-rules
==============

(DCG notation is intended for writing parsers and sequence generators
in a particular style; in the past it has also been used to thread an
implicit state variable, typically the I/O state, through code.  As a
matter of style, we recommend that in future DCG notation be reserved
for writing parsers and sequence generators and that state variable
syntax be used for passing state threads.)

   DCG-rules in Mercury have identical syntax and semantics to
DCG-rules in Prolog.

   A DCG-rule is an item of the form `HEAD --> BODY'.  The HEAD term
must not be a variable.  A DCG-rule is an abbreviation for an ordinary
rule with two additional implicit arguments appended to the arguments
of HEAD.  These arguments are fresh variables which we shall call V_IN
and V_OUT.  The BODY must be a valid DCG-goal, and is an abbreviation
for an ordinary goal.  The next section defines a mathematical function
`DCG-transform(V_IN, V_OUT, DCG-GOAL)' which specifies the semantics of
how DCG goals are transformed into ordinary goals.  (The
`DCG-transform' function is purely for the purposes of exposition, to
define the semantics -- it is not part of the language.)


File: mercury_ref.info,  Node: DCG-goals,  Next: Data-terms,  Prev: DCG-rules,  Up: Syntax

2.12 DCG-goals
==============

A DCG-goal is a term of one of the following forms:

`some VARS DCG-GOAL'
     A DCG existential quantification.  VARS must be a list of
     variables.  DCG-GOAL must be a valid DCG-goal.

     Semantics:
          transform(V_in, V_out, some Vars DCG_goal) =
          some Vars transform(V_in, V_out, DCG_goal)

`all VARS DCG-GOAL'
     A DCG universal quantification.  VARS must be a list of variables.
     DCG-GOAL must be a valid DCG-goal.

     Semantics:
          transform(V_in, V_out, all Vars DCG_goal) =
          all Vars transform(V_in, V_out, DCG_goal)

`DCG-GOAL1, DCG-GOAL2'
     A DCG sequence.  Intuitively, this means "parse DCG-goal1 and then
     parse DCG-goal2" or "do DCG-goal1 and then do DCG-goal2".  (Note
     that the only way this construct actually forces the desired
     sequencing is by the modes of the implicit DCG arguments.)
     DCG-GOAL1 and DCG-GOAL2 must be valid DCG-goals.

     Semantics:
          transform(V_in, V_out, (DCG-goal1, DCG-goal2)) =
          (transform(V_in, V_new, DCG_goal1),
           transform(V_new, V_out, DCG_goal2))
     where V_new is a fresh variable.

`DCG-GOAL1 ; DCG-GOAL2'
     A disjunction.  DCG-GOAL1 and DCG-GOAL2 must be valid goals.
     DCG-GOAL1 must not be of the form `DCG-goal1a -> DCG-goal1b'.  (If
     it is, then the goal is an if-then-else, not a disjunction.)

     Semantics:
          transform(V_in, V_out, (DCG_goal1 ; DCG_goal2)) =
          ( transform(V_in, V_out, DCG_goal1)
          ; transform(V_in, V_out, DCG_goal2) )

`{ GOAL }'
     A brace-enclosed ordinary goal.  GOAL must be a valid goal.

     Semantics:
          transform(V_in, V_out, { Goal }) = (Goal, V_out = V_in)

`[TERM, ...]'
     A DCG input match.  Unifies the implicit DCG input variable V_in,
     which must have type `list(_)', with a list whose initial elements
     are the terms specified and whose tail is the implicit DCG output
     variable V_out.  The terms must be valid data-terms.

     Semantics:
          transform(V_in, V_out, [Term1, ...]) = (V_in = [Term, ... | V_Out])

`[]'
     The null DCG goal (an empty DCG input match).  Equivalent to `{
     true }'.

     Semantics:
          transform(V_in, V_out, []) = (V_out = V_in)

`not DCG-GOAL'
`\+ DCG-GOAL'
     A DCG negation.  The two different syntaxes have identical
     semantics.  GOAL must be a valid goal.

     Semantics:
          transform(V_in, V_out, not DCG_goal) =
          (not transform(V_in, V_new, DCG_goal), V_out = V_in)
     where V_new is a fresh variable.

`if CONDGOAL then THENGOAL else ELSEGOAL'
`CONDGOAL -> THENGOAL ; ELSEGOAL'
     A DCG if-then-else.  The two different syntaxes have identical
     semantics.  CONDGOAL, THENGOAL, and ELSEGOAL must be valid
     DCG-goals.

     Semantics:
          transform(V_in, V_out, if CondGoal then ThenGoal else ElseGoal) =
          if transform(V_in, V_cond, CondGoal) then
                  transform(V_cond, V_out, ThenGoal)
          else
                  transform(V_in, V_out, ElseGoal)

`=(TERM)'
     A DCG unification.  Unifies TERM with the implicit DCG argument.
     TERM must be a valid data-term.

     Semantics:
          transform(V_in, V_out, =(Term)) = (Term = V_in, V_out = V_in)

`:=(TERM)'
     A DCG output unification.  Unifies TERM with the implicit DCG
     output argument, ignoring the input DCG argument.  TERM must be a
     valid data-term.

     Semantics:
          transform(V_in, V_out, :=(Term)) = (V_out = Term)

`TERM =^ FIELD_LIST'
     A DCG field selection.  Unifies TERM with the result of applying
     the field selection FIELD_LIST to the implicit DCG argument.  TERM
     must be a valid data-term.  FIELD_LIST must be a valid field list.
     *Note Record syntax::.

     Semantics:
          transform(V_in, V_out, Term =^ field_list) =
                  (Term = V_in ^ field_list, V_out = V_in)

`^ FIELD_LIST := TERM'
     A DCG field update.  Replaces a field in the implicit DCG argument.
     TERM must be a valid data-term.  FIELD_LIST must be a valid field
     list.  *Note Record syntax::.

     Semantics:
          transform(V_in, V_out, ^ field_list := Term) =
                  (V_out = V_in ^ field_list := Term)

`DCG-CALL'
     Any term which does not match any of the above forms must be a DCG
     predicate call.  If the term is a variable VAR, it is treated as
     if it were `call(VAR)'.  Then, the two implicit DCG arguments are
     appended to the specified arguments.

     Semantics:
          transform(V_in, V_out, p(A1, ..., AN)) =
          p(A1, ..., AN, V_in, V_out)



File: mercury_ref.info,  Node: Data-terms,  Next: Variable scoping,  Prev: DCG-goals,  Up: Syntax

2.13 Data-terms
===============

Syntactically, a data-term is just a term.

   There are a couple of differences from Prolog.  The first one is
that double-quoted strings are atomic in Mercury, they are not
abbreviations for lists of character codes.  The second is that Mercury
provides several extensions to Prolog's term syntax: Mercury terms may
contain record field selection and field update expressions,
conditional (if-then-else) expressions, function applications,
higher-order function applications, lambda expressions, and explicit
type qualifications.

   A data-term is either a variable, a data-functor, or a special
data-term.  A special data-term is a conditional expression, a record
syntax expression, a lambda expression, a higher-order function
application, or an explicit type qualification.

* Menu:

* Data-functors::
* Record syntax::
* Unification expressions::
* Conditional expressions::
* Lambda expressions::
* Higher-order function applications::
* Explicit type qualification::


File: mercury_ref.info,  Node: Data-functors,  Next: Record syntax,  Up: Data-terms

2.13.1 Data-functors
--------------------

A data-functor is an integer, a float, a string, a character literal
(any single-character name), a name, an implementation-defined literal,
or a compound data-term.  A compound data-term is a compound term which
does not match the form of a special data-term (*note Data-terms::),
and whose arguments are data-terms.  If a data-functor is a name or a
compound data-term, its top-level functor must name a function,
predicate, or data constructor declared in the program or in the
interface of an imported module.

   Implementation-defined literals are symbolic names whose value
represents a property of the compilation environment or the context in
which it appears. The implementation replaces these symbolic names with
actual constants during compilation.  Implementation-defined literals
can only appear within clauses. The following literals must be
supported by all Mercury implementations:

`$file'
     a string that gives the name of the file that contains the module
     being compiled. If the name of the file cannot be determined then
     it is replaced by an arbitrary string.

`$line'
     the line number (integer) of the goal in which the literal appears
     or -1 if it cannot be determined.

`$module'
     a string representation of the fully-qualified module name.

`$pred'
     a string containing the fully-qualified predicate or function name
     and arity.


   The Mercury Melbourne implementation additionally supports the
following extension:

`$grade'
     the grade (string) in which the module is compiled.



File: mercury_ref.info,  Node: Record syntax,  Next: Unification expressions,  Prev: Data-functors,  Up: Data-terms

2.13.2 Record syntax
--------------------

Record syntax provides a convenient way to select or update fields of
data constructors, independent of the definition of the constructor.
Record syntax expressions are transformed into sequences of calls to
field selection or update functions (*note Field access functions::).

   A field specifier is a name or a compound data-term.  A field list
is a list of field specifiers separated by `^'.  `field', `field1 ^
field2' and `field1(A) ^ field2(B, C)' are all valid field lists.

   If the top-level functor of a field specifier is `FIELD/N', there
must be a visible selection function `FIELD/(N + 1)'. If the field
specifier occurs in a field update expression, there must also be a
visible update function named `'FIELD :='/(N + 2)'.

   Record syntax expressions have one of the following forms.  There
are also record syntax DCG goals (*note DCG-goals::), which provide
similar functionality to record syntax expressions, except that they
act on the DCG arguments of a DCG clause.

`TERM ^ FIELD_LIST'
     A field selection. For each field specifier in FIELD_LIST, apply
     the corresponding selection function in turn.

     TERM must be a valid data-term.  FIELD_LIST must be a valid field
     list.

     A field selection is transformed using the following rules:
          transform(Term ^ Field(Arg1, ...)) = Field(Arg1, ..., Term).
          transform(Term ^ Field(Arg1, ...) ^ Rest) =
                          transform(Field(Arg1, ..., Term) ^ Rest).

     Examples:

     `Term ^ field' is equivalent to `field(Term)'.

     `Term ^ field(Arg)' is equivalent to `field(Arg, Term)'.

     `Term ^ field1(Arg1) ^ field2(Arg2, Arg3)' is equivalent to
     `field2(Arg2, Arg3, field1(Arg1, Term))'.

`TERM ^ FIELD_LIST := FIELDVALUE'
     A field update, returning a copy of TERM with the value of the
     field specified by FIELD_LIST replaced with FIELDVALUE.

     TERM must be a valid data-term.  FIELD_LIST must be a valid field
     list.

     A field update is transformed using the following rules:
          transform(Term ^ Field(Arg1, ...) := FieldValue) =
                          'Field :='(Arg1, ..., Term, FieldValue)).

          transform(Term0 ^ Field(Arg1, ...) ^ Rest := FieldValue) = Term :-
                  OldFieldValue = Field(Arg1, ..., Term0),
                  NewFieldValue = transform(OldFieldValue ^ Rest := FieldValue),
                  Term = 'Field :='(Arg1, ..., Term0, NewFieldValue).

     Examples:

     `Term ^ field := FieldValue' is equivalent to
     `'field :='(Term, FieldValue)'.

     `Term ^ field(Arg) := FieldValue' is equivalent to
     `'field :='(Arg, Term, FieldValue)'.

     `Term ^ field1(Arg1) ^ field2(Arg2) := FieldValue' is equivalent
     to the code
          OldField1 = field1(Arg1, Term),
          NewField1 = 'field2 :='(Arg2, OldField1, FieldValue),
          Result = 'field1 :='(Arg1, Term, NewField1)



File: mercury_ref.info,  Node: Unification expressions,  Next: Conditional expressions,  Prev: Record syntax,  Up: Data-terms

2.13.3 Unification expressions
------------------------------

A unification expression is an expression of the form

     X @ Y

where X and Y are data-terms.

   The meaning of a unification expression is that the arguments are
unified, and the expression is equivalent to the unified value.

   The strict sequential operational semantics (*note Semantics::) of an
expression `X @ Y' is that the expression is replaced by a fresh
variable Z, and immediately after Z is evaluated, the conjunction
`Z = X, Z = Y' is evaluated.

   For example

     p(X @ f(_, _), X).

is equivalent to

     p(H1, H2) :-
             H1 = X,
             H1 = f(_, _),
             H2 = X.

   Unification expressions are most useful when writing switches (*note
Determinism checking and inference::).  The arguments of a unification
expression are examined when checking for switches.  The arguments of
an equivalent user-defined function would not be.


File: mercury_ref.info,  Node: Conditional expressions,  Next: Lambda expressions,  Prev: Unification expressions,  Up: Data-terms

2.13.4 Conditional expressions
------------------------------

A conditional expression is an expression of either of the two following
forms

     (if GOAL then EXPRESSION1 else EXPRESSION2)
     (GOAL -> EXPRESSION1 ; EXPRESSION2)

GOAL is a goal; EXPRESSION1 and EXPRESSION2 are both data-terms. The
semantics of a conditional expression is that if GOAL is true, then the
expression has the meaning of EXPRESSION1, else the expression has the
meaning of EXPRESSION2.

   If GOAL takes the form `some [X, Y, Z] ...' then the scope of X, Y,
and Z includes EXPRESSION1.


File: mercury_ref.info,  Node: Lambda expressions,  Next: Higher-order function applications,  Prev: Conditional expressions,  Up: Data-terms

2.13.5 Lambda expressions
-------------------------

A lambda expression is a compound term of one of the following forms

     pred(Arg1::Mode1, Arg2::Mode2, ...) is Det :- Goal
     pred(Arg1::Mode1, Arg2::Mode2, ..., DCGMode0, DCGMode1) is Det --> DCGGoal
     func(Arg1::Mode1, Arg2::Mode2, ...) = (Result::Mode) is Det :- Goal
     func(Arg1, Arg2, ...) = (Result) is Det :- Goal
     func(Arg1, Arg2, ...) = Result :- Goal

where Arg1, Arg2, ... are zero or more data-terms, Result is a
data-term, Mode1, Mode2, ... are zero or more modes (*note Modes::),
DCGMode0 and DCGMode1 are modes (*note Modes::), Det is a determinism
(*note Determinism::), Goal is a goal (*note Goals::), and DCGGoal is a
DCG Goal (*note DCG-goals::).  The `:- Goal' part is optional; if it is
not specified, then `:- true' is assumed.  A lambda expression denotes
a higher-order predicate or function term whose value is the predicate
or function of the specified arguments determined by the specified
goal.  *Note Higher-order::.

   A lambda expression introduces a new scope: any variables occurring
in the arguments Arg1, Arg2, ... are locally quantified, i.e.  any
occurrences of variables with that name in the lambda expression are
considered to name a different variable than any variables with the
same name that occur outside of the lambda expression.  For variables
which occur in Result or Goal, but not in the arguments, the usual
Mercury rules for implicit quantification apply (*note Implicit
quantification::).

   The form of lambda expression using `-->' as its top level functor
is a syntactic abbreviation: an expression of the form

     pred(Var1::Mode1, Var2::Mode2, ..., DCGMode0, DCGMode1) is Det --> DCGGoal

is equivalent to

     pred(Var1::Mode1, Var2::Mode2, ...,
         DCGVar0::DCGMode0, DCGVar1::DCGMode1) is Det :- Goal

where DCGVar0 and DCGVar1 are fresh variables, and Goal is the result
of `DCG-transform(DCGVar0, DCGVar1, DCGGoal)' where DCG-transform is
the function specified in *note DCG-goals::.


File: mercury_ref.info,  Node: Higher-order function applications,  Next: Explicit type qualification,  Prev: Lambda expressions,  Up: Data-terms

2.13.6 Higher-order function applications
-----------------------------------------

A higher-order function application is a compound term of one of the
following two forms

     apply(FUNC, ARG1, ARG2, ..., ARGN)
     FUNCVAR(ARG1, ARG2, ..., ARGN)

where N >= 0, FUNC is a term of type `func(T1, T2, ..., Tn) = T',
FUNCVAR is a variable of that type, and ARG1, ARG2, ..., ARGN are terms
of types `T1', `T2', ..., `Tn'.  The type of the higher-order function
application term is T.  It denotes the result of applying the specified
function to the specified arguments.  *Note Higher-order::.


File: mercury_ref.info,  Node: Explicit type qualification,  Prev: Higher-order function applications,  Up: Data-terms

2.13.7 Explicit type qualification
----------------------------------

Explicit type qualifications are occasionally useful to resolve
ambiguities that can arise from overloading or polymorphic types.

   An explicit type qualification expression is a term of the form

     TERM : TYPE

TERM must be a valid data-term.  TYPE must be a valid type (*note
Types::).

   An explicit type qualification expression constrains the specified
term to have the specified type.  Apart from that, the meaning of an
explicit type qualification expression is just the same as the
specified TERM.

   Currently we also support the following alternative syntax for type
qualification:

     with_type(TERM, TYPE)

or equivalently, as it is more commonly written,

     TERM `with_type` TYPE


File: mercury_ref.info,  Node: Variable scoping,  Next: Implicit quantification,  Prev: Data-terms,  Up: Syntax

2.14 Variable scoping
=====================

There are three sorts of variables in Mercury: ordinary variables, type
variables, and inst variables.

   Variables occurring in types are called type variables.  Variables
occurring in insts or modes are called inst variables.  Variables that
occur in data-terms, and that are not inst variables or type variables,
are called ordinary variables.

   (Type variables can occur in data-terms in the right-hand [TYPE]
operand of an explicit type qualification.  Inst variables can occur in
data-terms in the right-hand [MODE] operand of an explicit mode
qualification.  Apart from that, all other variables in data-terms are
ordinary variables.)

   The three different variable sorts occupy different namespaces:
there is no semantic relationship between two variables of different
sorts (e.g. a type variable and an ordinary variable) even if they
happen to share the same name.  (However, as a matter of programming
style, it is generally a bad idea to use the same name for variables of
different sorts in the same clause.)

   The scope of ordinary variables is the clause or declaration in which
they occur, unless they are quantified, either explicitly (*note
Goals::) or implicitly (*note Implicit quantification::).

   The scope of type variables in a predicate or function's type
declaration extends over any explicit type qualifications (*note
Explicit type qualification::) in the clauses for that predicate or
function, and over `pragma type_spec' (*note Type specialization::)
declarations for that predicate or function, so that explicit type
qualifications and `pragma type_spec' declarations can refer to those
type variables. The scope of any type variables in an explicit type
qualification which do not occur in the predicate or function's type
declaration is the clause in which they occur.

   The scope of inst variables is the clause or declaration in which
they occur.


File: mercury_ref.info,  Node: Implicit quantification,  Next: Elimination of double negation,  Prev: Variable scoping,  Up: Syntax

2.15 Implicit quantification
============================

The rule for implicit quantification in Mercury is not the same as the
usual one in mathematical logic.  In Mercury, variables that do not
occur in the head of a clause are implicitly existentially quantified
around their closest enclosing scope (in a sense to be made precise in
the following paragraphs).  This allows most existential quantifiers to
be omitted, and leads to more concise code.

   An occurrence of a variable is "in a negated context" if it is in a
negation, in a universal quantification, in the condition of an
if-then-else, in an inequality, or in a lambda expression.

   Two goals are "parallel" if they are different disjuncts of the same
disjunction, or if one is the "else" part of an if-then-else and the
other goal is either the "then" part or the condition of the
if-then-else, or if they are the goals of disjoint (distinct and
non-overlapping) lambda expressions.

   If a variable occurs in a negated context and does not occur outside
of that negated context other than in parallel goals (and in the case
of a variable in the condition of an if-then-else, other than in the
"then" part of the if-then-else), then that variable is implicitly
existentially quantified inside the negation.


File: mercury_ref.info,  Node: Elimination of double negation,  Prev: Implicit quantification,  Up: Syntax

2.16 Elimination of double negation
===================================

The treatment of inequality, universal quantification, implication, and
logical equivalence as abbreviations can cause the introduction of
double negations which could make otherwise well-formed code
mode-incorrect.  To avoid this problem, the language specifies that
after syntax analysis and implicit quantification, and before mode
analysis is performed, the implementation must delete any double
negations and must replace any negations of conjunctions of negations
with disjunctions.  (Both of these transformations preserve the logical
meaning and type-correctness of the code, and they preserve or improve
mode-correctness: they never transform code fragments that would be
well-moded into ones that would be ill-moded.)


File: mercury_ref.info,  Node: Types,  Next: Modes,  Prev: Syntax,  Up: Top

3 Types
*******

The type system is based on many-sorted logic, and supports
polymorphism, type classes (*note Type classes::), and existentially
quantified types (*note Existential types::).

* Menu:

* Builtin types::
* User-defined types::
* Predicate and function type declarations::
* Field access functions::


File: mercury_ref.info,  Node: Builtin types,  Next: User-defined types,  Up: Types

3.1 Builtin types
=================

Certain special types are builtin, or are defined in the Mercury
library:

Primitive types: `char', `int', `float', `string'.
     There is a special syntax for constants of type `int', `float',
     and `string'.  (For `char', the standard syntax suffices.)

Predicate types: `pred', `pred(T)', `pred(T1, T2)', ...
Function types: `(func) = T', `func(T1) = T',
`func(T1, T2) = T', ...
     These higher-order function and predicate types are used to pass
     procedure addresses and closures to other predicates.  *Note
     Higher-order::.

Tuple types: `{}', `{T}', `{T1, T2}', ....
     A tuple type is equivalent to a discriminated union type (*note
     Discriminated unions::) with declaration
          :- type {Arg1, Arg2, ..., ArgN}
                  ---> { {Arg1, Arg2, ..., ArgN} }.

The universal type: `univ'.
     The type `univ' is defined in the standard library module `univ',
     along with the predicates `type_to_univ/2' and `univ_to_type/2'.
     With those predicates, any type can be converted to the universal
     type and back again.  The universal type is useful for situations
     where you need heterogeneous collections.

The "state-of-the-world" type: `io.state'.
     The type `io.state' is defined in the standard library module `io',
     and represents the state of the world.  Predicates which perform
     I/O are passed the old state of the world and produce a new state
     of the world.  In this way, we can give a declarative semantics to
     code that performs I/O.



File: mercury_ref.info,  Node: User-defined types,  Next: Predicate and function type declarations,  Prev: Builtin types,  Up: Types

3.2 User-defined types
======================

New types can be introduced with `:- type' declarations.  There are
several categories of derived types:

* Menu:

* Discriminated unions::
* Equivalence types::
* Abstract types::


File: mercury_ref.info,  Node: Discriminated unions,  Next: Equivalence types,  Up: User-defined types

3.2.1 Discriminated unions
--------------------------

These encompass both enumeration and record types in other languages.
A derived type is defined using `:- type TYPE ---> BODY'.  (Note there
are _three_ dashes in that arrow.  It should not be confused with the
two-dash arrow used for DCGs or the one-dash arrow used for
if-then-else.)  If the TYPE term is a functor of arity zero (i.e. one
having zero arguments), it names a monomorphic type.  Otherwise, it
names a polymorphic type; the arguments of the functor must be distinct
type variables.  The BODY term is defined as a sequence of constructor
definitions separated by semi-colons.

   Ordinarily, each constructor definition must be a functor whose
arguments (if any) are types.  Ordinary discriminated union definitions
must be "transparent": all type variables occurring in the BODY must
also occur in the TYPE.

   However, constructor definitions can optionally be existentially
typed.  In that case, the functor will be preceded by an existential
type quantifier and can optionally be followed by an existential type
class constraint.  For details, see *note Existential types::.
Existentially typed discriminated union definitions need not be
transparent.

   The arguments of constructor definitions may be labelled.  These
labels cause the compiler to generate functions which can be used to
conveniently select and update fields of a term in a manner independent
of the definition of the type (*note Field access functions::). A
labelled argument has the form `FIELDNAME :: TYPE'. It is an error for
two fields in the same module to have the same label.

   Here are some examples of discriminated union definitions:

     :- type fruit
             --->    apple
             ;       orange
             ;       banana
             ;       pear.

     :- type strange
             --->    foo(int)
             ;       bar(string).

     :- type employee
             --->    employee(
                            name        :: string,
                            age         :: int,
                            department  :: string
                     ).

     :- type tree
             --->    empty
             ;       leaf(int)
             ;       branch(tree, tree).

     :- type list(T)
             --->    []
             ;       [T | list(T)].

     :- type pair(T1, T2)
             --->    T1 - T2.

   If the body of a discriminated union type definition contains a term
whose top-level functor is `';'/2', the semi-colon is normally assumed
to be a separator.  This makes it difficult to define a type whose
constructors include `';'/2'.  To allow this, curly braces can be used
to quote the semi-colon.  It is then also necessary to quote curly
braces.  The following example illustrates this:

     :- type tricky
             --->    { int ; int }
             ;       { { int } }.

   This defines a type with two constructors, `';'/2' and `'{}'/1',
whose argument types are all `int'. We recommend against using
constructors named `'{}'' because of the possibility of confusion with
the builtin tuple types.

   Each discriminated union type definition introduces a distinct type.
Mercury considers two discriminated union types that have the same
bodies to be distinct types (name equivalence).  Having two different
definitions of a type with the same name and arity in the same module
is an error.

   Constructors may be overloaded among different types: there may be
any number of constructors with a given name and arity, so long as they
all have different types.  However, there must not be more than one
constructor with the same name, arity, and result type in the same
module.  (There is no particularly good reason for this restriction; in
the future we may allow several such functors as long as they have
different argument types.)  Note that excessive overloading of
constructors can slow down type checking and can make the program
confusing for human readers, so overloading should not be over-used.


File: mercury_ref.info,  Node: Equivalence types,  Next: Abstract types,  Prev: Discriminated unions,  Up: User-defined types

3.2.2 Equivalence types
-----------------------

These are type abbreviations.  They are defined using `==' as follows.
They may be polymorphic.

     :- type money == int.
     :- type assoc_list(KeyType, ValueType)
             == list(pair(KeyType, ValueType)).

   Equivalence type definitions must be transparent.  Unlike
discriminated union type definitions, equivalence type definitions must
not be cyclic; that is, the type on the left hand side of the `=='
(`assoc_list' and `money' in the examples above) must not occur on the
right hand side of the `=='.

   Mercury treats an equivalence type as an abbreviation for the type
on the right hand side of the definition; the two are equivalent in all
respects in scopes where the equivalence type is visible.


File: mercury_ref.info,  Node: Abstract types,  Prev: Equivalence types,  Up: User-defined types

3.2.3 Abstract types
--------------------

These are types whose implementation is hidden.  The type declarations

     :- type t1.
     :- type t2(T1, T2).

declare types `t1/0' and `t2/2' to be abstract types.  Such
declarations are only useful in the interface section of a module.
This means that the type names will be exported, but the constructors
(functors) for these types will not be exported.  The implementation
section of a module must give a definition for all of the abstract types
named in the interface section of the module.  Abstract types may be
defined as either discriminated union types or as equivalence types.


File: mercury_ref.info,  Node: Predicate and function type declarations,  Next: Field access functions,  Prev: User-defined types,  Up: Types

3.3 Predicate and function type declarations
============================================

The argument types of each predicate must be explicitly declared with a
`:- pred' declaration.  The argument types and return type of each
function must be explicitly declared with a `:- func' declaration.  For
example:

     :- pred is_all_uppercase(string).

     :- func strlen(string) = int.

   Predicates and functions can be polymorphic; that is, their
declarations can include type variables.  For example:

     :- pred member(T, list(T)).

     :- func length(list(T)) = int.

   A predicate or function can by declared to have a given higher-order
type (*note Higher-order::) by using ``with_type`' in the type
declaration.  This is useful where several predicates or functions need
to have the same type signature, which often occurs for typeclass
method implementations (*note Type classes::), and for predicates to be
passed as higher-order terms.

   For example,

     :- type foldl_pred(T, U) == pred(T, U, U).
     :- type foldl_func(T, U) == (func(T, U) = U).

     :- pred p(int) `with_type` foldl_pred(T, U).
     :- func f(int) `with_type` foldl_func(T, U).

is equivalent to

     :- pred p(int, T, U, U).
     :- pred f(int, T, U) = U.

   Type variables in predicate and function declarations are implicitly
universally quantified by default; that is, the predicate or function
may be called with arguments and (in the case of functions) return value
whose actual types are any instance of the types specified in the
declaration.  For example, the function `length/1' declared above could
be called with the argument having type `list(int)', or `list(float)',
or `list(list(int))', etc.

   Type variables in predicate and function declarations can also be
existentially quantified; this is discussed in *note Existential
types::.

   There must only be one predicate with a given name and arity in each
module, and only one function with a given name and arity in each
module.  It is an error to declare the same predicate or function twice.

   There must be at least one clause defined for each declared
predicate or function, except for those defined using the foreign
language interface (*note Foreign language interface::).  However,
Mercury implementations are permitted to provide a method of processing
Mercury programs in which such errors are not reported until and unless
the predicate or function is actually called.  (The University of
Melbourne Mercury implementation provides this with its `--allow-stubs'
option.  This can be useful during program development, since it allows
you to execute parts of a program while the program's implementation is
still incomplete.)

   Note that a predicate defined using DCG notation (*note DCG-rules::)
will appear to be defined with two fewer arguments than it is declared
with.  It will also appear to be called with two fewer arguments when
called from predicates defined using DCG notation.  However, when called
from an ordinary predicate or function, it must have all the arguments
it was declared with.

   The compiler infers the types of data-terms, and in particular the
types of variables and overloaded constructors, functions, and
predicates.  A "type assignment" is an assignment of a type to every
variable and of a particular constructor, function, or predicate to
every name in a clause.  A type assignment is "valid" if it satisfies
the following conditions.

   Each constructor in a clause must have been declared in at least one
visible type declaration.  The type assigned to each constructor term
must match one of the type declarations for that constructor, and the
types assigned to the arguments of that constructor must match the
argument types specified in that type declaration.

   The type assigned to each function call term must match the return
type of one of the `:- func' declarations for that function, and the
types assigned to the arguments of that function must match the
argument types specified in that type declaration.

   The type assigned to each predicate argument must match the type
specified in one of the `:- pred' declarations for that predicate.  The
type assigned to each head argument in a predicate clause must exactly
match the argument type specified in the corresponding `:- pred'
declaration.

   The type assigned to each head argument in a function clause must
exactly match the argument type specified in the corresponding `:-
func' declaration, and the type assigned to the result term in a
function clause must exactly match the result type specified in the
corresponding `:- func' declaration.

   The type assigned to each data-term with an explicit type
qualification (*note Explicit type qualification::) must match the type
specified by the type qualification expression(1).

   (Here "match" means to be an instance of, i.e. to be identical to
for some substitution of the type parameters, and "exactly match" means
to be identical up to renaming of type parameters.)

   One type assignment A is said to be "more general" than another type
assignment B if there is a binding of the type parameters in A that
makes it identical (up to renaming of parameters) to B.  If there is
more than one valid type assignment, the compiler must choose the most
general one.  If there are two valid type assignments which are not
identical up to renaming and neither of which is more general than the
other, then there is a type ambiguity, and compiler must report an
error.  A clause is "type-correct" if there is a unique (up to
renaming) most general valid type assignment.  Every clause in a
Mercury program must be type-correct.

   ---------- Footnotes ----------

   (1) The type of an explicitly type qualified term may be an instance
of the type specified by the qualifier. This allows explicit type
qualifications to constrain the types of two data-terms to be
identical, without knowing the exact types of the data-terms. It also
allows type qualifications to refer to the types of the results of
existentially typed predicates or functions.


File: mercury_ref.info,  Node: Field access functions,  Prev: Predicate and function type declarations,  Up: Types

3.4 Field access functions
==========================

Fields of constructors of discriminated union types may be labelled
(*note Discriminated unions::). These labels cause the compiler to
generate functions which can be used to select and update fields of a
term in a manner independent of the definition of the type.

   The Mercury language includes syntactic sugar to make it more
convenient to select and update fields inside nested terms (*note
Record syntax::) and to select and update fields of the DCG arguments
of a clause (*note DCG-goals::).

* Menu:

* Field selection::
* Field update::
* User-supplied field access function declarations::
* Field access examples::


File: mercury_ref.info,  Node: Field selection,  Next: Field update,  Up: Field access functions

3.4.1 Field selection
---------------------

     FIELD(TERM)

   Each field label `FIELD' in a constructor causes generation of a
field selection function `FIELD/1', which takes a data-term of the same
type as the constructor and returns the value of the labelled field,
failing if the top-level constructor of the argument is not the
constructor containing the field.

   If the declaration of the field is in the interface section of the
module, the corresponding field selection function is also exported
from the module.

   By default, this function has no declared modes -- the modes are
inferred at each call to the function. However, the type and modes of
this function may be explicitly declared, in which case it will have
only the declared modes.

   To create a higher-order term from a field selection function, an
explicit lambda expression must be used, unless a single mode
declaration is supplied for the field selection function.


File: mercury_ref.info,  Node: Field update,  Next: User-supplied field access function declarations,  Prev: Field selection,  Up: Field access functions

3.4.2 Field update
------------------

     'FIELD :='(TERM, VALUETERM)

   Each field label `FIELD' in a constructor causes generation of a
field update function `'FIELD :='/2'.  The first argument of this
function is a data-term of the same type as the constructor. The second
argument is a data-term of the same type as the labelled field. The
return value is a copy of the first argument with value of the labelled
field replaced by the second argument.  `'FIELD :='/2' fails if the
top-level constructor of the first argument is not the constructor
containing the labelled field.

   If the declaration of the field is in the interface section of the
module, the corresponding field update function is also exported from
the module.

   By default, this function has no declared modes -- the modes are
inferred at each call to the function. However, the type and modes of
this function may be explicitly declared, in which case it will have
only the declared modes.

   To create a higher-order term from a field update function, an
explicit lambda expression must be used, unless a single mode
declaration is supplied for the field update function.

   Some fields cannot be updated using field update functions.  For the
constructor `unsettable/2' below, neither field may be updated because
the resulting term would not be well-typed. A future release may allow
multiple fields to be updated by a single expression to avoid this
problem.

     :- type unsettable
             ---> some [T] unsettable(
                     unsettable1 :: T,
                     unsettable2 :: T
             ).


File: mercury_ref.info,  Node: User-supplied field access function declarations,  Next: Field access examples,  Prev: Field update,  Up: Field access functions

3.4.3 User-supplied field access function declarations
------------------------------------------------------

Type and mode declarations for compiler-generated field access functions
for fields of constructors local to a module may be placed in the
interface section of the module. This allows the implementation of a
type to be hidden while still allowing client modules to use record
syntax to manipulate values of the type. Supplying a type declaration
and a single mode declaration also allows higher-order terms to be
created from a field access function without using explicit lambda
expressions.

   Declarations for field access functions for fields occurring in the
interface section of a module must also occur in the interface section.

   Declarations and clauses for field access functions can also be
supplied for fields which are not a part of any type. This is useful
when the data structures of a program change so that a value which was
previously stored as part of a type is now computed each time it is
requested. It also allows record syntax to be used for type class
methods.

   User-declared field access functions may take extra arguments.  For
example, the Mercury standard library module `map' contains the
following functions:
     :- func elem(K, map(K, V)) = V is semidet.
     :- func 'elem :='(K, map(K, V), V) = map(K, V).
   Field access syntax may be used at the top-level of `func' and
`mode' declarations and in the head of clauses.  For instance:
     :- func map(K, V) ^ elem(K) = V.
     :- mode in        ^ in      = out is semidet.
     Map ^ elem(Key) = map.lookup(Map, Key).

     :- func (map(K, V) ^ elem(K) := V)  = V.
     :- mode (in        ^ in      := in) = out is semidet.
     (Map ^ elem(Key) := Value) = map.set(Map, Key, Value).

   The Mercury standard library modules `array' and `bt_array' define
similar functions.


File: mercury_ref.info,  Node: Field access examples,  Prev: User-supplied field access function declarations,  Up: Field access functions

3.4.4 Field access examples
---------------------------

The examples make use of the following type declarations:

     :- type type1
             ---> type1(
                     field1 :: type2,
                     field2 :: string
             ).

     :- type type2
             ---> type2(
                     field3 :: int,
                     field4 :: int
             ).

   The compiler generates some field access functions for `field1'.
The functions generated for the other fields are similar.

     +:- func type1 ^ field1 = type2.
     +type1(Field1, _) ^ field1 = Field1.

     +:- func (type1 ^ field1 := type2) = type1.
     +(type1(_, Field2) ^ field1 := Field1) = type1(Field1, Field2).

   Using these functions and the syntactic sugar described in *note
Record syntax::, programmers can write code such as

     +:- func type1 ^ increment_field3 = type1.

     +Term0 ^ increment_field3 =
             Term0 ^ field1 ^ field3 := Term0 ^ field1 ^ field3 + 1.

   The compiler expands this into

     incremental_field3(Term0) = Term :-
             OldField3 = field3(field1(Term0)),

             OldField1 = field1(Term0),
             NewField1 = 'field3 :='(OldField1, OldField3 + 1),
             Term = 'field1 :='(Term0, NewField1).

   The field access functions defined in the Mercury standard library
module `map' can be used as follows:

     :- func update_field_in_map(map(int, type1), int, string)
                     = map(int, type1) is semidet.

     update_field_in_map(Map, Index, Value) =
                     Map ^ elem(Index) ^ field2 := Value.


File: mercury_ref.info,  Node: Modes,  Next: Unique modes,  Prev: Types,  Up: Top

4 Modes
*******

* Menu:

* Insts modes and mode definitions::
* Predicate and function mode declarations::
* Constrained polymorphic modes::
* Different clauses for different modes::


File: mercury_ref.info,  Node: Insts modes and mode definitions,  Next: Predicate and function mode declarations,  Up: Modes

4.1 Insts, modes, and mode definitions
======================================

The "mode" of a predicate, or function, is a mapping from the initial
state of instantiation of the arguments of the predicate, or the
arguments and result of a function, to their final state of
instantiation.  To describe states of instantiation, we use information
provided by the type system.  Types can be viewed as regular trees with
two kinds of nodes: or-nodes representing types and and-nodes
representing constructors.  The children of an or-node are the
constructors that can be used to construct terms of that type; the
children of an and-node are the types of the arguments of the
constructors.  We attach mode information to the or-nodes of type trees.

   An "instantiatedness tree" is an assignment of an "instantiatedness"
-- either "free" or "bound" -- to each or-node of a type tree, with the
constraint that all descendants of a free node must be free.

   A term is "approximated by" an instantiatedness tree if for every
node in the instantiatedness tree,

   * if the node is "free", then the corresponding node in the term (if
     any) is a free variable that does not share with any other variable
     (we call such variables "distinct");

   * if the node is "bound", then the corresponding node in the term
     (if any) is a function symbol.


   When an instantiatedness tree tells us that a variable is bound,
there may be several alternative function symbols to which it could be
bound.  The instantiatedness tree does not tell us which of these it is
bound to; instead for each possible function symbol it tells us exactly
which arguments of the function symbol will be free and which will be
bound.  The same principle applies recursively to these bound arguments.

   Mercury's mode system allows users to declare names for
instantiatedness trees using declarations such as

     :- inst listskel == bound( [] ; [free | listskel] ).

   This instantiatedness tree describes lists whose skeleton is known
but whose elements are distinct variables.  As such, it approximates
the term `[A,B]' but not the term `[H|T]' (only part of the skeleton is
known), the term `[A,2]' (not all elements are variables), or the term
`[A,A]' (the elements are not distinct variables).

   As a shorthand, the mode system provides `free' and `ground' as
names for instantiatedness trees all of whose nodes are free and bound
respectively (with the exception of solver type values which may be
semantically ground, but be defined in terms of non-ground solver type
values; see *note Solver types:: for more detail).  The shape of these
trees is determined by the type of the variable to which they apply.

   A more concise, alternative syntax exists for `bound'
instantiatedness trees:

     :- inst maybeskel ---> no ; yes(ground).

which is equivalent to writing

     :- inst maybeskel == bound(no ; yes(ground)).

   As execution proceeds, variables may become more instantiated.  A
"mode mapping" is a mapping from an initial instantiatedness tree to a
final instantiatedness tree, with the constraint that no node of the
type tree is transformed from bound to free.  Mercury allows the user
to specify mode mappings directly by expressions such as `inst1 >>
inst2', or to give them a name using declarations such as

     :- mode m == inst1 >> inst2.

   Two standard shorthand modes are provided, corresponding to the
standard notions of inputs and outputs:

     :- mode in == ground >> ground.
     :- mode out == free >> ground.

   Prolog fans who want to use the symbols `+' and `-' can do so by
simply defining them using a mode declaration:

     :- mode (+) == in.
     :- mode (-) == out.

   These two modes are enough for most functions and predicates.
Nevertheless, Mercury's mode system is sufficiently expressive to
handle more complex data-flow patterns, including those involving
partially instantiated data structures.  (The current implementation
does not handle partially instantiated data structures yet.)

   For example, consider an interface to a database that associates
data with keys, and provides read and write access to the items it
stores.  To represent accesses to the database over a network, you
would need declarations such as

     :- type operation
             --->    lookup(key, data)
             ;       set(key, data).
     :- inst request
     	--->	lookup(ground, free)
             ;       set(ground, ground).
     :- mode create_request == free >> request.
     :- mode satisfy_request == request >> ground.

   `inst' and `mode' declarations can be parametric.  For example, the
following declaration

     :- inst listskel(Inst) ---> [] ; [Inst | listskel(Inst)].

defines the inst `listskel(Inst)' to be a list skeleton whose elements
have inst `Inst'; you can then use insts such as
`listskel(listskel(free))', which represents the instantiation state of
a list of lists of free variables.  The standard library provides the
parametric modes

     :- mode in(Inst) == Inst >> Inst.
     :- mode out(Inst) == free >> Inst.

so that for example the mode `create_request' defined above could have
be defined as

     :- mode create_request == out(request).

   There must not be more than one inst definition with the same name
and arity in the same module.  Similarly, there must not be more than
one mode definition with the same name and arity in the same module.


File: mercury_ref.info,  Node: Predicate and function mode declarations,  Next: Constrained polymorphic modes,  Prev: Insts modes and mode definitions,  Up: Modes

4.2 Predicate and function mode declarations
============================================

A "predicate mode declaration" assigns a mode mapping to each argument
of a predicate.  A "function mode declaration" assigns a mode mapping
to each argument of a function, and a mode mapping to the function
result.  Each mode of a predicate or function is called a "procedure".
For example, given the mode names defined by

     :- mode out_listskel ==
             free >> listskel.
     :- mode in_listskel ==
             listskel >> listskel.

the (type and) mode declarations of the function length and predicate
append are as follows:

     :- func length(list(T)) = int.
     :- mode length(in_listskel) = out.
     :- mode length(out_listskel) = in.

     :- pred append(list(T), list(T), list(T)).
     :- mode append(in, in, out).
     :- mode append(out, out, in).

   Note that functions may have more than one mode, just like
predicates; functions can be reversible.

   Alternately, the mode declarations for `length' could use the
standard library modes `in/1' and `out/1':

     :- func length(list(T)) = int.
     :- mode length(in(listskel)) = out.
     :- mode length(out(listskel)) = in.

   As for type declarations, a predicate or function can be defined to
have a given higher-order inst (*note Higher-order modes::) by using
``with_inst`' in the mode declaration.

   For example,

     :- inst foldl_pred == (pred(in, in, out) is det).
     :- inst foldl_func == (func(in, in) = out is det).

     :- mode p(in) `with_inst` foldl_pred.
     :- mode f(in) `with_inst` foldl_func.

is equivalent to

     :- mode p(in, in, in, out) is det.
     :- mode f(in, in, in) = out is det.

(`is det' is explained in *note Determinism::.)

   If a predicate or function has only one mode, the `pred' and `mode'
declaration can be combined:

     :- func length(list(T)::in) = (int::out).
     :- pred append(list(T)::in, list(T)::in, list(T)::out).

     :- pred p `with_type` foldl_pred(T, U) `with_inst` foldl_pred.

   If there is no mode declaration for a function, the compiler assumes
a default mode for the function in which all the arguments have mode
`in' and the result of the function has mode `out'.  (However, there is
no requirement that a function have such a mode; if there is any
explicit mode declaration, it overrides the default.)

   A function or predicate mode declaration is an assertion by the
programmer that for all possible argument terms and (if applicable)
result term for the function or predicate that are approximated (in our
technical sense) by the initial instantiatedness trees of the mode
declaration and all of whose free variables are distinct, if the
function or predicate succeeds then the resulting binding of those
argument terms and (if applicable) result term will in turn be
approximated by the final instantiatedness trees of the mode
declaration, with all free variables again being distinct.  We refer to
such assertions as "mode declaration constraints".  These assertions
are checked by the compiler, which rejects programs if it cannot prove
that their mode declaration constraints are satisfied.

   Note that with the usual definition of append, the mode

     :- mode append(in_listskel, in_listskel, out_listskel).

would not be allowed, since it would create aliasing between the
different arguments -- on success of the predicate, the list elements
would be free variables but they would not be distinct.

   In Mercury it is always possible to call a procedure with an
argument that is more bound than the initial inst specified for that
argument in the procedure's mode declaration.  In such cases, the
compiler will insert additional unifications to ensure that the
argument actually passed to the procedure will have the inst specified.
For example, if the predicate `p/1' has mode `p(out)', you can still
call `p(X)' if `X' is ground.  The compiler will transform this code to
`p(Y), X = Y' where `Y' is a fresh variable.  It is almost as if the
predicate `p/1' has another mode `p(in)'; we call such modes "implied
modes".

   To make this concept precise, we introduce the following definition.
A term "satisfies" an instantiatedness tree if for every node in the
instantiatedness tree,

   * if the node is "free", then the corresponding node in the term (if
     any) is either a distinct free variable, or a function symbol.

   * if the node is "bound", then the corresponding node in the term
     (if any) is a function symbol.


   The "mode set" for a predicate or function is the set of mode
declarations for the predicate or function.  A mode set is an assertion
by the programmer that the predicate should only be called with
argument terms that satisfy the initial instantiatedness trees of one
of the mode declarations in the set (i.e. the specified modes and the
modes they imply are the only allowed modes for this predicate or
function).  We refer to the assertion associated with a mode set as the
"mode set constraint"; these are also checked by the compiler.

   A predicate or function P is "well-moded with respect to a given
mode declaration" if given that the predicates and functions called by P
all satisfy their mode declaration constraints, there exists an
ordering of the conjuncts in each conjunction in the clauses of P such
that

   * P satisfies its mode declaration constraint, and

   * P satisfies the mode set constraint of all of the predicates and
     functions it calls

   We say that a predicate or function is well-moded if it is
well-moded with respect to all the mode declarations in its mode set,
and we say that a program is well-moded if all its predicates and
functions are well-moded.

   The mode analysis algorithm checks one procedure at a time.  It
abstractly interprets the definition of the predicate or function,
keeping track of the instantiatedness of each variable, and selecting a
mode for each call and unification in the definition.  To ensure that
the mode set constraints of called predicates and functions are
satisfied, the compiler may reorder the elements of conjunctions; it
reports an error if no satisfactory order exists.  Finally it checks
that the resulting instantiatedness of the procedure's arguments is the
same as the one given by the procedure's declaration.

   The mode analysis algorithm annotates each call with the mode used.


File: mercury_ref.info,  Node: Constrained polymorphic modes,  Next: Different clauses for different modes,  Prev: Predicate and function mode declarations,  Up: Modes

4.3 Constrained polymorphic modes
=================================

Mode declarations for predicates and functions may also have inst
parameters.  However, such parameters must be constrained to be
_compatible_ with some other inst.  In a predicate or function mode
declaration, an inst of the form `INSTPARAM =< INST', where INSTPARAM
is a variable and INST is an inst, states that INSTPARAM is constrained
to be _compatible_ with INST, that is, INSTPARAM represents some inst
that can be used anywhere where INST is required.  If an inst parameter
occurs more than once in a declaration, it must have the same
constraint on each occurrence.

   For example, in the mode declaration
     	:- mode append(in(list_skel(I =< ground)), in(list_skel(I =< ground)),
     	        out(list_skel(I =< ground))) is det.
   `I' is an inst parameter which is constrained to be ground.  If
`append' is called with the first two arguments having an inst of, say,
`list_skel(bound(f))' then after `append' returns, all three arguments
will have inst `list_skel(bound(f))'.  If the mode of append had been
simply
     	:- mode append(in(list_skel(ground)), in(list_skel(ground)),
     	        out(list_skel(ground))) is det.
   then we would only have been able to infer an inst of
`list_skel(ground)' for the third argument, not the more specific inst.

   Note that attempting to call `append' when the first two arguments
do not have ground insts (e.g. `list_skel(bound(g(free)))') is a mode
error because it violates the constraint on the inst parameter.

   To avoid having to repeat a constraint everywhere that an inst
parameter occurs, it is possible to list the constraints after the rest
of the mode declaration, following a `<='.  E.g. the above example
could have been written as
     	:- (mode append(in(list_skel(I)), in(list_skel(I)),
                     out(list_skel(I))) is det) <= I =< ground.

   Note that in the current Mercury implementation this syntax requires
parentheses around the `mode(...) is DET' part of the declaration.

   Also, if the constraint on an inst parameter is `ground' then it is
not necessary to give the constraint in the declaration.  The example
can be further shortened to
     	:- mode append(in(list_skel(I)), in(list_skel(I)), out(list_skel(I)))
                     is det.

   Constrained polymorphic modes are particularly useful when passing
objects with higher-order types to polymorphic predicates since they
allow the higher-order mode information to be retained (*note
Higher-order::).


File: mercury_ref.info,  Node: Different clauses for different modes,  Prev: Constrained polymorphic modes,  Up: Modes

4.4 Different clauses for different modes
=========================================

Because the compiler automatically reorders conjunctions to satisfy the
modes, it is often possible for a single clause to satisfy different
modes.  However, occasionally reordering of conjunctions is not
sufficient; you may want to write different code for different modes.

   For example, the usual code for list append

     	append([], Ys, Ys).
     	append([X|Xs], Ys, [X|Zs]) :- append(Xs, Ys, Zs).

works fine in most modes, but is not very satisfactory for the
`append(out, in, in)' mode of append, because although every call in
this mode only has at most one solution, the compiler's determinism
inference will not be able to infer that.  This means that using the
usual code for append in this mode will be inefficient, and the overly
conservative determinism inference may cause spurious determinism
errors later.

   For this mode, it is better to use a completely different algorithm:

     	append(Prefix, Suffix, List) :-
     		list.length(List, ListLength),
     		list.length(Suffix, SuffixLength),
     		PrefixLength = ListLength - SuffixLength,
     		list.split_list(PrefixLength, List, Prefix, Suffix).

However, that code doesn't work in the other modes of append.

   To handle such cases, you can use mode annotations on clauses, which
indicate that particular clauses should only be used for particular
modes.  To specify that a clause only applies to a given mode, each
argument ARG of the clause head should be annotated with the
corresponding argument mode MODE, using the `::' mode qualification
operator, i.e. `ARG :: MODE'.

   For example, if append was declared as

     	:- pred append(list(T), list(T), list(T)).
     	:- mode append(in, in, out).
     	:- mode append(out, out, in).
     	:- mode append(in, out, in).
     	:- mode append(out, in, in).

then you could implement it as

     	append(L1::in,  L2::in,  L3::out) :- usual_append(L1, L2, L3).
     	append(L1::out, L2::out, L3::in)  :- usual_append(L1, L2, L3).
     	append(L1::in,  L2::out, L3::in)  :- usual_append(L1, L2, L3).
     	append(L1::out, L2::in,  L3::in)  :- other_append(L1, L2, L3).

     	usual_append([], Ys, Ys).
     	usual_append([X|Xs], Ys, [X|Zs]) :- usual_append(Xs, Ys, Zs).

     	other_append(Prefix, Suffix, List) :-
     		list.length(List, ListLength),
     		list.length(Suffix, SuffixLength),
     		PrefixLength = ListLength - SuffixLength,
     		list.split_list(PrefixLength, List, Prefix, Suffix).

   This language feature can be used to write "impure" code that
doesn't have any consistent declarative semantics.  For example, you
can easily use it to write something similar to Prolog's (in)famous
var/1 predicate:

     	:- mode var(in).
     	:- mode var(free>>free).
     	var(_::in) :- fail.
     	var(_::free>>free) :- true.

As you can see, in this case the two clauses are _not_ equivalent.

   Because of this possibility, predicates or functions which are
defined using different code for different modes are by default assumed
to be impure; the programmer must either (1) carefully ensure that the
logical meaning of the clauses is the same for all modes, which can be
declared to the compiler through a `pragma promise_equivalent_clauses'
declaration, or a `pragma promise_pure' declaration, or (2) declare the
predicate or function as impure.  *Note Impurity::.

   In the example with `append' above, the two ways of implementing
append do have the same declarative semantics, so we can safely use the
first approach:

     	:- pragma promise_equivalent_clauses(append/3).

   The pragma

     	:- pragma promise_pure(append/3).

   would also promise that the clauses are equivalent, but on top of
that would also promise that the code of each clause is pure.
Sometimes, if some clauses contain impure code, that is a promise that
the programmer wants to make, but this extra promise is unnecessary in
this case.

   In the example with `var/1' above, the two clauses have different
semantics, so the predicate must be declared as impure:

     	:- impure pred var(T).


File: mercury_ref.info,  Node: Unique modes,  Next: Determinism,  Prev: Modes,  Up: Top

5 Unique modes
**************

Mode declarations can also specify so-called "unique modes".  Mercury's
unique modes are similar to "linear types" in some functional
programming languages such as Clean.  They allow you to specify when
there is only one reference to a particular value, and when there will
be no more references to that value.  If the compiler knows there will
be no more references to a value, it can perform "compile-time garbage
collection" by automatically inserting code to deallocate the storage
associated with that value.  Even more importantly, the compiler can
also simply reuse the storage immediately, for example by destructively
updating one element of an array rather than making a new copy of the
entire array in order to change one element.  Unique modes are also the
mechanism Mercury uses to provide declarative I/O.

   We have not yet implemented unique modes fully, and the details are
still in a state of flux.  So the following should be considered
tentative.

* Menu:

* Destructive update::
* Backtrackable destructive update::
* Limitations of the current implementation::


File: mercury_ref.info,  Node: Destructive update,  Next: Backtrackable destructive update,  Up: Unique modes

5.1 Destructive update
======================

In addition to the insts mentioned above (`free', `ground', and
`bound(...)'), Mercury also provides "unique" insts `unique' and
`unique(...)' which are like `ground' and `bound(...)' respectively,
except that they carry the additional constraint that there can only be
one reference to the corresponding value.  There is also an inst `dead'
which means that there are no references to the corresponding value, so
the compiler is free to generate code that reuses that value.  There
are three standard modes for manipulation unique values:

     % unique output
     :- mode uo == free >> unique.

     % unique input
     :- mode ui == unique >> unique.

     % destructive input
     :- mode di == unique >> dead.

   Mode `uo' is used to create a unique value.  Mode `ui' is used to
inspect a unique value without losing its uniqueness.  Mode `di' is
used to deallocate or reuse the memory occupied by a value that will
not be used.

   Note that a value is not considered `unique' if it might be needed
on backtracking.  This means that unique modes are generally only
useful for code whose determinism is `det' or `cc_multi' (*note
Determinism::).

   Unlike `bound' instantiatedness trees, there is no alternative
syntax for `unique' instantiatedness trees.


File: mercury_ref.info,  Node: Backtrackable destructive update,  Next: Limitations of the current implementation,  Prev: Destructive update,  Up: Unique modes

5.2 Backtrackable destructive update
====================================

     "Well it just so happens that your friend here is only _mostly_
     dead.
     There's a big difference between mostly dead and all dead...
     Now, mostly dead is slightly alive.
     Now, all dead -- well, with all dead, there's usually only one
     thing that you can do."

     "What's that?"

     "Go through his clothes and look for loose change!"

     -- from the movie "The Princess Bride".

   To allow for backtrackable destructive updates -- that is, updates
whose effect is undone on backtracking, perhaps by recording the
overwritten values on a "trail" so that they can be restored after
backtracking -- Mercury also provides "mostly unique" modes.  The insts
`mostly_unique' and `mostly_dead' are equivalent to `unique' and `dead',
except that only references which will be encountered during forward
execution are counted -- it is OK for `mostly_unique' or `mostly_dead'
values to be needed again on backtracking.

   Mercury defines some standard modes for manipulating "mostly unique"
values, just as it does for unique values:

     % mostly unique output
     :- mode muo == free >> mostly_unique.

     % mostly unique input
     :- mode mui == mostly_unique >> mostly_unique.

     % mostly destructive input
     :- mode mdi == mostly_unique >> mostly_dead.


File: mercury_ref.info,  Node: Limitations of the current implementation,  Prev: Backtrackable destructive update,  Up: Unique modes

5.3 Limitations of the current implementation
=============================================

The implementation of the mode analysis algorithm is not quite complete;
as a result, it is not possible to use nested unique modes, i.e.  modes
in which anything but the top level of a variable is unique.  If you
do, you will get unique mode errors when you try to get a unique field
of a unique data structure.  It is also not possible to use
unique-input modes; only destructive-input and unique-output modes work.

   The Mercury compiler does not (yet) reuse `dead' values.  The only
destructive update in the current implementation occurs in library
modules, e.g. for I/O and arrays.  We do however plan to implement
structure reuse and compile-time garbage collection in the very near
future.


File: mercury_ref.info,  Node: Determinism,  Next: User-defined equality and comparison,  Prev: Unique modes,  Up: Top

6 Determinism
*************

* Menu:

* Determinism categories::
* Determinism checking and inference::
* Replacing compile-time checking with run-time checking::
* Interfacing nondeterministic code with the real world::
* Committed choice nondeterminism::


File: mercury_ref.info,  Node: Determinism categories,  Next: Determinism checking and inference,  Up: Determinism

6.1 Determinism categories
==========================

For each mode of a predicate or function, we categorise that mode
according to how many times it can succeed, and whether or not it can
fail before producing its first solution.

   If all possible calls to a particular mode of a predicate or function
which return to the caller (calls which terminate, do not throw an
exception and do not cause a fatal runtime error)

   * have exactly one solution, then that mode is "deterministic"
     (`det');

   * either have no solutions or have one solution, then that mode is
     "semideterministic" (`semidet');

   * have at least one solution but may have more, then that mode is
     "multisolution" (`multi');

   * have zero or more solutions, then that mode is "nondeterministic"
     (`nondet');

   * fail without producing a solution, then that mode has a
     determinism of `failure'.

   If no possible calls to a particular mode of a predicate or function
can return to the caller, then that mode has a determinism of
`erroneous'.

   The determinism annotation `erroneous' is used on the library
predicates `require.error/1' and `exception.throw/1', but apart from
that determinism annotations `erroneous' and `failure' are generally
not needed.

   To summarize:

                     Maximum number of solutions
     Can fail?       0               1               > 1
     no              erroneous       det             multi
     yes             failure         semidet         nondet

   (Note: the "Can fail?" column here indicates only whether the
procedure can fail before producing at least one solution; attempts to
find a _second_ solution to a particular call, e.g. for a procedure
with determinism `multi', are always allowed to fail.)

   The determinism of each mode of a predicate or function is indicated
by an annotation on the mode declaration.  For example:

     :- pred append(list(T), list(T), list(T)).
     :- mode append(in, in, out) is det.
     :- mode append(out, out, in) is multi.
     :- mode append(in, in, in) is semidet.

     :- func length(list(T)) = int.
     :- mode length(in) = out is det.
     :- mode length(in(list_skel)) = out is det.
     :- mode length(in) = in is semidet.

   An annotation of `det' or `multi' is an assertion that for every
value each of the inputs, there exists at least one value of the
outputs for which the predicate is true, or (in the case of functions)
for which the function term is equal to the result term.  Conversely,
an annotation of `det' or `semidet' is an assertion that for every
value each of the inputs, there exists at most one value of the outputs
for which the predicate is true, or (in the case of functions) for
which the function term is equal to the result term.  These assertions
are called the "mode-determinism assertions"; they can play a role in
the semantics, because in certain circumstances they may allow an
implementation to perform optimizations that would not otherwise be
allowed, such as optimizing away a goal with no outputs even though it
might infinitely loop.

   If the mode of the predicate is given in the `:- pred' declaration
rather than in a separate `:- mode' declaration, then the determinism
annotation goes on the `:- pred' declaration (and similarly for
functions).  In particular, this is necessary if a predicate does not
have any argument variables.  If the determinism declaration is given
on a `:- func' declaration without the mode, the function is assumed to
have the default mode (see *note Modes:: for more information on
default modes of functions).

   For example:

     :- pred loop(int::in) is erroneous.
     loop(X) :- loop(X).

     :- pred p is det.
     p.

     :- pred q is failure.
     q :- fail.

   If there is no mode declaration for a function, then the default
mode for that function is considered to have been declared as `det'.
If you want to write a partial function, i.e. one whose determinism is
`semidet', then you must explicitly declare the mode and determinism.

   In Mercury, a function is supposed to be a true mathematical function
of its arguments; that is, the value of the function's result should be
determined only by the values of its arguments.  Hence, for any mode of
a function that specifies that all the arguments are fully input (i.e.
for which the initial inst of all the arguments is a ground inst), the
determinism of that mode can only be `det', `semidet', `erroneous', or
`failure'.

   The determinism categories form this lattice:

                  erroneous
                   /     \
               failure   det
                  \     /   \
                  semidet  multi
                      \     /
                       nondet

   The higher up this lattice a determinism category is, the more the
compiler knows about the number of solutions of procedures of that
determinism.


File: mercury_ref.info,  Node: Determinism checking and inference,  Next: Replacing compile-time checking with run-time checking,  Prev: Determinism categories,  Up: Determinism

6.2 Determinism checking and inference
======================================

The determinism of goals is inferred from the determinism of their
component parts, according to the rules below.  The inferred
determinism of a procedure is just the inferred determinism of the
procedure's body.

   For procedures that are local to a module, the determinism
annotations may be omitted; in that case, their determinism will be
inferred.  (To be precise, the determinism of procedures without a
determinism annotation is defined as the least fixpoint of the
transformation which, given an initial assignment of the determinism
`det' to all such procedures, applies those rules to infer a new
determinism assignment for those procedures.)

   It is an error to omit the determinism annotation for procedures
that are exported from their containing module.

   If a determinism annotation is supplied for a procedure, the
declared determinism is compared against the inferred determinism.  If
the declared determinism is greater than or not comparable to the
inferred determinism (in the partial ordering above), it is an error.
If the declared determinism is less than the inferred determinism, it
is not an error, but the implementation may issue a warning.

   The determinism category of each goal is inferred according to the
following rules.  These rules work with the two components of
determinism category: whether the goal can fail without producing a
solution, and the maximum number of solutions of the goal (0, 1, or
more).  If the inference process below reports that a goal can succeed
more than once, but the goal generates no outputs that are visible from
outside the goal, and the goal is not impure (*note Impurity::), then
the final determinism of the goal will be based on the goal succeeding
at most once, since the compiler will implicitly prune away any
duplicate solutions.

Calls
     The determinism category of a call is the determinism declared or
     inferred for the called mode of the called procedure.

Unifications
     The determinism of a unification is either `det', `semidet', or
     `failure', depending on its mode.

     A unification that assigns the value of one variable to another is
     deterministic.  A unification that constructs a structure and
     assigns it to a variable is also deterministic.  A unification
     that tests whether a variable has a given top function symbol is
     semideterministic, unless the compiler knows the top function
     symbol of that variable, in which case its determinism is either
     det or failure depending on whether the two function symbols are
     the same or not.  A unification that tests two variables for
     equality is semideterministic, unless the compiler knows that the
     two variables are aliases for one another, in which case the
     unification is deterministic, or unless the compiler knows that
     the two variables have different function symbols in the same
     position, in which case the unification has a determinism of
     failure.

     The compiler knows the top function symbol of a variable if the
     previous part of the procedure definition contains a unification
     of the variable with a function symbol, or if the variable's type
     has only one function symbol.

Conjunctions
     The determinism of the empty conjunction (the goal `true') is
     `det'.  The conjunction `(A, B)' can fail if either A can fail, or
     if A can succeed at least once, and B can fail.  The conjunction
     can succeed at most zero times if either A or B can succeed at
     most zero times.  The conjunction can succeed more than once if
     either A or B can succeed more than once and both A and B can
     succeed at least once.  (If e.g. A can succeed at most zero times,
     then even if B can succeed many times the maximum number of
     solutions of the conjunction is still zero.)  Otherwise, i.e. if
     both A and B succeed at most once, the conjunction can succeed at
     most once.

Switches
     A disjunction is a _switch_ if each disjunct has near its start a
     unification that tests the same bound variable against a different
     function symbol.  For example, consider the common pattern

          (
                  L = [], empty(Out)
          ;
                  L = [H|T], nonempty(H, T, Out)
          )

     If L is input to the disjunction, then the disjunction is a switch
     on L.

     If two variables are unified with each other, then whatever
     function symbol one variable is unified with, the other variable
     is considered to be unified with the same function symbol.  In the
     following example, since K is unified with L, the second disjunct
     unifies L as well as K with cons, and thus the disjunction is
     recognized as a switch.

          (
                  L = [], empty(Out)
          ;
                  K = L, K = [H|T], nonempty(H, T, Out)
          )

     A switch can fail if the various arms of the switch do not cover
     all the function symbols in the type of the switched-on variable,
     or if the code in some arms of the switch can fail, bearing in
     mind that in each arm of the switch, the unification that tests
     the switched-on variable against the function symbol of that arm
     is considered to be deterministic.  A switch can succeed several
     times if some arms of the switch can succeed several times,
     possibly because there are multiple disjuncts that test the
     switched-on variable against the same function symbol.  A switch
     can succeed at most zero times only if all arms of the switch can
     succeed at most zero times.

     Only unifications may occur before the test of the switched-on
     variable in each disjunct. Tests of the switched-on variable may
     occur within existential quantification goals.

     The following example is a switch.

          (
                  Out = 1, L = []
          ;
                  some [H, T] (
                          L = [H|T],
                          nonempty(H, T, Out)
                  )
          )

     The following example is not a switch because the call in the first
     disjunct occurs before the test of the switched-on variable.

          (
                  empty(Out), L = []
          ;
                  L = [H|T], nonempty(H, T, Out)
          )

     The unification of the switched-on variable with a function symbol
     may occur inside a nested disjunction in a given disjunct,
     provided that unification is preceded only by other unifications,
     both inside the nested disjunction and before the nested
     disjunction.  The following example is a switch on X, provided X
     is bound beforehand.

          (
                  X = f
          	p(Out)
          ;
          	Y = X,
                  (
          		Y = g,
          		Intermediate = 42
          	;
          		Z = Y,
          		Z = h(Arg),
          		q(Arg, Intermediate)
          	),
          	r(Intermediate, Out)
          )

Disjunctions
     The determinism of the empty disjunction (the goal `fail') is
     `failure'.  A disjunction `(A ; B)' that is not a switch can fail
     if both A and B can fail.  It can succeed at most zero times if
     both A and B can succeed at most zero times.  It can succeed at
     most once if one of A and B can succeed at most once and the other
     can succeed at most zero times.  Otherwise, i.e. if either A or B
     can succeed more than once, or if both A and B can succeed at
     least once, it can succeed more than once.

If-then-else
     If the condition of an if-then-else cannot fail, the if-then-else
     is equivalent to the conjunction of the condition and the "then"
     part, and its determinism is computed accordingly.  Otherwise, an
     if-then-else can fail if either the "then" part or the "else" part
     can fail.  It can succeed at most zero times if the "else" part
     can succeed at most zero times and if at least one of the
     condition and the "then" part can succeed at most zero times.  It
     can succeed more than once if any one of the condition, the "then"
     part and the "else" part can succeed more than once.

Negations
     If the determinism of the negated goal is `erroneous', then the
     determinism of the negation is `erroneous'.  If the determinism of
     the negated goal is `failure', the determinism of the negation is
     `det'.  If the determinism of the negated goal is `det' or `multi',
     the determinism of the negation is `failure'.  Otherwise, the
     determinism of the negation is `semidet'.



File: mercury_ref.info,  Node: Replacing compile-time checking with run-time checking,  Next: Interfacing nondeterministic code with the real world,  Prev: Determinism checking and inference,  Up: Determinism

6.3 Replacing compile-time checking with run-time checking
==========================================================

Note that "perfect" determinism inference is an undecidable problem,
because it requires solving the halting problem.  (For instance, in the
following example

     :- pred p(T, T).
     :- mode p(in, out) is det.

     p(A, B) :-
             (
                     something_complicated(A, B)
             ;
                     B = A
             ).

`p/2' can have more than one solution only if `something_complicated'
can succeed.)  Sometimes, the rules specified by the Mercury language
for determinism inference will infer a determinism that is not as
precise as you would like.  However, it is generally easy to overcome
such problems.  The way to do this is to replace the compiler's static
checking with some manual run-time checking.  For example, if you know
that a particular goal should never fail, but the compiler infers that
goal to be `semidet', you can check at runtime that the goal does
succeed, and if it fails, call the library predicate `error/1'.

     :- pred q(T, T).
     :- mode q(in, out) is det.

     q(A, B) :-
             ( goal_that_should_never_fail(A, B0) ->
                     B = B0
             ;
                     error("goal_that_should_never_fail failed!")
             ).

The predicate `error/1' has determinism `erroneous', which means the
compiler knows that it will never succeed or fail, so the inferred
determinism for the body of `q/2' is `det'.  (Checking assumptions like
this is good coding style anyway.  The small amount of up-front work
that Mercury requires is paid back in reduced debugging time.)
Mercury's mode analysis knows that computations with determinism
erroneous can never succeed, which is why it does not require the
"else" part to generate a value for `B'.  The introduction of the new
variable `B0' is necessary because the condition of an if-then-else is
a negated context, and can export the values it generates only to the
"then" part of the if-then-else, not directly to the surrounding
computation.  (If the surrounding computations had direct access to
values generated in conditions, they might access them even if the
condition failed.)


File: mercury_ref.info,  Node: Interfacing nondeterministic code with the real world,  Next: Committed choice nondeterminism,  Prev: Replacing compile-time checking with run-time checking,  Up: Determinism

6.4 Interfacing nondeterministic code with the real world
=========================================================

Normally, attempting to call a `nondet' or `multi' mode of a predicate
from a predicate declared as `semidet' or `det' will cause a
determinism error.  So how can we call nondeterministic code from
deterministic code?  There are several alternative possibilities.

   If you just want to see if a nondeterministic goal is satisfiable or
not, without needing to know what variable bindings it produces, then
there is no problem - determinism analysis considers `nondet' and
`multi' goals with no non-local output variables to be `semidet' and
`det' respectively.

   If you want to use the values of output variables, then you need to
ask yourself which one of possibly many solutions to a goal do you want?
If you want all of them, you need to use the predicate `solutions/2' in
the standard library module `solutions', which collects all of the
solutions to a goal into a list -- *note Higher-order::.

   If you just want one solution and don't care which, the calling
predicate should be declared `nondet' or `multi'.  The nondeterminism
should then be propagated up the call tree to the point at which it can
be pruned.  In Mercury, pruning can be achieved in several ways.

   The first way is the one mentioned above: if a goal has no non-local
output variables then the implementation will only attempt to satisfy
the goal once.  Any potential duplicate solutions will be implicitly
pruned away.

   The second way is to rely on the fact that the implementation will
only seek a single solution to `main/2', so alternative solutions to
`main/2' (and hence also to `nondet' or `multi' predicates called
directly or indirectly from `main/2') are implicitly pruned away.  This
is one way to achieve "don't care" style nondeterminism in Mercury.

   The other situation in which you may want pruning and committed
choice style nondeterminism is when you know that all the solutions
returned will be equivalent.  For example, you might want to find the
maximum element in a set by iterating over the elements in the set.
Iterating over the elements in a set in an unspecified order is a
nondeterministic operation, but no matter which order you remove them,
the maximum value in the set should be the same.

   If you know that there will only ever be at most one distinct
solution under the equality theory of the output variables, then you
can use a `promise_equivalent_solutions' determinism cast.

   Note that specifying a user-defined equivalence relation as the
equality predicate for user-defined types (*note User-defined equality
and comparison::) means that `promise_equivalent_solutions' can be used
to express more general forms of equivalence.  For example, if you
define a set type which represents sets as unsorted lists, you would
want to define a user-defined equivalence relation for that type, which
could sort the lists before comparing them.  The
`promise_equivalent_solutions' determinism cast could then be used for
sets even though the lists used to represent the sets might not be in
the same order in every solution.


File: mercury_ref.info,  Node: Committed choice nondeterminism,  Prev: Interfacing nondeterministic code with the real world,  Up: Determinism

6.5 Committed choice nondeterminism
===================================

In addition to the determinism annotations described earlier, there are
"committed choice" versions of `multi' and `nondet', called `cc_multi'
and `cc_nondet'.  These can be used instead of `multi' or `nondet' if
all calls to that mode of the predicate (or function) occur in a
context in which only one solution is needed.

   Such single-solution contexts are determined as follows.

   * The body of any procedure declared `cc_multi' or `cc_nondet' is in
     a single-solution context.  For example, the program entry point
     `main/2' may be declared `cc_multi', and in that case the clauses
     for `main' are in a single-solution context.

   * Any goal with no output variables is in a single-solution context.

   * If a conjunction is in a single-solution context, then the
     right-most conjunct is in a single-solution context, and if the
     right-most conjunct cannot fail, then rest of the conjunction is
     also in a single-solution context.  ("Right-most" here refers to
     the order _after_ mode reordering.)

   * If an if-then-else is in a single-solution context, then the
     "then" part and the "else" part are in single-solution contexts,
     and if the "then" part cannot fail, then the condition of the
     if-then-else is also in a single-solution context.

   * For other compound goals, i.e. disjunctions, negations, and
     (explicitly) existentially quantified goals, if the compound goal
     is in a single-solution context, then the immediate sub-goals of
     that compound goal are also in single-solution contexts.


   The compiler will check that all calls to a committed-choice mode of
a predicate (or function) do indeed occur in a single-solution context.

   You can declare two different modes of a predicate (or function)
which differ only in "cc-ness" (i.e. one being `multi' and the other
`cc_multi', or one being `nondet' and the other `cc_nondet').  In that
case, the compiler will select the appropriate one for each call
depending on whether the call comes from a single-solution context or
not.  Calls from single-solution contexts will call the committed
choice version, while calls which are not from single-solution contexts
will call the backtracking version.

   There are several reasons to use committed choice determinism
annotations.  One reason is for efficiency: committed choice
annotations allow the compiler to generate much more efficient code.
Another reason is for doing I/O, which is allowed only in `det' or
`cc_multi' predicates, not in `multi' predicates.  Another is for
dealing with types that use non-canonical representations (*note
User-defined equality and comparison::).  And there are a variety of
other applications.


File: mercury_ref.info,  Node: User-defined equality and comparison,  Next: Higher-order,  Prev: Determinism,  Up: Top

7 User-defined equality and comparison
**************************************

When defining abstract data types, often it is convenient to use a
non-canonical representation -- that is, one for which a single
abstract value may have more than one different possible concrete
representations.  For example, you may wish to implement an abstract
type `set' by representing a set as an (unsorted) list.

     :- module set_as_unsorted_list.
     :- interface.
     :- type set(T).

     :- implementation.
     :- import_module list.
     :- type set(T) ---> set(list(T)).

In this example, the concrete representations `set([1,2])' and
`set([2,1])' would both represent the same abstract value, namely the
set containing the elements 1 and 2.

   For types such as this, which do not have a canonical representation,
the standard definition of equality is not the desired one; we want
equality on sets to mean equality of the abstract values, not equality
of their representations.  To support such types, Mercury allows
programmers to specify a user-defined equality predicate for
user-defined types:

     :- type set(T) ---> set(list(T))
             where equality is set_equals.

Here `set_equals' is the name of a user-defined predicate that is used
for equality on the type `set(T)'.  It could for example be defined in
terms of a `subset' predicate.

     :- pred set_equals(set(T)::in, set(T)::in) is semidet.
     set_equals(S1, S2) :-
             subset(S1, S2),
             subset(S2, S1).

   A comparison predicate can also be supplied.

     :- type set(T) ---> set(list(T))
             where equality is set_equals, comparison is set_compare.

     :- pred set_compare(builtin.comparison_result::uo,
                     set(T)::in, set(T)::in) is det.
     set_compare(Result, Set1, Set2) :-
     	promise_equivalent_solutions [Result] (
     		set_compare_2(Set1, Set2, Result)
     	).

     :- pred set_compare_2(set(T)::in, set(T)::in,
                     builtin.comparison_result::uo) is cc_multi.
     set_compare_2(set(List1), set(List2), Result) :-
             builtin.compare(Result, list.sort(List1), list.sort(List2)).

   If a comparison predicate is supplied and the unification predicate
is omitted, a unification predicate is generated by the compiler in
terms of the comparison predicate.  For the `set' example, the
generated predicate would be:

     set_equals(S1, S2) :-
             set_compare((=), S1, S2).

   If a unification predicate is supplied without a comparison
predicate, the compiler will generate a comparison predicate which
throws an exception of type `exception.software_error' when called.

   A type declaration for a type `foo(T1, ..., TN)' may contain a
`where equality is EQUALITYPRED' specification only if it declares a
discriminated union type or a foreign type (*note Using foreign types
from Mercury::) and the following conditions are satisfied:

   * EQUALITYPRED must be the name of a predicate with signature
          :- pred EQUALITYPRED(foo(T1, ..., TN)::in,
                          foo(T1, ..., TN)::in) is semidet.

     It is legal for the type, mode and determinism to be more
     permissive: the type or the mode's initial insts may be more
     general (e.g. the type of the equality predicate could be just the
     polymorphic type `pred(T, T)') and the mode's final insts or the
     determinism may be more specific (e.g. the determinism of the
     equality predicate could be any of `det', `failure' or
     `erroneous').

   * If the type is a discriminated union then its definition cannot be
     a single zero-arity constructor.

   * The equality predicate must be "pure" (*note Impurity::).

   * The equality predicate must be defined in the same module as the
     type.

   * If the type is exported the equality predicate must also be
     exported.

   * EQUALITYPRED should be an equivalence relation; that is, it must be
     symmetric, reflexive, and transitive.  However, the compiler is
     not required to check this(1).


   Types with user-defined equality can only be used in limited ways.
Because there multiple representations for the same abstract value, any
attempt to examine the representation of such a value is a conceptually
non-deterministic operation.  In Mercury this is modelled using
committed choice nondeterminism.

   The semantics of specifying `where equality is EQUALITYPRED' on the
type declaration for a type T are as follows:

   * If the program contains any deconstruction unification or switch
     on a variable of type T that could fail, other than unifications
     with mode `(in, in)', then it is a compile-time error.

   * If the program contains any deconstruction unification or switch
     on a variable of type T that cannot fail, then that operation has
     determinism `cc_multi'.

   * Any attempts to examine the representation of a variable of type T
     using facilities of the standard library (e.g. `argument'/3 and
     `functor/3' in `deconstruct') that do not have determinism
     `cc_multi' or `cc_nondet' will result in a run-time error.

   * In addition to the usual equality axioms, the declarative
     semantics of the program will contain the axiom `X = Y <=>
     EQUALITYPRED(X, Y)' for all X and Y of type `T'.

   * Any `(in, in)' unifications for type T are computed using the
     specified predicate EQUALITYPRED.


   A type declaration for a type `foo(T1, ..., TN)' may contain a
`where comparison is COMPAREPRED' specification only if it declares a
discriminated union type or a foreign type (*note Using foreign types
from Mercury::) and the following conditions are satisfied:

   * COMPAREPRED must be the name of a predicate with signature
          :- pred COMPAREPRED(builtin.comparison_result::uo,
                          foo(T1, ..., TN)::in, foo(T1, ..., TN)::in) is det.

     As with equality predicates, it is legal for the type, mode and
     determinism to be more permissive.

   * If the type is a discriminated union then its definition cannot be
     a single zero-arity constructor.

   * The comparison predicate must also be "pure" (*note Impurity::).

   * The comparison predicate must be defined in the same module as the
     type.

   * If the type is exported the comparison predicate must also be
     exported.

   * The relation
          compare_eq(X, Y) :- COMPAREPRED((=), X, Y).
     must be an equivalence relation; that is, it must be symmetric,
     reflexive, and transitive.  The compiler is not required to check
     this.

   * The relations
          compare_leq(X, Y) :- COMPAREPRED(R, X, Y), (R = (=) ; R = (<)).
          compare_geq(X, Y) :- COMPAREPRED(R, X, Y), (R = (=) ; R = (>)).
     must be total order relations: that is they must be antisymmetric,
     reflexive and transitive.  The compiler is not required to check
     this.


   For each type for which the declaration has a `where comparison is
COMPAREPRED' specification, any calls to the standard library predicate
`builtin.compare/3' with arguments of that type are evaluated as if
they were calls to COMPAREPRED.

   A type declaration may contain a `where equality is EQUALITYPRED,
comparison is COMPAREPRED' specification only if in addition to the
conditions above, `all [X, Y] (COMPAREPRED((=), X, Y) <=>
EQUALITYPRED(X, Y))'.  The compiler is not required to check this.

   ---------- Footnotes ----------

   (1) If EQUALITYPRED is not an equivalence relation, then the program
is inconsistent: its declarative semantics contains a contradiction,
because the additional axioms for the user-defined equality contradict
the standard equality axioms.  That implies that the implementation may
compute any answer at all (*note Semantics::), i.e. the behaviour of
the program is undefined.


File: mercury_ref.info,  Node: Higher-order,  Next: Modules,  Prev: User-defined equality and comparison,  Up: Top

8 Higher-order programming
**************************

Mercury supports higher-order functions and predicates with currying,
closures, and lambda expressions.  (To be pedantic, it would be more
accurate to say that Mercury supports higher-order procedures: in
Mercury, when you construct a higher-order term, you only get one mode
of a predicate or function; if you want multiple modes, you must pass
multiple higher-order procedures.)

* Menu:

* Creating higher-order terms::
* Calling higher-order terms::
* Higher-order modes::


File: mercury_ref.info,  Node: Creating higher-order terms,  Next: Calling higher-order terms,  Up: Higher-order

8.1 Creating higher-order terms
===============================

To create a higher-order predicate or function term, you can use a
lambda expression, or, if the predicate or function has only one mode
and it is not a zero-arity function, you can just use its name.  For
example, if you have declared a predicate

     :- pred sum(list(int), int).
     :- mode sum(in, out) is det.

the following unifications have the same effect:

     X = (pred(List::in, Length::out) is det :- sum(List, Length))
     Y = sum

   In the above example, the type of `X', and `Y' is `pred(list(int),
int)', which means a predicate of two arguments of types `list(int)'
and `int' respectively.

   Similarly, given

     :- func scalar_product(int, list(int)) = list(int).
     :- mode scalar_product(in, in) = out is det.

the following three unifications have the same effect:

     X = (func(Num, List) = NewList :- NewList = scalar_product(Num, List))
     Y = (func(Num::in, List::in) = (NewList::out) is det
             :- NewList = scalar_product(Num, List))
     Z = scalar_product

   In the above example, the type of `X', `Y', and `Z' is `func(int,
list(int)) = list(int)', which means a function of two arguments, whose
types are `int' and `list(int)', with a return type of `int'.  As with
`:- func' declarations, if the modes and determinism of the function
are omitted in a higher-order function term, then the modes default to
`in' for the arguments, `out' for the function result, and the
determinism defaults to `det'.

   The Melbourne Mercury implementation currently requires that you use
an explicit lambda expression to specify which mode you want, if the
predicate or function has more than one mode (but see below for an
exception to this rule).

   You can also create higher-order function terms of non-zero arity
and higher-order predicate terms by "currying", i.e. specifying the
first few arguments to a predicate or function, but leaving the
remaining arguments unspecified.  For example, the unification

     Sum123 = sum([1,2,3])

binds `Sum123' to a higher-order predicate term of type `pred(int)'.
Similarly, the unification

     Double = scalar_product(2)

binds `Double' to a higher-order function term of type `func(list(int))
= list(int)'.

   As a special case, currying of a multi-moded predicate or function
is allowed provided that the mode of the predicate or function can be
determined from the insts of the higher-order curried arguments.  For
example, `P = list.foldl(io.write)' is allowed because the inst of
`io.write' matches exactly one mode of `list.foldl'.

   For higher-order predicate expressions that thread an accumulator
pair, we have syntax that allows you to use DCG notation in the goal of
the expression.  For example,

     Pred = (pred(Strings::in, Num::out, di, uo) is det -->
         io.write_string("The strings are: "),
         { list.length(Strings, Num) },
         io.write_strings(Strings),
         io.nl
     )

is equivalent to

     Pred = (pred(Strings::in, Num::out, IO0::di, IO::uo) is det :-
         io.write_string("The strings are: ", IO0, IO1),
         list.length(Strings, Num),
         io.write_strings(Strings, IO1, IO2),
         io.nl(IO2, IO)
     )

   Higher-order function terms of zero arity can only be created using
an explicit lambda expression; you have to use e.g. `(func) = foo'
rather than plain `foo', because the latter denotes the result of
evaluating the function, rather than the function itself.

   Note that when constructing a higher-order term, you cannot just use
the name of a builtin language construct such as `=', `\=', `call', or
`apply', and nor can such constructs be curried.  Instead, you must
either use an explicit lambda expression, or you must write a
forwarding predicate or function.  For example, instead of

     list.filter(\=(2), [1, 2, 3], List)

you must write either

     list.filter((pred(X::in) is semidet :- X \= 2), [1, 2, 3], List)

or

     list.filter(not_equal(2), [1, 2, 3], List)

where you have defined `not_equal' using

     :- pred not_equal(T::in, T::in) is semidet.
     not_equal(X, Y) :- X \= Y.

   Another case when this arises is when want to curry a higher-order
term.  Suppose, for example, that you have a higher-order predicate
term `OldPred' of type `pred(int, char, float)', and you want to
construct a new higher-order predicate term `NewPred' of type
`pred(char, float)' from `OldPred' by supplying a value for just the
first argument.  The solution is the same: use an explicit lambda
expression or a forwarding predicate.  In either case, the body of the
lambda expression or the forwarding predicate must contain a
higher-order call with all the arguments supplied.


File: mercury_ref.info,  Node: Calling higher-order terms,  Next: Higher-order modes,  Prev: Creating higher-order terms,  Up: Higher-order

8.2 Calling higher-order terms
==============================

Once you have created a higher-order predicate term (sometimes known as
a closure), the next thing you want to do is to call it.  For
predicates, you use the builtin goal call/N:

`call(Closure)'
`call(Closure1, Arg1)'
`call(Closure2, Arg1, Arg2)'
...
     A higher-order predicate call.  `call(Closure)' just calls the
     specified higher-order predicate term.  The other forms append the
     specified arguments onto the argument list of the closure before
     calling it.

   For example, the goal

     call(Sum123, Result)

would bind `Result' to the sum of `[1, 2, 3]', i.e. to 6.

   For functions, you use the builtin expression apply/N:

`apply(Closure)'
`apply(Closure1, Arg1)'
`apply(Closure2, Arg1, Arg2)'
...
     A higher-order function application.  Such a term denotes the
     result of invoking the specified higher-order function term with
     the specified arguments.

   For example, given the definition of `Double' above, the goal

     List = apply(Double, [1, 2, 3])

would be equivalent to

     List = scalar_product(2, [1, 2, 3])

and so for a suitable implementation of the function `scalar_product/2'
this would bind `List' to `[2, 4, 6]'.

   One extremely useful higher-order predicate in the Mercury standard
library is `solutions/2', which has the following declaration:

     :- pred solutions(pred(T), list(T)).
     :- mode solutions(pred(out) is nondet, out) is det.

   The term which you pass to `solutions/2' is a higher-order predicate
term.  You can pass the name of a one-argument predicate, or you can
pass a several-argument predicate with all but one of the arguments
supplied (a closure).  The declarative semantics of `solutions/2' can
be defined as follows:

     solutions(Pred, List) is true iff
             all [X] (call(Pred, X) <=> list.member(X, List))
             and List is sorted.

where `call(Pred, X)' invokes the higher-order predicate term `Pred'
with argument `X', and where `list.member/2' is the standard library
predicate for list membership.  In other words, `solutions(Pred, List)'
finds all the values of `X' for which `call(Pred, X)' is true, collects
these solutions in a list, sorts the list, and returns that list as its
result.  Here's an example: the standard library defines a predicate
`list.perm(List0, List)'

     :- pred list.perm(list(T), list(T)).
     :- mode list.perm(in, out) is nondet.

which succeeds iff List is a permutation of List0.  Hence the following
call to solutions

     solutions(list.perm([3,1,2]), L)

should return all the possible permutations of the list `[3,1,2]' in
sorted order:

     L = [[1,2,3],[1,3,2],[2,1,3],[2,3,1],[3,1,2],[3,2,1]].

   See also `unsorted_solutions/2' and `solutions_set/2', which are
defined in the standard library module `solutions' and documented in
the Mercury Library Reference Manual.


File: mercury_ref.info,  Node: Higher-order modes,  Prev: Calling higher-order terms,  Up: Higher-order

8.3 Higher-order modes
======================

In Mercury, the mode and determinism of a higher-order predicate or
function term are part of that term's _inst_, not its _type_.  This
allows a single higher-order predicate to work on argument predicates
of different modes and determinism, which is particularly useful for
library predicates such as `list.map' and `list.foldl'.

   The language contains builtin `inst' values

     (pred) is DETERMINISM
     pred(MODE) is DETERMINISM
     pred(MODE1, MODE2) is DETERMINISM
     ...
     (func) = MODE is DETERMINISM
     func(MODE1) = MODE is DETERMINISM
     func(MODE1, MODE2) = MODE is DETERMINISM
     ...

   These insts represent the instantiation state of variables bound to
higher-order predicate and function terms with the appropriate mode and
determinism.  For example, `pred(out) is det' represents the
instantiation state of being bound to a higher-order predicate term
which is `det' and accepts one output argument; the term `sum([1,2,3])'
from the example above is one such higher-order predicate term which
matches this instantiation state.

   As a convenience, the language also contains builtin `mode' values
of the same name (and they are what we have been using in the examples
up to now).  These modes map from the corresponding `inst' to itself.
It is as if they were defined by

     :- mode (pred is DETERMINISM) == in(pred is DETERMINISM).
     :- mode (pred(INST) is DETERMINISM) ==
         in(pred(INST) is DETERMINISM).
     ...

using the parametric inst `in/1' mentioned in *note Modes:: which maps
an inst to itself.

   If you want to define a predicate which returns a higher-order
predicate term, you would use a mode such as `free >> pred(...) is ...',
or `out(pred(...) is ... )'.  For example:

     :- pred foo(pred(int)).
     :- mode foo(free >> pred(out) is det) is det.

     foo(sum([1,2,3])).

   Note that in Mercury it is an error to attempt to unify two
higher-order terms.  This is because equivalence of higher-order terms
is undecidable in the general case.

   For example, given the definition of `foo' above, the goal

             foo((pred(X::out) is det :- X = 6))

is illegal.  If you really want to compare higher-order predicates for
equivalence, you must program it yourself; for example, the above goal
could legally be written as

             P = (pred(X::out) is det :- X = 6),
             foo(Q),
             all [X] (call(P, X) <=> call(Q, X)).

   Note that the compiler will only catch direct attempts at
higher-order unifications; indirect attempts (via polymorphic
predicates, for example `(list.append([], [P], [Q])' may result in an
error at run-time rather than at compile-time.

   In order to call a higher-order term, the compiler must know its
higher-order inst.  This can cause problems when higher-order terms are
placed into a polymorphic collection type and then extracted, since the
declared mode for the extraction will typically be `out' and the
higher-order inst information will be lost.  To partially alleviate
this problem, and to make higher-order functional programming easier,
if the term to be called has a function type, but no higher-order inst
information, we assume that it has the default higher-order function
inst `func(in, ..., in) = out is DETERMINISM'.

   As a consequence of this, it is a mode error to pass a higher-order
function term that does not match this standard mode to somewhere where
its higher-order inst information may be lost, such as to a polymorphic
predicate where the argument mode is `in'.

   Mercury also provides builtin `inst' values for use with solver
types:

     any_pred is DETERMINISM
     any_pred(MODE) is DETERMINISM
     any_pred(MODE1, MODE2) is DETERMINISM
     ...
     any_func = MODE is DETERMINISM
     any_func(MODE1) = MODE is DETERMINISM
     any_func(MODE1, MODE2) = MODE is DETERMINISM
     ...

   See *note Solver types:: for more details.


File: mercury_ref.info,  Node: Modules,  Next: Type classes,  Prev: Higher-order,  Up: Top

9 Modules
*********

* Menu:

* The module system::
* An example module::
* Sub-modules::
* Module initialisation::
* Module finalisation::
* Module-local mutable variables::


File: mercury_ref.info,  Node: The module system,  Next: An example module,  Up: Modules

9.1 The module system
=====================

The Mercury module system is relatively simple and straightforward.

   Each module must start with a `:- module MODULENAME' declaration,
specifying the name of the module.

   An `:- interface.' declaration indicates the start of the module's
interface section: this section specifies the entities that are
exported by this module.  Mercury provides support for abstract data
types, by allowing the definition of a type to be kept hidden, with the
interface only exporting the type name.  The interface section may
contain definitions of types, type classes, data constructors,
instantiation states, and modes, and declarations for abstract data
types, abstract type class instances, functions, predicates, and
(sub-)modules.  The interface section may not contain definitions for
functions or predicates (i.e. clauses), or definitions of (sub-)modules.

   An `:- implementation.' declaration indicates the start of the
module's implementation section.  Any entities declared in this section
are local to the module (and its sub-modules) and cannot be used by
other modules.  The implementation section must contain definitions for
all abstract data types, abstract instance declarations, functions,
predicates, and sub-modules exported by the module, as well as for all
local types, type class instances, functions, predicates, and
sub-modules.  The implementation section can be omitted if it is empty.

   The module may optionally end with a `:- end_module MODULENAME'
declaration; the name specified in the `end_module' must be the same as
that in the corresponding `module' declaration.

   If a module wishes to make use of entities exported by other modules,
then it must explicitly import those modules using one or more `:-
import_module MODULES' or `:- use_module MODULES' declarations, in
order to make those declarations visible.  In both cases, MODULES is a
comma-separated list of fully-qualified module names.  These
declarations may occur either in the interface or the implementation
section.  If the imported entities are used in the interface section,
then the corresponding `import_module' or `use_module' declaration must
also be in the interface section.  If the imported entities are only
used in the implementation section, the `import_module' or `use_module'
declaration should be in the implementation section.

   The names of predicates, functions, constructors, constructor fields,
types, modes, insts, type classes, and (sub-)modules can be explicitly
module qualified using the `.' operator, e.g. `module.name' or
`module.submodule.name'.  This is useful both for readability and for
resolving name conflicts.  Uses of entities imported using `use_module'
declarations _must_ be explicitly module qualified.

   Currently we also support `__' as an alternative module qualifier,
so you can write `module__name' instead of `module.name'.

   Certain optimizations require information or source code for
predicates defined in other modules to be as effective as possible.  At
the moment, inlining and higher-order specialization are the only
optimizations that the Mercury compiler can perform across module
boundaries.

   One module must export a predicate `main/2', which must be declared
as either

     :- pred main(io.state::di, io.state::uo) is det.

or

     :- pred main(io.state::di, io.state::uo) is cc_multi.

(or any declaration equivalent to one of the two above).

   Mercury has a standard library which includes modules for lists,
stacks, queues, priority queues, sets, bags (multi-sets), maps
(dictionaries), random number generation, input/output and filename and
directory handling.  See the Mercury Library Reference Manual for
details.


File: mercury_ref.info,  Node: An example module,  Next: Sub-modules,  Prev: The module system,  Up: Modules

9.2 An example module.
======================

For illustrative purposes, here is the definition of a simple module
for managing queues:

     :- module queue.
     :- interface.

     % Declare an abstract data type.

     :- type queue(T).

     % Declare some predicates which operate on the abstract data type.

     :- pred empty_queue(queue(T)).
     :- mode empty_queue(out) is det.
     :- mode empty_queue(in) is semidet.

     :- pred put(queue(T), T, queue(T)).
     :- mode put(in, in, out) is det.

     :- pred get(queue(T), T, queue(T)).
     :- mode get(in, out, out) is semidet.

     :- implementation.

     % Queues are implemented as lists. We need the `list' module
     % for the declaration of the type list(T), with its constructors
     % '[]'/0 % and '.'/2, and for the declaration of the predicate
     % list.append/3.

     :- import_module list.

     % Define the queue ADT.

     :- type queue(T) == list(T).

     % Declare the exported predicates.

     empty_queue([]).

     put(Queue0, Elem, Queue) :-
              list.append(Queue0, [Elem], Queue).

     get([Elem | Queue], Elem, Queue).

     :- end_module queue.


File: mercury_ref.info,  Node: Sub-modules,  Next: Module initialisation,  Prev: An example module,  Up: Modules

9.3 Sub-modules
===============

As mentioned above, modules may contain sub-modules.  There are two
kinds of sub-modules, called nested sub-modules and separate
sub-modules; the difference is that nested sub-modules are defined in
the same source file as the containing module, whereas separate
sub-modules are defined in separate source files.  Implementations
should support separate compilation of separate sub-modules.

   A module may not contain more than one sub-module with the same name.

* Menu:

* Nested sub-modules::
* Separate sub-modules::
* Visibility rules::
* Implementation bugs and limitations::


File: mercury_ref.info,  Node: Nested sub-modules,  Next: Separate sub-modules,  Up: Sub-modules

9.3.1 Nested sub-modules
------------------------

Nested sub-modules within a module are delimited by matching `:-
module' and `:- end_module' declarations.  (Note that `:- end_module'
for nested sub-modules are mandatory, not optional, even if the nested
sub-module is the last thing in the source file.  Also note that the
module name in a `:- module' or `:- end_module' declaration need not be
fully-qualified.)  The sequence of items thus delimited is known as a
sub-module item sequence.

   The interface and implementation parts of a nested sub-module may be
specified in two different sub-module declarations.  If a sub-module
item sequence includes an interface section, then it is a declaration
of that sub-module; if it includes an implementation section, then it
is a definition of that sub-module; and if includes both, then it is
both declaration and definition.

   It is an error to declare a sub-module twice, or to define it twice.
It is an error to define a sub-module without declaring it.  As
mentioned earlier, it is an error to define a sub-module in the
interface section of its parent module.

   If a sub-module is declared but not explicitly defined, then there
is an implicit definition with an empty implementation section for that
sub-module (this will result in an error, if the interface section
includes declarations but not definitions for any types, predicates,
modes, or (doubly) nested sub-modules).


File: mercury_ref.info,  Node: Separate sub-modules,  Next: Visibility rules,  Prev: Nested sub-modules,  Up: Sub-modules

9.3.2 Separate sub-modules
--------------------------

Separate sub-modules are declared using `:- include_module MODULES'
declarations.  Each `:- include_module' declaration specifies a
comma-separated list of sub-modules.

     :- include_module MODULE1, MODULE2, ..., MODULEN.

   Each of the named sub-modules in an `:- include_module' declaration
must be defined in a separate source file.  The mapping between module
names and source file names is implementation-defined.  (For a module
named `foo.bar.baz', The University of Melbourne Mercury implementation
requires the source to be located in a file named `foo.bar.baz.m',
`bar.baz.m', or `baz.m'.)  The separate source file must contain the
declaration (interface) and definition (implementation) of the
sub-module.  It must start with a `:- module' declaration which matches
that in the `:- include_module' declaration in the parent, followed by
the interface and (if necessary) implementation sections, and it may
optionally end with a `:- end_module' declaration.  (Note: the module
names in the `:- module', `:- end_module', and `:- include_module'
declarations need not be fully-qualified.  However, if the file name
used for a particular module does not include all the module
qualifiers, then the University of Melbourne Mercury implementation
requires the module name in the `:- module' declaration for that module
to be fully qualified.)

   The semantics of separate sub-modules are identical to those of
nested sub-modules.  The procedure to transform a separate sub-module
into a nested sub-module is as follows:

  1. Replace the `:- include_module SUBMODULE' declaration with the
     interface section of the sub-module enclosed within `:- module
     SUBMODULE' and `:- end_module SUBMODULE' declarations.

  2. Place the implementation section of the sub-module enclosed within
     `:- module SUBMODULE' and `:- end_module SUBMODULE' declarations
     in the implementation section of the parent module.

   For example

     :- module x.
     :- interface.
     :- include_module y.
     :- end_module x.

is equivalent to

     :- module x.
     :- interface.
         :- module y.
         % interface section of module `y'
         :- end_module y.
     :- implementation.
         :- module y.
         % implementation section of module `y'
         :- end_module y.
     :- end_module x.


File: mercury_ref.info,  Node: Visibility rules,  Next: Implementation bugs and limitations,  Prev: Separate sub-modules,  Up: Sub-modules

9.3.3 Visibility rules
----------------------

Any declarations in the parent module, including those in the parent
module's implementation section, are visible in the parent's
sub-modules, including indirect sub-modules (i.e. sub-sub-modules,
etc.).  Similarly, declarations in the interfaces of any modules
imported using an `:- import_module' or a `:- use_module' in the parent
module are visible in the parent's sub-modules, including indirect
sub-modules.

   Declarations in a child module are not visible in the parent module,
or in "sibling" modules (other children of the same parent), or in
other unrelated modules unless the child is explicitly imported using
an `:- import_module' or `:- use_module' declaration.  It is an error
to import a module without importing all of its parent modules.

   Note that a sub-module for which the `:- module' or `:-
include_module' declaration occurs only in the implementation section
of the parent module may only be imported or used by its parent module
or by sub-modules of its parent module.

   Note that as mentioned previously, all `:- import_module' and `:-
use_module' declarations must use fully-qualified module names.


File: mercury_ref.info,  Node: Implementation bugs and limitations,  Prev: Visibility rules,  Up: Sub-modules

9.3.4 Implementation bugs and limitations
-----------------------------------------

The current implementation of sub-modules has a couple of minor
limitations.

   * The compiler sometimes reports spurious errors if you define an
     equivalence type in a sub-module and export it as abstract type.

   * Using `mmake' to do parallel makes (e.g. `mmake --jobs 2') doesn't
     always work correctly if you're using nested sub-modules.  (The
     work-around is to use separate sub-modules instead of nested
     sub-modules, i.e. to put the sub-modules in separate source files.)


File: mercury_ref.info,  Node: Module initialisation,  Next: Module finalisation,  Prev: Sub-modules,  Up: Modules

9.4 Module initialisation
=========================

Modules that interact with foreign libraries or services may require
special initialisation before use.  Such modules may include any number
of `initialise' directives in their implementation sections.  An
`initialise' directive has the following form:

     :- initialise initpredname/arity.

   where the predicate `initpredname' must be declared with one of the
following signatures:

     :- pred initpredname(io::di, io::uo) is DET.
     :- impure pred initpredname is DET.

   DET must be either `det' or `cc_multi'.

   The effect of the `initialise' declaration is to ensure that
`initpredname/arity' is invoked before the program's `main/2'
predicate.  Initialisation predicates within a module are executed in
the order in which they are specified, although no order may be assumed
between different modules or sub-modules.  Initialisation predicates
are only invoked after any initialisation required by the Mercury
standard library.

   If `initpredname/arity' terminates with an uncaught exception then
the program will immediately abort execution.  In this circumstance
those predicates specified by other `initialise' directives that have
not yet been executed will not be executed, `main/2' will not be
executed and no predicate specified in a `finalise' directive will be
executed.

   `initialize' is also allowed as a synonym for `initialise'.


File: mercury_ref.info,  Node: Module finalisation,  Next: Module-local mutable variables,  Prev: Module initialisation,  Up: Modules

9.5 Module finalisation
=======================

Modules that require special finalisation at program termination may
include any number of `finalise' directives in their implementation
sections.

   A `finalise' directive has the following form:

     :- finalise finalpredname/arity.

   where the predicate `finalpredname/arity' must be declared with one
of the following signature:

     :- pred finalpredname(io::di, io::uo) is DET.
     :- impure pred finalpredname is DET

   DET must be either `det' or `cc_multi'.

   The effect of the `finalise' declaration is to ensure that
`finalpredname/arity' is invoked after the program's `main' predicate.
Finalisation predicates within a module are executed in the order in
which they are specified, although no order may be assumed between
different modules or sub-modules.  Any finalisation required by the
Mercury standard library will always occur after any finalisation
predicates have been invoked.

   If `finalpredname/arity' terminates with an uncaught exception then
the program will immediately abort execution.  No predicates specified
by other `finalise' directives that have not yet been executed will be
executed.

   `finalize' is also allowed as a synonym for `finalise'.


File: mercury_ref.info,  Node: Module-local mutable variables,  Prev: Module finalisation,  Up: Modules

9.6 Module-local mutable variables
==================================

Certain special cases require a module to have one or more mutable (i.e.
destructively updatable) variables, for example to hold the constraint
store for a solver type.

   A mutable variable is declared using the `mutable' directive:

     :- mutable(varname, vartype, initial_value, varinst, [attribute, ...]).

   This constructs a new mutable variable with access predicates that
have the following signatures:

     :- semipure pred get_varname(vartype::out(varinst)) is det.
     :- impure   pred set_varname(vartype::in(varinst)) is det.

   The initial value of `varname' is `initial_value', which is set
before the program's `main/2' predicate is executed.

   The type `vartype' is not allowed to contain any type variables or
have any type class constraints.

   The inst `varinst' is not allowed to contain any inst variables.  It
is also not allowed to be equivalent to, or contain components that are
equivalent to, the builtin insts `free', `unique', `mostly_unique',
`dead' or `mostly_dead'.

   The initial value of a mutable, `initial_value', may be any Mercury
expression with type `vartype' and inst `varinst' subject to the above
restrictions. It may be impure or semipure.

   The following `attributes' must be supported:

`trailed'/`untrailed'
     This attribute declares if the implementation should generate code
     so that the effects of `set_varname/1' can be undone on
     backtracking.  The default, in case none is specified, is
     `trailed'.

`attach_to_io_state'
     This attribute causes the compiler to also construct access
     predicates that have the following signatures:

          :- pred get_varname(vartype::out(varinst), io::di, io::uo) is det.
          :- pred set_varname(vartype::in(varinst),  io::di, io::uo) is det.

`constant'
     This attribute causes the compiler to construct only a `get'
     access predicate, but not a `set' access predicate.  Since
     `varname' will always have the initial value given to it, the
     `get' access predicate is pure; its signature will be:

          :- pred get_varname(vartype::out(varinst)) is det.

     The `constant' attribute cannot be specified together with the
     `attach_to_io_state' attribute (since they disagree on this
     signature).  It also cannot be specified together with an explicit
     `trailed' attribute.


   The Melbourne Mercury compiler also supports the following
attributes:

`foreign_name(Lang, Name)'
     Allow foreign code to access the mutable variable in some
     implementation dependent manner.  `Lang' must be a valid target
     language for this Mercury implementation.  `Name' must be a valid
     identifier in that language.  It is an error to specify more than
     one foreign name attribute for each language.

     For the C backends this attribute allows foreign code to access
     the mutable variable as an external variable called `Name'.  For
     the low-level C backend, e.g. the asm_fast grades, the type of this
     variable will be `MR_Word'.  For the high-level C backend, e.g.
     the hlc grades, the type of this variable depends upon the Mercury
     type of the mutable.  For mutables of the Mercury types `int',
     `float', `char' and `string', the corresponding C types will be
     `MR_Integer', `MR_Float', `MR_Char' and `MR_String' respectively.
     For mutables of any other type the corresponding C type will be
     `MR_Word'.

     This attribute is not currently implemented for the non-C backends.

`thread_local'
     This attribute allows a mutable to take on different values in each
     thread.  When a child thread is spawned, it inherits all the
     values of thread-local mutables of the parent thread.  Changing
     the value of a thread-local mutable does not affect its value in
     any other threads.

     The `thread_local' attribute cannot be specified together with
     either of the `trailed' or `constant' attributes.


   It is an error for a `mutable' directive to appear in the interface
section of a module.  The usual visibility rules for sub-modules apply
to the mutable variable access predicates.

   For the purposes of determining when mutables are assigned their
initial values, the expression `initial_value' behaves as though it were
a predicate specified in an `initialise' directive.

             :- initialise foo/2.
             :- mutable(bar, int, 561, ground, [untrailed]).
             :- initialise baz/2.

   In the above example `foo/2' is invoked first, then `bar' is set
with an initial value of 561 and the `baz/2' is invoked.

   The effect of a mutable initial value expression terminating with an
uncaught exception is also the same as though it were a predicate
specified in a `initialise' directive.


File: mercury_ref.info,  Node: Type classes,  Next: Existential types,  Prev: Modules,  Up: Top

10 Type classes
***************

Mercury supports constrained polymorphism in the form of type classes.
Type classes allow the programmer to write predicates and functions
which operate on variables of any type (or sequence of types) for which
a certain set of operations is defined.

* Menu:

* Typeclass declarations::
* Instance declarations::
* Abstract typeclass declarations::
* Abstract instance declarations::
* Type class constraints on predicates and functions::
* Type class constraints on type class declarations::
* Type class constraints on instance declarations::
* Functional dependencies::


File: mercury_ref.info,  Node: Typeclass declarations,  Next: Instance declarations,  Up: Type classes

10.1 Typeclass declarations
===========================

A "type class" is a name for a set of types (or a set of sequences of
types) for which certain predicates and/or functions, called the
"methods" of that type class, are defined.  A `typeclass' declaration
defines a new type class, and specifies the set of predicates and/or
functions that must be defined on a type (or sequence of types) for it
(them) to be considered to be an instance of that type class.

   The `typeclass' declaration gives the name of the type class that it
is defining, the names of the type variables which are parameters to
the type class, and the operations (i.e. methods) which form the
interface of the type class.  For each method, all parameters of the
typeclass must be determined by the type variables appearing in the
type signature of the method.  A variable is determined by a type
signature if it appears in the type signature, but if functional
dependencies are present then it may also be determined from the other
variables (*note Functional dependencies::).

   For example,

     :- typeclass point(T) where [
             % coords(Point, X, Y):
             %       X and Y are the cartesian coordinates of Point
             pred coords(T, float, float),
             mode coords(in, out, out) is det,

             % translate(Point, X_Offset, Y_Offset) = NewPoint:
             %       NewPoint is Point translated X_Offset units in the X direction
             %       and Y_Offset units in the Y direction
             func translate(T, float, float) = T
     ].

declares the type class `point', which represents points in two
dimensional space.

   `pred', `func' and `mode' declarations are the only legal
declarations inside a `typeclass' declaration.  The mode and
determinism of type class methods must be explicitly declared or (for
functions) defaulted, not inferred.  In other words, for each predicate
declared in a type class, there must be at least one mode declaration,
and each mode declaration in a type class must include an explicit
determinism annotation.  Functions with no explicit mode declaration
get the usual default mode (*note Modes::): all arguments have mode
`in', the result has mode `out', and the determinism is `det'.

   The number of parameters to the type class (e.g. `T') is not limited.
For example, the following is allowed:

     :- typeclass a(T1, T2) where [...].

   The parameters must be distinct variables.  Each `typeclass'
declaration must have at least one parameter.

   It is OK for a `typeclass' declaration to declare no methods, e.g.

     :- typeclass foo(T) where [].

   There must not be more than one type class declaration with the same
name and arity in the same module.


File: mercury_ref.info,  Node: Instance declarations,  Next: Abstract typeclass declarations,  Prev: Typeclass declarations,  Up: Type classes

10.2 Instance declarations
==========================

Once the interface of the type class has been defined in the `typeclass'
declaration, we can use an `instance' declaration to define how a
particular type (or sequence of types) satisfies the interface declared
in the `typeclass' declaration.

   An instance declaration has the form

     :- instance CLASSNAME(TYPENAME(TYPEVAR, ...), ...)
             where [METHODDEFINITION, METHODDEFINITION, ...].

   An `instance' declaration gives a type for each parameter of the
type class.  Each of these types must be either a type with no
arguments, or a polymorphic type whose arguments are all distinct type
variables.  For example `int', `list(T)' and `bintree(K,V)' are allowed,
but `T', `list(int)' and `bintree(T,T)' are not.  The types in an
instance declaration must not be abstract types which are elsewhere
defined as equivalence types.  A program may not contain more than one
instance declaration for a particular type (or sequence of types, in
the case of a multi-parameter type class) and typeclass.  These
restrictions ensure that there are no overlapping instance
declarations, i.e. for each typeclass there is at most one instance
declaration that may be applied to any type (or sequence of types).

   Each METHODDEFINITION entry in the `where [...]' part of an
`instance' declaration defines the implementation of one of the class
methods for this instance.  There are two ways of defining methods.
The first way is to define a method by giving the name of the predicate
or function which implements that method.  In this case, the
METHODDEFINITION must have one of the following forms:

     pred(METHODNAME/ARITY) is PREDNAME
     func(METHODNAME/ARITY) is FUNCNAME

The PREDNAME or FUNCNAME must name a function or predicate of the
specified arity whose type, modes, determinism, and purity are at least
as permissive as the declared type, modes, determinism, and purity of
the class method with the specified METHODNAME and ARITY, after the
types of the arguments in the instance declaration have been
substituted in place of the parameters in the type class declaration.

   The second way of defining methods is by listing the clauses for the
definition inside the instance declaration.  A METHODDEFINITION can be
a clause.  These clauses are just like the clauses used to define
ordinary predicates or functions (*note Items::), and so they can be
facts, rules, or DCG rules.  The only difference is that in instance
declarations, clauses are separated by commas rather than being
terminated by periods, and so rules and DCG rules in instance
declarations must normally be enclosed in parentheses.  As with
ordinary predicates, you can have more than one clause for each method.
The clauses must satisfy the declared type, modes, determinism and
purity for the method, after the types of the arguments in the instance
declaration have been substituted in place of the parameters in the
type class declaration.

   These two ways are mutually exclusive: each method must be defined
either by a single naming definition (using the `pred(...) is PREDNAME'
or `func(...) is FUNCNAME' form), or by a set of one or more clauses,
but not both.

   Here's an example of an instance declaration and the different kinds
of method definitions that it can contain:

     :- typeclass foo(T) where [
     	func method1(T, T) = int,
     	func method2(T) = int,
     	pred method3(T::in, int::out) is det,
     	pred method4(T::in, io.state::di, io.state::uo) is det,
     	func method5(bool, T) = T
     ].

     :- instance foo(int) where [
     	% method defined by naming the implementation
     	func(method1/2) is (+),

     	% method defined by a fact
     	method2(X) = X + 1,

     	% method defined by a rule
     	(method3(X, Y) :- Y = X + 2),

     	% method defined by a DCG rule
     	(method4(X) --> io.print(X), io.nl),

     	% method defined by multiple clauses
     	method5(no, _) = 0,
     	(method5(yes, X) = Y :- X + Y = 0)
     ].

   Each `instance' declaration must define an implementation for every
method declared in the corresponding `typeclass' declaration.  It is an
error to define more than one implementation for the same method within
a single `instance' declaration.

   Any call to a method must have argument types (and in the case of
functions, return type) which are constrained to be a member of that
method's type class, or which match one of the instance declarations
visible at the point of the call.  A method call will invoke the
predicate or function specified for that method in the instance
declaration that matches the types of the arguments to the call.

   Note that even if a type class has no methods, an explicit instance
declaration is required for a type to be considered an instance of that
type class.

   Here's an example of some code using an instance declaration:

     :- type coordinate
             ---> coordinate(
                     float,           % X coordinate
                     float            % Y coordinate
             ).

     :- instance point(coordinate) where [
             pred(coords/3) is coordinate_coords,
             func(translate/3) is coordinate_translate
     ].


     :- pred coordinate_coords(coordinate, float, float).
     :- mode coordinate_coords(in, out, out) is det.

     coordinate_coords(coordinate(X, Y), X, Y).

     :- func coordinate_translate(coordinate, float, float) = coordinate.

     coordinate_translate(coordinate(X, Y), Dx, Dy) = coordinate(X + Dx, Y + Dy).

   We have now made the `coordinate' type an instance of the `point'
type class.  If we introduce a new type, `coloured_coordinate' which
represents a point in two dimensional space with a colour associated
with it, it can also become an instance of the type class:

     :- type rgb
             ---> rgb(
                     int,
                     int,
                     int
             ).

     :- type coloured_coordinate
             ---> coloured_coordinate(
                     float,
                     float,
                     rgb
             ).

     :- instance point(coloured_coordinate) where [
             pred(coords/3) is coloured_coordinate_coords,
             func(translate/3) is coloured_coordinate_translate
     ].


     :- pred coloured_coordinate_coords(coloured_coordinate, float, float).
     :- mode coloured_coordinate_coords(in, out, out) is det.

     coloured_coordinate_coords(coloured_coordinate(X, Y, _), X, Y).

     :- func coloured_coordinate_translate(coloured_coordinate, float, float)
             = coloured_coordinate.

     coloured_coordinate_translate(coloured_coordinate(X, Y, Colour), Dx, Dy)
             = coloured_coordinate(X + Dx, Y + Dy, Colour).

   If we call `translate/3' with the first argument having type
`coloured_coordinate', this will invoke `coloured_coordinate_translate'.
Likewise, if we call `translate/3' with the first argument having type
`coordinate', this will invoke `coordinate_translate'.

   Further instances of the type class could be made, e.g. a type that
represents the point using polar coordinates.


File: mercury_ref.info,  Node: Abstract typeclass declarations,  Next: Abstract instance declarations,  Prev: Instance declarations,  Up: Type classes

10.3 Abstract typeclass declarations
====================================

Abstract typeclass declarations are typeclass declarations whose
definitions are hidden.  An abstract typeclass declaration has the same
form as a typeclass declaration, but without the `where[...]' part.  An
abstract typeclass declaration defines a name for a set of (sequences
of) types, but does not define what methods must be implemented for
instances of the type class.

   Like abstract type declarations, abstract typeclass declarations are
only useful in the interface section of a module.  Each abstract
typeclass declaration must be accompanied by a corresponding
non-abstract typeclass declaration that defines the methods for that
type class.

   Non-abstract instance declarations can only be made in scopes where
the non-abstract typeclass declaration is visible.


File: mercury_ref.info,  Node: Abstract instance declarations,  Next: Type class constraints on predicates and functions,  Prev: Abstract typeclass declarations,  Up: Type classes

10.4 Abstract instance declarations
===================================

Abstract instance declarations are instance declarations whose
implementations are hidden.  An abstract instance declaration has the
same form as an instance declaration, but without the `where [...]'
part.  An abstract instance declaration declares that a sequence of
types is an instance of a particular type class without defining how
the type class methods are implemented for those types.  Like abstract
type declarations, abstract instance declarations are only useful in
the interface section of a module.  Each abstract instance declaration
must be accompanied by a corresponding non-abstract instance declaration
that defines how the type class methods are implemented.

   Here's an example:

     :- module hashable.
     :- interface.
     :- import_module int, string.

     :- typeclass hashable(T) where [func hash(T) = int].
     :- instance hashable(int).
     :- instance hashable(string).

     :- implementation.

     :- instance hashable(int) where [func(hash/1) is hash_int].
     :- instance hashable(string) where [func(hash/1) is hash_string].

     :- func hash_int(int) = int.
     hash_int(X) = X.

     :- func hash_string(string) = int.
     hash_string(S) = H :-
             % use the standard library predicate string.hash/2
             string.hash(S, H).

     :- end_module hashable.


File: mercury_ref.info,  Node: Type class constraints on predicates and functions,  Next: Type class constraints on type class declarations,  Prev: Abstract instance declarations,  Up: Type classes

10.5 Type class constraints on predicates and functions
=======================================================

Mercury allows a type class constraint to appear as part of a predicate
or function's type signature.  This constrains the values that can be
taken by type variables in the signature to belong to particular type
classes.

   A type class constraint has the form:

             <= TYPECLASS(TYPE, ...), ...

where TYPECLASS is the name of a type class and TYPE is a type.  Any
variable that appears in TYPE must be determined by the predicate's or
function's type signature.  A variable is determined by a type
signature if it appears in the type signature, but if functional
dependencies are present then it may also be determined from other
variables (*note Functional dependencies::).  Each type class
constraint in a predicate or function declaration must contain at least
one variable.

   For example

     :- pred distance(P1, P2, float) <= (point(P1), point(P2)).
     :- mode distance(in, in, out) is det.

     distance(A, B, Distance) :-
             coords(A, Xa, Ya),
             coords(B, Xb, Yb),
             XDist = Xa - Xb,
             YDist = Ya - Yb,
             Distance = sqrt(XDist*XDist + YDist*YDist).

   In the above example, the `distance' predicate is able to calculate
the distance between any two points, regardless of their
representation, as long as the `coords' operation has been defined.
These constraints are checked at compile time.


File: mercury_ref.info,  Node: Type class constraints on type class declarations,  Next: Type class constraints on instance declarations,  Prev: Type class constraints on predicates and functions,  Up: Type classes

10.6 Type class constraints on type class declarations
======================================================

Type class constraints may also appear in `typeclass' declarations,
meaning that one type class is a "superclass" of another.

   The arguments of a constraint on a type class declaration must be
either type variables or ground types.  Each constraint must contain at
least one variable argument and all variables that appear in the
arguments must also be arguments to the type class in question.

   For example, the following declares the `ring' type class, which
describes types with a particular set of numerical operations defined:

     :- typeclass ring(T) where [
             func zero = (T::out) is det,               % '+' identity
             func one = (T::out) is det,                % '*' identity
             func plus(T::in, T::in) = (T::out) is det, % '+'/2 (forward mode)
             func mult(T::in, T::in) = (T::out) is det, % '*'/2 (forward mode)
             func negative(T::in) = (T::out) is det     % '-'/1 (forward mode)
     ].

   We can now add the following declaration:

     :- typeclass euclidean(T) <= ring(T) where [
             func div(T::in, T::in) = (T::out) is det,
             func mod(T::in, T::in) = (T::out) is det
     ].

   This introduces a new type class, `euclidean', of which `ring' is a
superclass.  The operations defined by the `euclidean' type class are
`div', `mod', as well as all those defined by the `ring' type class.
Any type declared to be an instance of `euclidean' must also be
declared to be an instance of `ring'.

   Typeclass constraints on type class declarations gives rise to a
superclass relation.  This relation must be acyclic.  That is, it is an
error if a type class is its own (direct or indirect) superclass.


File: mercury_ref.info,  Node: Type class constraints on instance declarations,  Next: Functional dependencies,  Prev: Type class constraints on type class declarations,  Up: Type classes

10.7 Type class constraints on instance declarations
====================================================

Typeclass constraints may also be placed upon instance declarations.
The arguments of such constraints must be either type variables or
ground types.  Each constraint must contain at least one variable
argument and all variables that appear in the arguments must be type
variables that appear in the types in the instance declaration.

   For example, consider the following declaration of a type class of
types that may be printed:

     :- typeclass portrayable(T) where [
             pred portray(T::in, io.state::di, io.state::uo) is det
     ].

   The programmer could declare instances such as

     :- instance portrayable(int) where [
             pred(portray/3) is io.write_int
     ].

     :- instance portrayable(char) where [
             pred(portray/3) is io.write_char
     ].

   However, when it comes to writing the instance declaration for a
type such as `list(T)', we want to be able print out the list elements
using the `portray/3' for the particular type of the list elements.
This can be achieved by placing a type class constraint on the
`instance' declaration, as in the following example:

     :- instance portrayable(list(T)) <= portrayable(T) where [
             pred(portray/3) is portray_list
     ].

     :- pred portray_list(list(T), io.state, io.state) <= portrayable(T).
     :- mode portray_list(in, di, uo) is det.

     portray_list([], !IO).
     portray_list([X | Xs], !IO) :-
     	portray(X, !IO),
     	io.write_char(' ', !IO),
     	portray_list(Xs, !IO).

   For abstract instance declarations, the type class constraints on an
abstract instance declaration must exactly match the type class
constraints on the corresponding non-abstract instance declaration that
defines that instance.


File: mercury_ref.info,  Node: Functional dependencies,  Prev: Type class constraints on instance declarations,  Up: Type classes

10.8 Functional dependencies
============================

Type class constraints may include any number of functional
dependencies.  A functional dependency constraint takes the form
`(DOMAIN -> RANGE)'.  The DOMAIN and RANGE arguments are either single
type variables, or conjunctions of type variables separated by commas.

     	:- typeclass TYPECLASS(VAR, ...) <= ((D -> R), ...) ...

     	:- typeclass TYPECLASS(VAR, ...) <= (D1, D2, ... -> R1, R2, ...), ...

   Each type variable must appear in the parameter list of the
typeclass.  Abstract typeclass declarations must have exactly the same
functional dependencies as in the implementation.

   Mutually recursive functional dependencies are allowed, so the
following examples are legal:

     	:- typeclass foo(A, B) <= ((A -> B), (B -> A)).
     	:- typeclass bar(A, B, C, D) <= ((A, B -> C), (B, C -> D), (D -> A, C)).

   A functional dependency on a typeclass places an additional
requirement on the set of instances which are allowed for that type
class.  The requirement is that all types bound to variables in the
range of the functional dependency must be able to be uniquely
determined by the types bound to variables in the domain of the
functional dependency.  If more than one functional dependency is
present, then the requirement for each one must be satisfied.

   For example, given the typeclass declaration

     	:- typeclass baz(A, B) <= (A -> B) where ...

it would be illegal to have both of the instances

     	:- instance baz(int, int) where ...
     	:- instance baz(int, string) where ...

although either one would be acceptable on its own.

   The following instance would also be illegal

     	:- instance baz(string, list(T)) where ...

since the variable `T' may not always be bound to the same type.
However, the instance

     	:- instance baz(list(S), list(T)) <= baz(S, T) where ...

   is legal because the `baz(S, T)' constraint ensures that whatever
`T' is bound to, it is always uniquely determined from the binding of
`S'.

   The extra requirements that result from the use of functional
dependencies allow the bindings of some variables to be determined from
the bindings of others.  This in turn relaxes some of the requirements
of typeclass constraints on predicate and function signatures, and on
existentially typed data constructors.

   Without any functional dependencies, all variables in constraints
must appear in the signature of the predicate or function being
declared.  However, variables which are in the range of a functional
dependency need not appear in the signature, since it is known that
their bindings will be determined from the bindings of the variables in
the domain.

   More formally, the constraints on a predicate or function signature
_induce_ a set of functional dependencies on the variables appearing in
those constraints.  A functional dependency `(A1, ... -> B1, ...)' is
induced from a constraint `TYPECLASS(TYPE1, ...)' if and only if the
typeclass `TYPECLASS' has a functional dependency `(D1, ... -> R1,
...)', and for each typeclass parameter `Di' there exists an `Aj' every
type variable appearing in the `TYPEK' corresponding to `Di', and each
`Bi' appears in the `TYPEJ' bound to the typeclass parameter `Rk' for
some K.

   For example, with the definition of `baz' above, the constraint
`baz(map(X, Y), list(Z))' induces the constraint `(X, Y -> Z)', since X
and Y appear in the domain argument, and Z appears in the range
argument.

   The set of type variables determined from a signature is the
_closure_ of the set appearing in the signature under the functional
dependencies induced from the constraints.  The closure is defined as
the smallest set of variables which includes all of the variables
appearing in the signature, and is such that, for each induced
functional dependency `DOMAIN -> RANGE', if the closure includes all of
the variables in DOMAIN then it includes all of the variables in RANGE.

   For example, the declaration

     	:- pred p(X, Y) <= baz(map(X, Y), list(Z)).

is acceptable since the closure of {X, Y} under the induced functional
dependency must include Z.  Moreover, the typeclass `baz/2' would be
allowed to have a method that only uses the first parameter, A, since
the second parameter, B, would always be determined from the first.

   Note that, since all instances must satisfy the superclass
constraints, the restrictions on instances obviously transfer from
superclass to subclass.  Again, this allows the requirements of
typeclass constraints to be relaxed.  Thus, the functional dependencies
on the ancestors of constraints also induce functional dependencies on
the variables, and the closure that we calculate takes these into
account.

   For example, in this code

     	:- typeclass quux(P, Q, R) <= baz(R, P) where ...

     	:- pred q(Q, R) <= quux(P, Q, R).
   the signature of `q/2' is acceptable since the superclass constraint
on `quux/2' induces the dependency `R -> P' on the type variables,
hence P is in the closure of {Q, R}.

   The presence of functional dependencies also allows "improvement" to
occur during type inference.  This can occur in two ways.  First, if
two constraints of a given class match on all of the domain arguments
of a functional dependency on that class, then it can be inferred that
they also match on the range arguments.  For example, given the
constraints `baz(A, B1)' and `baz(A, B2)', it will be inferred that `B1
= B2'.

   Similarly, if a constraint of a given class is subsumed by a known
instance of that class in the domain arguments, then its range
arguments can be unified with the corresponding instance range
arguments.  For example, given the instance:

     	:- instance baz(list(T), string) where ...

then the constraint `baz(list(int), X)' can be improved with the
inference that `X = string'.


File: mercury_ref.info,  Node: Existential types,  Next: Exception handling,  Prev: Type classes,  Up: Top

11 Existential types
********************

Existentially quantified type variables (or simply "existential types"
for short) are useful tools for data abstraction.  In combination with
type classes, they allow you to write code in an "object oriented"
style that is similar to the use of interfaces in Java or abstract base
classes in C++.

   Mercury supports existential type quantifiers on predicate and
function declarations, and in data type definitions.  You can put type
class constraints on existentially quantified type variables.

* Menu:

* Existentially typed predicates and functions::
* Existential class constraints::
* Existentially typed data types::
* Some idioms using existentially quantified types::


File: mercury_ref.info,  Node: Existentially typed predicates and functions,  Next: Existential class constraints,  Up: Existential types

11.1 Existentially typed predicates and functions
=================================================

* Menu:

* Syntax for explicit type quantifiers::
* Semantics of type quantifiers::
* Examples of correct code using type quantifiers::
* Examples of incorrect code using type quantifiers::


File: mercury_ref.info,  Node: Syntax for explicit type quantifiers,  Next: Semantics of type quantifiers,  Up: Existentially typed predicates and functions

11.1.1 Syntax for explicit type quantifiers
-------------------------------------------

Type variables in type declarations for polymorphic predicates or
functions are normally universally quantified.  However, it is also
possible to existentially quantify such type variables, by using an
explicit existential quantifier of the form `some VARS' before the
`pred' or `func' declaration, where VARS is a list of variables.

   For example:

     % Here the type variables `T' is existentially quantified
     :- some [T] pred foo(T).

     % Here the type variables `T1' and `T2' are existentially quantified.
     :- some [T1, T2] func bar(int, list(T1), set(T2)) = pair(T1, T2).

     % Here the type variable `T2' is existentially quantified,
     % but the type variables `T1' and `T3' are universally quantified.
     :- some [T2] pred foo(T1, T2, T3).

   Explicit universal quantifiers, of the form `all VARS', are also
permitted on `pred' and `func' declarations, although they are not
necessary, since universal quantification is the default.  (If both
universal and existential quantifiers are present, the universal
quantifiers must precede the existential quantifiers.)  For example:

     % Here the type variable `T2' is existentially quantified,
     % but the type variables `T1' and `T3' are universally quantified.
     :- all [T3] some [T2] pred foo(T1, T2, T3).


File: mercury_ref.info,  Node: Semantics of type quantifiers,  Next: Examples of correct code using type quantifiers,  Prev: Syntax for explicit type quantifiers,  Up: Existentially typed predicates and functions

11.1.2 Semantics of type quantifiers
------------------------------------

If a type variable in the type declaration for a polymorphic predicate
or function is universally quantified, this means the caller will
determine the value of the type variable, and the callee must be defined
so that it will work for _all_ types which are an instance of its
declared type.

   For an existentially quantified type variable, the situation is the
converse: the _callee_ must determine the value of the type variable,
and all _callers_ must be defined so as to work for all types which are
an instance of the called procedure's declared type.

   When type checking a predicate or function, if a variable has a type
that occurs as a universally quantified type variable in the predicate
or function declaration, or a type that occurs as an existentially
quantified type variable in the declaration of one of the predicates or
functions that it calls, then its type is treated as an opaque type.
This means that there are very few things which it is legal to do with
such a variable -- basically you can only pass it to another procedure
expecting the same type, unify it with another value of the same type,
put it in a polymorphic data structure, or pass it to a polymorphic
procedure whose argument type is universally quantified.  (Note,
however, that the standard library includes some quite powerful
procedures such as `io.write' which can be useful in this context.)

   A non-variable type (i.e. a type that is not a type variable) is
considered _more general_ than an existentially quantified type
variable.  Type inference will therefore never infer an existentially
quantified type for a predicate or function unless that predicate or
function calls (directly or indirectly) a predicate or function which
was explicitly declared to have an existentially quantified type.

   Note that an existentially typed procedure is not allowed to have
different types for its existentially typed arguments in different
clauses (even mode-specific clauses) or in different subgoals of a
single clause; however, the same effect can be achieved in other ways
(*note Some idioms using existentially quantified types::).

   For procedures involving calls to existentially-typed predicates or
functions, the compiler's mode analysis must take account of the modes
for type variables in all polymorphic calls.  Universally quantified
type variables have mode `in', whereas existentially quantified type
variables have mode `out'.  As usual, the compiler's mode analysis will
attempt to reorder the elements of conjunctions in order to satisfy the
modes.


File: mercury_ref.info,  Node: Examples of correct code using type quantifiers,  Next: Examples of incorrect code using type quantifiers,  Prev: Semantics of type quantifiers,  Up: Existentially typed predicates and functions

11.1.3 Examples of correct code using type quantifiers
------------------------------------------------------

Here are some examples of type-correct code using universal and
existential types.

     /* simple examples */

     :- pred foo(T).
     foo(_).
     	% ok

     :- pred call_foo.
     call_foo :- foo(42).
     	% ok (T = int)

     :- some [T] pred e_foo(T).
     e_foo(X) :- X = 42.
     	% ok (T = int)

     :- pred call_e_foo.
     call_e_foo :- e_foo(_).
     	% ok

     /* examples using higher-order functions */

     :- func bar(T, T, func(T) = int) = int.
     bar(X, Y, F) = F(X) + F(Y).
     	% ok

     :- func call_bar = int.
     call_bar = bar(2, 3, (func(X) = X*X)).
     	% ok (T = int)
     	% returns 13 (= 2*2 + 3*3)

     :- some [T] pred e_bar(T, T, func(T) = int).
     :-          mode e_bar(out, out, out(func(in) = out is det)).
     e_bar(2, 3, (func(X) = X * X)).
     	% ok (T = int)

     :- func call_e_bar = int.
     call_e_bar = F(X) + F(Y) :- e_bar(X, Y, F).
     	% ok
     	% returns 13 (= 2*2 + 3*3)


File: mercury_ref.info,  Node: Examples of incorrect code using type quantifiers,  Prev: Examples of correct code using type quantifiers,  Up: Existentially typed predicates and functions

11.1.4 Examples of incorrect code using type quantifiers
--------------------------------------------------------

Here are some examples of code using universal and existential types
that contains type errors.

     /* simple examples */

     :- pred bad_foo(T).
     bad_foo(42).
     	% type error

     :- some [T] pred e_foo(T).
     e_foo(42).
     	% ok

     :- pred bad_call_e_foo.
     bad_call_e_foo :- e_foo(42).
     	% type error

     :- some [T] pred e_bar1(T).
     e_bar1(42).
     e_bar1(42).
     e_bar1(43).
     	% ok (T = int)

     :- some [T] pred bad_e_bar2(T).
     bad_e_bar2(42).
     bad_e_bar2("blah").
     	% type error (cannot unify types `int' and `string')

     :- some [T] pred bad_e_bar3(T).
     bad_e_bar3(X) :- e_foo(X).
     bad_e_bar3(X) :- e_foo(X).
     	% type error (attempt to bind type variable `T' twice)


File: mercury_ref.info,  Node: Existential class constraints,  Next: Existentially typed data types,  Prev: Existentially typed predicates and functions,  Up: Existential types

11.2 Existential class constraints
==================================

Existentially quantified type variables are especially useful in
combination with type class constraints.

   Type class constraints can be either universal or existential.
Universal type class constraints are written using `<=', as described
in *note Type class constraints on predicates and functions::; they
signify a constraint that the _caller_ must satisfy.  Existential type
class constraints are written in the same syntax as universal
constraints, but using `=>' instead of `<='; they signify a constraint
that the _callee_ must satisfy.  (If a declaration has both universal
and existential constraints, then the existential constraints must
precede the universal constraints.)

   For example:

     % Here `c1(T2)' and `c2(T2)' are existential constraints,
     % and `c3(T1)' is a universal constraint,
     :- all [T1] some [T2] ((pred p(T1, T2) => (c1(T2), c2(T2))) <= c3(T1)).

   Existential constraints must only constrain type variables that are
explicitly existentially quantified.  Likewise, universal constraints
must only constrain type variables that are universally quantified,
although in this case the quantification does not have to be explicit
because universal quantification is the default (see *note Syntax for
explicit type quantifiers::).


File: mercury_ref.info,  Node: Existentially typed data types,  Next: Some idioms using existentially quantified types,  Prev: Existential class constraints,  Up: Existential types

11.3 Existentially typed data types
===================================

Type variables occurring in the body of a discriminated union type
definition may be existentially quantified.  Constructor definitions
within discriminated union type definitions may be preceded by an
existential type quantifier and followed by one or more existential
type class constraints.

   For example:

     % A simple heterogeneous list type
     :- type list_of_any
     	---> nil_any
     	;    some [T] cons_any(T, list_of_any).

     % A heterogeneous list type with a type class constraint
     :- typeclass showable(T) where [ func show(T) = string ].
     :- type showable_list
     	---> nil
     	;    some [T] (cons(T, showable_list) => showable(T)).

     % A different way of doing the same kind of thing, this
     % time using the standard type list(T).
     :- type showable ---> some [T] (s(T) => showable(T)).
     :- type list_of_showable == list(showable).

     % Here's an arbitrary example involving multiple
     % type variables and multiple constraints
     :- typeclass foo(T1, T2) where [ /* ... */ ].
     :- type bar(T)
     	---> f1
     	;    f2(T)
     	;    some [T]
     	     f4(T)
     	;    some [T1, T2]
     	     (f4(T1, T2, T) => showable(T1), showable(T2))
     	;    some [T1, T2]
     	     (f5(list(T1), T2) => fooable(T1, list(T2)))
     	.

   Construction and deconstruction of existentially quantified data
types are inverses: when constructing a value of an existentially
quantified data type, the "existentially quantified" functor acts for
purposes of type checking like a universally quantified function: the
caller will determine the values of the type variables.  Conversely,
for deconstruction the functor acts like an existentially quantified
function: the caller must be defined so as to work for all possible
values of the existentially quantified type variables which satisfy the
declared type class constraints.

   In order to make this distinction clear to the compiler, whenever
you want to construct a value using an existentially quantified
functor, you must prepend `new ' onto the functor name.  This tells the
compiler to treat it as though it were universally quantified: the
caller can bind that functor's existentially quantified type variables
to any type which satisfies the declared type class constraints.
Conversely, any occurrence without the `new ' prefix must be a
deconstruction, and is therefore existentially quantified: the caller
must not bind the existentially quantified type variables, but the
caller is allowed to depend on those type variables satisfying the
declared type class constraints, if any.

   For example, the function `make_list' constructs a value of type
`list_of_showable' containing a sequence of values of different types,
all of which are instances of the `showable' class

     :- instance showable(int).
     :- instance showable(float).
     :- instance showable(string).

     :- func make_list = showable_list.
     make_list = List :-
     	Int = 42,
     	Float = 1.0,
     	String = "blah",
     	List =  'new cons'(Int,
     		'new cons'(Float,
     		'new cons'(String, nil))).

while the function `process_list' below applies the `show' method of
the `showable' class to the values in such a list.

     :- func process_list(list_of_showable) = list(string).
     process_list(nil) = "".
     process_list(cons(Head, Tail)) = [show(Head) | process_list(Tail)].


File: mercury_ref.info,  Node: Some idioms using existentially quantified types,  Prev: Existentially typed data types,  Up: Existential types

11.4 Some idioms using existentially quantified types
=====================================================

The standard library module `univ' provides an abstract type named
`univ' which can hold values of any type.  You can form heterogeneous
containers (containers that can hold values of different types at the
same time) by using data structures that contain `univ's, e.g.
`list(univ)'.

   The interface to `univ' includes the following:

     % `univ' is a type which can hold any value.
     :- type univ.

     % The function univ/1 takes a value of any type and constructs
     % a `univ' containing that value (the type will be stored along
     % with the value)
     :- func univ(T) = univ.

     % The function univ_value/1 takes a `univ' argument and extracts
     % the value contained in the `univ' (together with its type).
     % This is the inverse of the function univ/1.
     :- some [T] func univ_value(univ) = T.

   The `univ' type in the standard library is in fact a simple example
of an existentially typed data type.  It could be implemented as
follows:

     :- implementation.
     :- type univ ---> some [T] mkuniv(T).
     univ(X) = 'new mkuniv'(X).
     univ_value(mkuniv(X)) = X.

   An existentially typed procedure is not allowed to have different
types for its existentially typed arguments in different clauses or in
different subgoals of a single clause.  For instance, both of the
following examples are illegal:

     :- some [T] pred bad_example(string, T).
     bad_example("foo", 42).
     bad_example("bar", "blah").
     	% type error (cannot unify `int' and `string')

     :- some [T] pred bad_example2(string, T).
     bad_example2(Name, Value) :-
     	( Name = "foo", Value = 42
     	; Name = "bar", Value = "blah"
     	).
     	% type error (cannot unify `int' and `string')

   However, using `univ', it is possible for an existentially typed
function to return values of different types at each invocation.

     :- some [T] pred good_example(string, T).
     good_example(Name, univ_value(Univ)) :-
     	( Name = "foo", Univ = univ(42)
     	; Name = "bar", Univ = univ("blah")
     	).

   Using `univ' doesn't work if you also want to use type class
constraints.  If you want to use type class constraints, then you must
define your own existentially typed data type, analogous to `univ', and
use that:

     :- type univ_showable ---> some [T] (mkshowable(T) => showable(T)).

     :- some [T] pred harder_example(string, T) => showable(T).
     harder_example(Name, Showable) :-
     	( Name = "bar", Univ = 'new mkshowable'(42)
     	; Name = "bar", Univ = 'new mkshowable'("blah")
     	),
     	Univ = mkshowable(Showable).

   The issue can also arise for mode-specific clauses (*note Different
clauses for different modes::).  For instance, the following example is
illegal:

     :- some [T] pred bad_example3(string, T).
     :-          mode bad_example3(in(bound("foo")), out) is det.
     :-          mode bad_example3(in(bound("bar")), out) is det.
     :- pragma promise_pure(bad_example3/2).
     bad_example3("foo"::in(bound("foo")), 42::out).
     bad_example3("bar"::in(bound("bar")), "blah"::out).
     	% type error (cannot unify `int' and `string')

   The solution is similar, although in this case an intermediate
predicate is required:

     :- some [T] pred good_example3(string, T).
     :-          mode good_example3(in(bound("foo")), out) is det.
     :-          mode good_example3(in(bound("bar")), out) is det.
     good_example3(Name, univ_value(Univ)) :-
     	good_example3_univ(Name, Univ).

     :- pred good_example3_univ(string, univ).
     :- mode good_example3_univ(in(bound("foo")), out) is det.
     :- mode good_example3_univ(in(bound("bar")), out) is det.
     :- pragma promise_pure(good_example3_univ/2).
     good_example3_univ("foo"::in(bound("foo")), univ(42)::out).
     good_example3_univ("bar"::in(bound("bar")), univ("blah")::out).


File: mercury_ref.info,  Node: Exception handling,  Next: Semantics,  Prev: Existential types,  Up: Top

12 Exception handling
*********************

Mercury procedures may throw exceptions.  Exceptions may be caught using
the predicates defined in the `exception' library module, or using try
goals.

A `try' goal has the following form:

             try PARAMS GOAL
             then THENGOAL
             else ELSEGOAL
             catch TERM -> CATCHGOAL
             ...
             catch_any CATCHANYVAR -> CATCHANYGOAL

   GOAL, THENGOAL, ELSEGOAL, CATCHGOAL, CATCHANYGOAL must be valid
goals.

   GOAL must have one of the following determinisms: `det', `semidet',
`cc_multi', or `cc_nondet'.

   The non-local variables of GOAL must not have an inst equivalent to
`unique' or `mostly_unique' or `any', unless they have the type
`io.state'.

   PARAMS must be a valid list of zero or more try parameters.

   The "then" part is mandatory.  The "else" part is mandatory if GOAL
may fail; otherwise it must be omitted.  There may be zero or more
"catch" branches.  The "catch_any" part is optional.  CATCHANYVAR must
be a single variable.

   The try parameter `io' takes a single argument, which must be the
name of a state variable prefixed by `!'; for example, `io(!IO)'.  The
state variable must have the type `io.state', and be in scope of the
try goal.  The state variable is threaded through `Goal', so it may
perform I/O but cannot fail.  If no `io' parameter exists, `Goal' may
not perform I/O and may fail.

   A try goal has determinism `cc_multi'.

   On entering a try goal, GOAL is executed.  If it succeeds without
throwing an exception, THENGOAL is executed.  Any variables bound by
GOAL are visible in THENGOAL only.  If GOAL fails, then ELSEGOAL is
executed.

   If GOAL throws an exception, the exception value is unified with
each of the TERMs in the "catch" branches in turn.  On the first
successful unification, the corresponding CATCHGOAL is executed (and
other "catch" and "catch_any" branches ignored).  Variables bound
during the unification of the TERM are in scope of the corresponding
CATCHGOAL.

   If the exception value does not unify with any of the terms in
"catch" branches, and a "catch_any" branch is present, the exception is
bound to CATCHANYVAR and the CATCHANYGOAL executed.  CATCHANYVAR is
visible in the CATCHANYGOAL only, and is existentially typed, i.e. it
has type `some [T] T'.

   Finally, if the thrown value did not unify with any "catch" term,
and there is no "catch_any" branch, the exception is rethrown.

The declarative semantics of a try goal is:

             (try [] Goal
              then Then
              else Else
              catch CP1 -> CG1
              catch CG2 -> CG2
              ...
              catch_any CAV -> CAG
             )  <=>
                     (
                             Goal, Then
                     ;
                             not Goal, Else
                     ;
                             some [Excp]
                             ( Excp = CP1 -> CG1
                             ; Excp = CP2 -> CG2
                             ; ...
                             ; Excp = CAV, CAG
                             )
                     ).

   If no `else' branch is present, let `Else = fail'.  If no
`catch_any' branch is present, let `CAG = fail'.

An example of a try goal that performs I/O is:

     :- pred p_carefully(io::di, io::uo) is cc_multi.

     p_carefully(!IO) :-
             (try [io(!IO)] (
                     io.write_string("Calling p\n", !IO),
                     p(Output, !IO)
             )
             then
                     io.write_string("p returned: ", !IO),
                     io.write(Output, !IO),
                     io.nl(!IO)
             catch S ->
                     io.write_string("p threw a string: ", !IO),
                     io.write_string(S, !IO),
                     io.nl(!IO)
             catch 42 ->
                     io.write_string("p threw 42\n", !IO)
             catch_any Other ->
                     io.write_string("p threw something: ", !IO),
                     io.write(Other, !IO),
                     % Rethrow the value.
                     throw(Other)
             ).


File: mercury_ref.info,  Node: Semantics,  Next: Foreign language interface,  Prev: Exception handling,  Up: Top

13 Semantics
************

A legal Mercury program is one that complies with the syntax, type,
mode, determinism, and module system rules specified in earlier
chapters.  If a program does not comply with those rules, the compiler
must report an error.

   For each legal Mercury program, there is an associated predicate
calculus theory whose language is specified by the type declarations in
the program and whose axioms are the completion of the clauses for all
predicates in the program, plus the usual equality axioms extended with
the completion of the equations for all functions in the program, plus
axioms corresponding to the mode-determinism assertions (*note
Determinism::), plus axioms specifying the semantics of library
predicates and functions.  The declarative semantics of a legal Mercury
program is specified by this theory.

   Mercury implementations must be sound: the answers they compute must
be true in every model of the theory.  Mercury implementations are not
required to be complete: they may fail to compute an answer in finite
time, or they may exhaust the resource limitations of the execution
environment, even though an answer is provable in the theory.  However,
there are certain minimum requirements that they must satisfy with
respect to completeness.

   There is an operational semantics of Mercury programs called the
"strict sequential" operational semantics.  In this semantics, the
program is executed top-down, starting from `main/2' preceded by any
module initialisation goals (as per *note Module initialisation::),
followed by any module finalisation goals (as per *note Module
finalisation::), and function calls within a goal, conjunctions and
disjunctions are all executed in depth-first left-to-right order.
Conjunctions and function calls are "minimally" reordered as required
by the modes: the order is determined by selecting the first
mode-correct sub-goal (conjunct or function call), executing that, then
selecting the first of the remaining sub-goals which is now
mode-correct, executing that, and so on.  (There is no interleaving of
different individual conjuncts or function calls, however; the
sub-goals are reordered, not split and interleaved.)  Function
application is strict, not lazy.

   Mercury implementations are required to provide a method of
processing Mercury programs which is equivalent to the strict sequential
operational semantics.

   There is another operational semantics of Mercury programs called
the "strict commutative" operational semantics.  This semantics is
equivalent to the strict sequential operational semantics except that
there is no requirement that function calls, conjunctions and
disjunctions be executed left-to-right; they may be executed in any
order, and may even be interleaved.  Furthermore, the order may even be
different each time a particular goal is entered.

   As well as providing the strict sequential operational semantics,
Mercury implementations may optionally provide additional
implementation-defined operational semantics, provided that any such
implementation-defined operational semantics are at least as complete
as the strict commutative operational semantics.  An
implementation-defined semantics is "at least as complete" as the
strict commutative semantics if and only if the implementation-defined
semantics guarantees to compute an answer in finite time for any
program for which an answer would be computed in finite time for all
possible executions under the strict commutative semantics (i.e. for
all possible orderings of conjunctions and disjunctions).

   Thus, to summarize, there are in fact a variety of different
operational semantics for Mercury.  In one of them, the strict
sequential semantics, there is no nondeterminism -- the behaviour is
always specified exactly.  Programs are executed top-down using SLDNF
(or something equivalent), mode analysis does "minimal" reordering (in
a precisely defined sense), function calls, conjunctions and
disjunctions are executed depth-first left-to-right, and function
evaluation is strict.  All implementations are required to support the
strict sequential semantics, so that a program which works on one
implementation using this semantics will be guaranteed to work on any
other implementation.  However, implementations are also allowed to
support other operational semantics, which may have non-determinism, so
long as they are sound with respect to the declarative semantics, and
so long as they meet a minimum level of completeness (they must be at
least as complete as the strict commutative semantics, in the sense
that every program which terminates for all possible orderings must
also terminate in any implementation-defined operational semantics).

   This compromise allows Mercury to be used in several different ways.
Programmers who care more about ease of programming and portability
than about efficiency can use the strict sequential semantics, and can
then be guaranteed that if their program works on one correct
implementation, it will work on all correct implementations.  Compiler
implementors who want to write optimizing implementations that do lots
of clever code reorderings and other high-level transformations or that
want to offer parallelizing implementations which take maximum
advantage of parallelism can define different semantic models.
Programmers who care about efficiency more than portability can write
code for these implementation-defined semantic models.  Programmers who
care about efficiency _and_ portability can achieve this by writing
code for the strict commutative semantics.  Of course, this is not
quite as easy as using the strict sequential semantics, since it is in
general not sufficient to test your programs on just one implementation
if you are to be sure that it will be able to use the maximally
efficient operational semantics on any implementation.  However, if you
do write code which works for all possible executions under the strict
commutative semantics (i.e. for all possible orderings of conjunctions
and disjunctions), then you can be guaranteed that it will work
correctly on every implementation, under every possible
implementation-defined semantics.

   The University of Melbourne Mercury implementation offers eight
different semantics, which can be selected with different combinations
of the `--no-reorder-conj', `--no-reorder-disj', and
`--no-fully-strict' options.  (The `--no-fully-strict' option allows
the compiler to improve completeness by optimizing away infinite loops
and goals with determinism `erroneous'.)  The default semantics are the
strict commutative semantics.  Enabling `--no-reorder-conj' and
`--no-reorder-disj' gives the strict sequential semantics.

   Future implementations of Mercury may wish to offer other
operational semantics.  For example, they may wish to provide semantics
in which function evaluation is lazy, rather than strict; semantics
with a guaranteed fair search rule; and so forth.


File: mercury_ref.info,  Node: Foreign language interface,  Next: Impurity,  Prev: Semantics,  Up: Top

14 Foreign language interface
*****************************

* Menu:

* Calling foreign code from Mercury::  How to implement a Mercury predicate
				       or function as a call to code
				       written in a different
				       programming language.
* Calling Mercury from foreign code::  How to call a Mercury predicate
                                       or function from a different
                                       programming language.
* Using foreign types from Mercury::   How to use a type defined in
				       a different programming language
				       in Mercury code.
* Using Mercury enumerations in foreign code:: How to use an enumeration type
                                               defined in Mercury in a
                                               different programming language.
* Using foreign enumerations in Mercury code:: How to use an enumeration type
                                                defined in a foreign language
                                                in Mercury code.
* Data passing conventions::	       How Mercury types are passed to
				       different languages.
* Adding foreign declarations::        How to add declarations of
  				       entities in other programming
				       languages.
* Adding foreign definitions::         How to add definitions of
  				       entities in other programming
				       languages.
* Language specific bindings::         Information specific to each
  				       foreign language.

   This chapter documents the foreign language interface.


File: mercury_ref.info,  Node: Calling foreign code from Mercury,  Next: Calling Mercury from foreign code,  Up: Foreign language interface

14.1 Calling foreign code from Mercury
======================================

Mercury procedures can be implemented using fragments of foreign
language code using `pragma foreign_proc'.

* Menu:

* pragma foreign_proc::         Defining Mercury procedures using foreign code.
* Foreign code attributes::   	Describing properties of foreign
				functions or code.


File: mercury_ref.info,  Node: pragma foreign_proc,  Next: Foreign code attributes,  Up: Calling foreign code from Mercury

14.1.1 pragma foreign_proc
--------------------------

A declaration of the form

     :- pragma foreign_proc("LANG", PRED(VAR1::MODE1, VAR2::MODE2, ...),
             ATTRIBUTES, FOREIGN_CODE).

or

     :- pragma foreign_proc("LANG", FUNC(VAR1::MODE1, VAR2::MODE2, ...) = (VAR::MODE),
             ATTRIBUTES, FOREIGN_CODE).

means that any calls to the specified mode of PRED or FUNC will result
in execution of the foreign code given in FOREIGN_CODE written in
language LANG, if LANG is selected as the foreign language code by this
implementation.  See the "Foreign Language Interface" chapter of the
Mercury User's Guide, for more information about how the implementation
selects the appropriate `foreign_proc' to use.

   The foreign code fragment may refer to the specified variables
(VAR1, VAR2, ..., and VAR) directly by name.  It is an error for a
variable to occur more than once in the argument list.  These variables
will have foreign language types corresponding to their Mercury types,
as determined by language and implementation specific rules.

   All `foreign_proc' implementations are assumed to be impure.  If
they are actually pure or semipure, they must be explicitly promised as
such by the user (either by using foreign language attributes specified
below, or a promise_pure or promise_semipure pragma as specified in
*note Impurity::).

   Additional restrictions on the foreign language interface code
depend on the foreign language and compilation options.  For more
information, including the list of supported foreign languages and the
strings used to identify them, see the language specific information in
the "Foreign Language Interface" chapter of the Mercury User's Guide.

   If there is a `pragma foreign_proc' declaration for any mode of a
predicate or function, then there must be either a clause or a `pragma
foreign_proc' declaration for every mode of that predicate or function.

   Here's an example of code using `pragma foreign_proc': The following
code defines a Mercury function `sin/1' which calls the C function
`sin()' of the same name.

     :- func sin(float) = float.
     :- pragma foreign_proc("C", sin(X::in) = (Sin::out),
             [may_call_mercury],
             "Sin = sin(X);").

   If the foreign language code does not recursively invoke Mercury
code, as in the above example, then you can use `will_not_call_mercury'
in place of `may_call_mercury' in the declarations above.  This allows
the compiler to use a slightly more efficient calling convention.  (If
you use this form, and the foreign code _does_ invoke Mercury code,
then the behaviour is undefined -- your program may misbehave or crash.)

   If there are both Mercury definitions and foreign_proc definitions
for a procedure and/or foreign_proc definitions for different languages,
it is implementation defined which definition is used.

   For pure and semipure procedures, the declarative semantics of the
foreign_proc definitions must be the same as that of the Mercury code.
The only thing that is allowed to differ is the efficiency (including
the possibility of non-termination) and the order of solutions.

   It is an error for a procedure with a `pragma foreign_proc'
declaration to have a determinism of `multi' or `nondet'.

   Since foreign_procs with the determinism `multi' or `nondet' cannot
be defined directly, procedures with those determinisms that require
foreign code in their implementation must be defined using a
combination of Mercury clauses and (semi)deterministic foreign_procs.
The following implementation for the standard library predicate
`string.append/3' in the mode `append(out, out, in) is multi'
illustrates this technique:

     :- pred append(string, string, string).
     :- mode append(out, out, in) is multi.

     append(S1, S2, S3) :-
         S3Len = string.length(S3),
         append_2(0, S3Len, S1, S2, S3).

     :- pred append_2(int::in, int::in, string::out, string::out, string::in) is multi.

     append_2(NextS1Len, S3Len, S1, S2, S3) :-
         ( NextS1Len = S3Len ->
             append_3(NextS1Len, S3Len, S1, S2, S3)
         ;
             (
                 append_3(NextS1Len, S3Len, S1, S2, S3)
             ;
                 append_2(NextS1Len + 1, S3Len, S1, S2, S3)
             )
         ).

     :- pred append_3(int::inb, int::in, string::out, string::out, string::in) is det.

     :- pragma foreign_proc("C",
         append_3(S1Len::in, S3Len::in, S1::out, S2::out, S3::in),
         [will_not_call_mercury, promise_pure],
     "
         S1 = allocate_string(S1Len);   /* Allocate a new string of length S1Len */
         memcpy(S1, S3, S1Len);
         S1[S1Len] = '\\0';
         S2 = allocate_string(S2, S3Len - S1Len);
         strcpy(S2, S3Len + S1Len);
     ").


File: mercury_ref.info,  Node: Foreign code attributes,  Prev: pragma foreign_proc,  Up: Calling foreign code from Mercury

14.1.2 Foreign code attributes
------------------------------

As described above, `pragma foreign_proc' declarations may include a
list of attributes describing properties of the given foreign function
or code.  All Mercury implementations must support the attributes
listed below.  They may also support additional attributes.

   The attributes which must be supported by all implementations are as
follows:

`may_call_mercury'/`will_not_call_mercury'
     This attribute declares whether or not execution inside this
     foreign language code may call back into Mercury or not.  The
     default, in case neither is specified, is `may_call_mercury'.
     Specifying `will_not_call_mercury' may allow the compiler to
     generate more efficient code.  If you specify
     `will_not_call_mercury', but the foreign language code _does_
     invoke Mercury code, then the behaviour is undefined.

`promise_pure'/`promise_semipure'
     This attribute promises that the purity of the given predicate or
     function definition is pure or semipure.  It is equivalent to a
     corresponding `pragma promise_pure' or `pragma promise_semipure'
     declaration (*note Impurity::).  If omitted, the clause specified
     by the `foreign_proc' is assumed to be impure.

`thread_safe'/`not_thread_safe'/`maybe_thread_safe'
     This attribute declares whether or not it is safe for multiple
     threads to execute this foreign language code concurrently.  The
     default, in case none is specified, is `not_thread_safe'.  If the
     foreign language code is declared `thread_safe', then the Mercury
     implementation is permitted to execute the code concurrently from
     multiple threads without taking any special precautions.  If the
     foreign language code is declared `not_thread_safe', then the
     Mercury implementation must not invoke the code concurrently from
     multiple threads.  If the Mercury implementation does use
     multithreading, then it must take appropriate steps to prevent
     this.  (The experimental multithreaded version of the current
     University of Melbourne Mercury implementation protects
     `not_thread_safe' code using a mutex: C code that is not
     thread-safe has code inserted around it to obtain and release a
     mutex.  All non-thread-safe foreign language code shares a single
     mutex.)  If the foreign language code is declared
     `maybe_thread_safe' then whether the code is considered
     `thread_safe' or `not_thread_safe' depends upon a compiler flag.
     This attribute is useful when the thread safety of the foreign
     code itself is conditional.  The Melbourne Mercury compiler uses
     the `--maybe-thread-safe' option to set the value of the
     `maybe_thread_safe' attribute.

   Additional attributes which are supported by the Melbourne Mercury
compiler are as follows:

`tabled_for_io'
     This attribute should be attached to foreign procedures that do
     I/O.  It tells the debugger to make calls to the foreign procedure
     idempotent.  This allows the debugger to safely retry across such
     calls and also allows safe declarative debugging of code
     containing such calls.  For more information see the I/O tabling
     section of the Mercury user guide.  If the foreign procedure
     contains gotos or static variables then the `pragma no_inline'
     directive should also be given.  Note that currently I/O tabling
     will only be done for foreign procedures that take a pair of I/O
     state arguments.  Impure foreign procedures that perform I/O will
     not be made idempotent, even if the tabled_for_io attribute is
     present.  Note also that the tabled_for_io attribute will likely
     be replaced in a future release with a more general solution.

`terminates'/`does_not_terminate'
     This attribute specifies the termination properties of the given
     predicate or function definition.  It is equivalent to the
     corresponding `pragma terminates' or `pragma does_not_terminate'
     declaration.  If omitted, the termination property of the
     procedure is determined by the value of the
     `may_call_mercury'/`will_not_call_mercury' attribute.  See *note
     Termination analysis:: for more details.

`max_stack_size(Size)'
     This attribute declares the maximum stack usage of a particular
     piece of code.  The unit that `Size' is measured in depends upon
     foreign language being used.  Currently this attribute is only
     used (and is in fact required) by the `IL' foreign language
     interface, and is measured in units of stack items.

`will_not_throw_exception'
     This attribute promises that the given predicate or function will
     not make calls back to Mercury that may result in an exception
     being thrown.  It is an error to apply this attribute to
     procedures that have determinism erroneous.  This attribute is
     ignored for code that is declared as not making calls back to
     Mercury via the `will_not_call_mercury' attribute.  Note:
     predicates or functions that have polymorphic arguments but do not
     explicitly throw an exception, via a call to exception.throw/1 or
     require.error/1, may still throw exceptions because they may be
     called with arguments whose types have user-defined equality or
     comparison predicates.  If these user-defined equality or
     comparison predicates throw exceptions then unifications or
     comparisons involving these types may also throw exceptions.  As
     such, we recommend that only implementors of the Mercury system
     use this annotation for polymorphic predicates and functions.

`will_not_modify_trail/may_modify_trail'
     This attribute declares whether or not a foreign procedure modifies
     the trail (see *note Trailing::).  Specifying that a foreign
     procedure will not modify the trail may allow the compiler to
     generate more efficient code for that procedure.  In compilation
     grades that do not support trailing this attribute is ignored.
     The default, in case none is specified, is `may_modify_trail'.

`will_not_call_mm_tabled/may_call_mm_tabled'
     This attribute declares whether or not a foreign procedure makes
     calls back to Mercury procedures that are evaluated using minimal
     model tabling (*note Tabled evaluation::).  Specifying that a
     foreign procedure will not call procedures evaluated using minimal
     model tabling may allow the compiler to generate more efficient
     code.  In compilation grades that do not support minimal model
     tabling this attribute is ignored.  These attributes may not be
     used with procedures that do not make calls back to Mercury, i.e.
     that have the `will_not_call_mercury' attribute.  The default for
     foreign procedures that `may_call_mercury', in case none is
     specified, is `may_call_mm_tabled'.

`affects_liveness/does_not_affect_liveness'
     This attribute declares whether or not a foreign procedure uses
     and/or modifies any part of the Mercury virtual machine
     (registers, stack slots) through means other than its arguments.
     The `affects_liveness' attribute says that it does; The
     `does_not_affect_liveness' attribute says that it does not.  In
     the absence of either attribute, the compiler assumes
     `affects_liveness', unless the code of the foreign_proc in
     question is empty.

`may_duplicate/may_not_duplicate'
     This attribute tells the compiler whether it is allowed to
     duplicate the foreign code fragment through optimizations such as
     inlining.  The `may_duplicate' attribute says that it may; The
     `may_not_duplicate' attribute says that it may not.  In the
     absence of either attribute, the compiler is allowed make its own
     judgement in the matter, based on factors such as the size of the
     code fragment.



File: mercury_ref.info,  Node: Calling Mercury from foreign code,  Next: Using foreign types from Mercury,  Prev: Calling foreign code from Mercury,  Up: Foreign language interface

14.2 Calling Mercury from foreign code
======================================

Mercury procedures may be exported so that they can be called by code
written in a foreign language.

   A declaration of the form:

     :- pragma foreign_export("LANG",
             PRED(MODE1, MODE2, ...), "FOREIGNNAME").

or

     :- pragma foreign_export("LANG",
             FUNC(MODE1, MODE2, ...) = MODE,
             "FOREIGNNAME").

exports a procedure for use by foreign language LANG.  For each
exported procedure the Mercury implementation will create an interface
to the named Mercury procedure in the foreign language using the name
FOREIGNNAME.  The form of this interface is dependent upon the
specified foreign language.  For further details see the language
specific information below.

   It is an error to export a Mercury procedure that has a determinism
of multi or nondet.


File: mercury_ref.info,  Node: Data passing conventions,  Next: Adding foreign declarations,  Prev: Using foreign enumerations in Mercury code,  Up: Foreign language interface

14.3 Data passing conventions
=============================

For each supported foreign language, we explain how to map a Mercury
type to a type in that foreign language.  We also map the Mercury
parameter passing convention to the foreign language's parameter
passing convention.

* Menu:

* C data passing conventions ::
* C# data passing conventions ::
* Java data passing conventions ::
* Erlang data passing conventions ::


File: mercury_ref.info,  Node: C data passing conventions,  Next: C# data passing conventions,  Up: Data passing conventions

14.3.1 C data passing conventions
---------------------------------

For each of the Mercury types `int', `float', `char', and `string',
there is a C typedef for the corresponding type in C: `MR_Integer',
`MR_Float', `MR_Char', and `MR_String' respectively.

   In the current implementation, `MR_Integer' is a typedef for a signed
integral type whose size is the same size as a pointer of type `void *';
`MR_Float' is a typedef for `double' (unless the program and the
Mercury library was compiled with `--single-prec-float', in which case
it is a typedef for `float'); `MR_Char' is a typedef for a signed
32-bit integral type and `MR_String' is a typedef for `char *'.

   Mercury variables of type `int', `float', `char', or `string' are
passed to and from C as C variables whose type is given by the
corresponding typedef.

   For the Mercury standard library type `bool.bool', there is a
corresponding C type, `MR_Bool'.  C code can refer to the boolean data
constructors `yes' and `no', as `MR_YES' and `MR_NO' respectively.

   For the Mercury standard library type `builtin.comparison_result',
there is a corresponding C type, `MR_Comparison_Result'.  C code can
refer to the data constructors of this type, `(<)', `(=)' and `(>)', as
`MR_COMPARE_LESS', `MR_COMPARE_EQUAL' and `MR_COMPARE_GREATER'
respectively.

   Mercury variables of a type for which there is a C `pragma
foreign_type' declaration (*note Using foreign types from Mercury::)
will be passed as the corresponding C type.

   Mercury tuple types are passed as `MR_Tuple', which in the current
implementation is a typedef for a pointer of type `void *' if
`--high-level-code' is enabled, and a typedef for `MR_Word' otherwise.

   Mercury variables of any other type are passed as a `MR_Word', which
in the current implementation is a typedef for an unsigned type whose
size is the same size as a pointer.  (Note: it would in fact be better
for each Mercury type to map to a distinct abstract type in C, since
that would be more type-safe, and thus we may change this in a future
release.  We advise programmers who are manipulating Mercury types in C
code to use typedefs for each user-defined Mercury type, and to treat
each such type as an abstract data type.  This is good style and it
will also minimize any compatibility problems if and when we do change
this.)

   Mercury lists can be manipulated by C code using the following
macros, which are defined by the Mercury implementation.

     MR_list_is_empty(list)     /* test if a list is empty */
     MR_list_head(list)         /* get the head of a list */
     MR_list_tail(list)         /* get the tail of a list */
     MR_list_empty()            /* create an empty list */
     MR_list_cons(head,tail)    /* construct a list with the given head and tail */

   Note that the use of these macros is subject to some caveats (*note
Memory management for C::).

   The implementation provides the macro `MR_word_to_float' for
converting a value of type `MR_Word' to one of type `MR_Float', and the
macro `MR_float_to_word' for converting a value of type `MR_Float' to
one of type `MR_Word'.  These macros must be used to perform these
conversions since for some Mercury implementations `sizeof(MR_Float)'
is greater than `sizeof(MR_Word)'.

   The following fragment of C code illustrates the correct way to
extract the head of a Mercury list of floats.

     MR_Float f;
     f = MR_word_to_float(MR_list_head(list));

   Omitting the call to `MR_word_to_float' in the above example would
yield incorrect results for implementations where `sizeof(MR_Float)' is
greater than `sizeof(MR_Word)'.


File: mercury_ref.info,  Node: C# data passing conventions,  Next: Java data passing conventions,  Prev: C data passing conventions,  Up: Data passing conventions

14.3.2 C# data passing conventions
----------------------------------

The Mercury types `int', `float', and `string' are mapped to the Common
Language Infrastructure (CLI) types `System.Int32', `System.Double', and
`System.String' respectively, which correspond to the C# types `int',
`double', and `string'.  The Mercury type `char' is mapped like `int';
_not_ to the CLI type `System.Char' because that only holds 16-bit
numeric values.

   For the Mercury standard library type `bool.bool', there is a
corresponding C# type, `mr_bool.Bool_0'.  C# code can refer to the
boolean data constructors `yes' and `no', as `mr_bool.YES' and
`mr_bool.NO' respectively.

   For the Mercury standard library type `builtin.comparison_result',
there is a corresponding C# type, `builtin.Comparison_result_0'.  C#
code can refer to the data constructors of this type, `(<)', `(=)' and
`(>)', as `builtin.COMPARE_LESS', `builtin.COMPARE_EQUAL' and
`builtin.COMPARE_GREATER' respectively.

   Mercury variables of a type for which there is a C# `pragma
foreign_type' declaration (*note Using foreign types from Mercury::)
will be passed as the corresponding C# type.  Both reference and value
types are supported.

   Mercury tuple types are passed as `object[]' where the length of the
array is the number of elements in the tuple.

   Mercury variables whose type is a type variable will be passed as
`System.Object'.

   Mercury variables whose type is a Mercury discriminated union type
will be passed as a CLI type whose type name is determined from the
Mercury type name (ignoring any type parameters) followed by an
underscore and then the type arity, expressed as a decimal integer.
The first character of the type name will have its case inverted, and
the name may be mangled to satisfy C# lexical rules.

For example, the following Mercury type corresponds to the C# class
that follows (some implementation details elided):

     :- type maybe(T)
         --->    yes(yes_field :: T)
         ;       no.

     public static class Maybe_1 {
         public static class Yes_1 : Maybe_1 {
             public object yes_field;
             public Yes_1(object x) { ... }
         }
         public static class No_0 : Maybe_1 {
             public No_0() { ... }
         }
     }

   C# code generated by the Mercury compiler is placed in the `mercury'
namespace.  Mercury module qualifiers are converted into a C# class
name by concatenating the components with double underscore separators
(`__').  For example the Mercury type `foo.bar.baz/1' will be passed as
the C# type `mercury.foo__bar.Baz_1'.

   Mercury array types are mapped to `System.Array'.

   Mercury variables whose type is a Mercury equivalence type will be
passed as the representation of the right hand side of the equivalence
type.

   This mapping is subject to change and you should try to avoid writing
code that relies heavily upon a particular representation of Mercury
terms.

   Mercury arguments declared with input modes are passed by value to
the C# function.

   Arguments of type `io.state' or `store.store(_)' are not passed or
returned at all.  (The reason for this is that these types represent
mutable state, and in C# modifications to mutable state are done via
side effects, rather than argument passing.)

   The handling of multiple output arguments is as follows.

   If the Mercury procedure is deterministic and has no output
arguments, then the return type of the C# function is `void'; if it has
one output argument, then the return value of the function is that
output argument.

   If the Mercury procedure is deterministic and has two or more output
arguments, then the return type of the C# function is `void'.  At the
position of each output argument, the C# function has an `out'
parameter.

   If the Mercury procedure is semi-deterministic then the C# function
returns a `bool'.  A `true' return value denotes success and `false'
denotes failure.  Output arguments are handled in the same way as
multiple outputs for deterministic procedures, using `out' parameters.
On failure the values of the `val' fields are undefined.

   Mercury lists can be manipulated by C# code using the following
methods, which are defined by the Mercury implementation.

     bool      list.is_empty(List_1 list)     // test if a list is empty
     object    list.det_head(List_1 list)     // get the head of a list
     List_1    list.det_tail(List_1 list)     // get the tail of a list
     List_1    list.empty_list()              // create an empty list
     List_1    list.cons(object head, List_1 tail)
                                              // construct a list with
                                              //  the given head and tail


File: mercury_ref.info,  Node: Java data passing conventions,  Next: Erlang data passing conventions,  Prev: C# data passing conventions,  Up: Data passing conventions

14.3.3 Java data passing conventions
------------------------------------

The Mercury types `int', `float', and `string' are mapped to the Java
types `int', `double', and `java.lang.String' respectively.  The
Mercury type `char' is mapped like `int'; _not_ to the Java type `char'
because that only holds 16-bit numeric values.

   For the Mercury standard library type `bool.bool', there is a
corresponding Java type, `bool.Bool_0'.  Java code can refer to the
boolean data constructors `yes' and `no', as `bool.YES' and `bool.NO'
respectively.

   For the Mercury standard library type `builtin.comparison_result',
there is a corresponding Java type, `builtin.Comparison_result_0'.
Java code can refer to the data constructors of this type, `(<)', `(=)'
and `(>)', as `builtin.COMPARE_LESS', `builtin.COMPARE_EQUAL' and
`builtin.COMPARE_GREATER' respectively.

   Mercury variables of a type for which there is a Java `pragma
foreign_type' declaration (*note Using foreign types from Mercury::)
will be passed as the corresponding Java type.

   Mercury tuple types are passed as `java.lang.Object[]' where the
length of the array is the number of elements in the tuple.

   Mercury variables whose types are universally quantified type
variables will have generic types.  Mercury variables whose types are
existentially quantified type variables will be passed as
`java.lang.Object'.

   Mercury variables whose type is a Mercury discriminated union type
will be passed as a Java type whose type name is determined from the
Mercury type name (ignoring any type parameters) followed by an
underscore and then the type arity, expressed as a decimal integer.
The first character of the type name will have its case inverted, and
the name may be mangled to satisfy Java lexical rules.  Generics are
used in the Java type for any type parameters.

For example, the following Mercury type corresponds to the Java class
that follows (some implementation details elided):

     :- type maybe(T)
         --->    yes(yes_field :: T)
         ;       no.

     public static class Maybe_1<T> {
         public static class Yes_1<T> extends Maybe_1 {
             public T yes_field;
             public Yes_1(T x) { ... }
         }
         public static class No_0<T> extends Maybe_1 {
             public No_0() { ... }
         }
     }

   Java code generated by the Mercury compiler is placed in the
`jmercury' package.  Mercury module qualifiers are converted into a
Java class name by concatenating the components with double underscore
separators (`__').  For example the Mercury type `foo.bar.baz/1' will
be passed as the Java type `jmercury.foo__bar.Baz_1'.

   Mercury array types are mapped to Java array types.

   Mercury variables whose type is a Mercury equivalence type will be
passed as the representation of the right hand side of the equivalence
type.

   This mapping is subject to change and you should try to avoid writing
code that relies heavily upon a particular representation of Mercury
terms.

   Mercury arguments declared with input modes are passed by value to
the corresponding Java function.  If the Mercury procedure is a function
whose result has an input mode, then the Mercury function result is
appended to the list of input parameters, so that the Mercury function
result becomes the last parameter to the corresponding Java function.

   Arguments of type `io.state' or `store.store(_)' are not passed or
returned at all.  (The reason for this is that these types represent
mutable state, and in Java modifications to mutable state are done via
side effects, rather than argument passing.)

   The handling of multiple output arguments is as follows.

   If the Mercury procedure is deterministic and has no output
arguments, then the return type of the Java function is `void'; if it
has one output argument, then the return value of the function is that
output argument.

   If the Mercury procedure is deterministic and has two or more output
arguments, then the return type of the Java function is `void'.  At the
position of each output argument, the Java function takes a value of
the type `jmercury.runtime.Ref<T>' where `T' is the Java type
corresponding to the type of the output argument.  `Ref' is a class
with a single field `val', which is assigned the output value when the
function returns.

   If the Mercury procedure is semi-deterministic then the Java function
returns a `boolean'.  A `true' return value denotes success and `false'
denotes failure.  Output arguments are handled in the same way as
multiple outputs for deterministic procedures, using the `Ref' class.
On failure the values of the `val' fields are undefined.

   Mercury lists can be manipulated by Java code using the following
methods, which are defined by the Mercury implementation.

     boolean   list.is_empty(List_1<E> list)     // test if a list is empty
     E         list.det_head(List_1<E> list)     // get the head of a list
     List_1<E> list.det_tail(List_1<E> list)     // get the tail of a list
     List_1<E> list.empty_list()                 // create an empty list
     <E, F extends E> List_1<E> list.cons(F head, List_1<E> tail)
                                                 // construct a list with
                                                 //  the given head and tail


File: mercury_ref.info,  Node: Erlang data passing conventions,  Prev: Java data passing conventions,  Up: Data passing conventions

14.3.4 Erlang data passing conventions
--------------------------------------

The Mercury types `int', `float' and `char' are mapped to Erlang
integers, floats and integers respectively.  A Mercury `string' is
represented by an Erlang binary, not by a list of integers.

   Mercury variables whose type is a Mercury discriminated union type
will be passed as an Erlang tuple with the first element of the tuple
being an Erlang atom named after the Mercury data constructor.  For
example, values of the type:

         :- type maybe_int
             --->    yes(int)
             ;       no.

would be represented in Erlang as `{yes, INTEGER}' and `{no}'.

   Mercury variables whose type is a Mercury equivalence type will be
passed as the representation of the right hand side of the equivalence
type.

   This mapping is subject to change and you should try to avoid writing
code that relies heavily upon a particular representation of Mercury
terms.

   Arguments of dummy types, e.g. `io.state', are represented by the
atom `false' when necessary.  They are not passed to and from calls to
monomorphic procedures.

   Mercury arguments declared with input modes are passed by value to
the corresponding Erlang function.

   The result of an Erlang function depends on the determinism of the
Mercury procedure that it was derived from.  Procedures which succeed
exactly once and have a single output variable return the single value
directly.  Procedures which succeed exactly once and have zero or two
or more output variables return a tuple of those output variables in
order.

   Procedures which are semideterministic return, on success, a tuple of
the variables with output modes (including when the number of output
variables is one).  On failure they return the Erlang atom `fail'.

   Procedures which are nondeterministic take as a final argument a
success continuation.  This is an function which has an input variable
for each variable of the Mercury procedure with an output mode.  For
each solution, the success continuation is called with the values of
those output variables.  When there are no more solutions the Erlang
function returns with an undefined value.


File: mercury_ref.info,  Node: Using foreign types from Mercury,  Next: Using Mercury enumerations in foreign code,  Prev: Calling Mercury from foreign code,  Up: Foreign language interface

14.4 Using foreign types from Mercury
=====================================

Types defined in a foreign language can be accessed in Mercury using a
declaration of the form

     :- pragma foreign_type(LANG, MERCURYTYPENAME, FOREIGNTYPEDESCRIPTOR).

   This defines MERCURYTYPENAME as a synonym for type
FOREIGNTYPEDESCRIPTOR defined in the foreign language LANG.  You must
declare MERCURYTYPENAME using a (possibly abstract) `:- type'
declaration as usual. The `pragma foreign_type' must not have wider
visibility than the type declaration (if the `pragma foreign_type'
declaration is in the interface, the `:- type' declaration must be
also).

   FOREIGNTYPEDESCRIPTOR defines how the Mercury type is mapped for a
particular foreign language.  Specific syntax is given in the language
specific information below.

   MERCURYTYPENAME is treated as an abstract type at all times in
Mercury code.  However, if MERCURYTYPENAME is one of the parameters of a
foreign_proc for LANG, and the `pragma foreign_type' declaration is
visible to the foreign_proc, it will be passed to that foreign_proc as
specified by FOREIGNTYPEDESCRIPTOR.

   Multiple foreign language definitions may be given for the same type
-- the appropriate definition will be used for the appropriate language
(see the language specific information below for details).  All
definitions must have the same visibility.  A Mercury definition, which
must define a discriminated union type, may also be given.  The
constructors for the type will only be visible in Mercury clauses for
predicates or functions with `pragma foreign_proc' clauses for all of
the languages for which there are `foreign_type' declarations for the
type.

   You can also associate assertions about the properties of the
foreign type with the `foreign_type' declaration, using the following
syntax:

     :- pragma foreign_type(LANG, MERCURYTYPENAME, FOREIGNTYPEDESCRIPTOR, [FOREIGNTYPEASSERTION, ...]).

   Currently, two kinds of assertions are supported.  The
`can_pass_as_mercury_type' assertion states that on the C backends,
values of the given type can be passed to and from Mercury code without
boxing, via simple casts, which is faster.  This requires the type to
be either an integer type or a pointer type, and requires its size to
be the same as or less than the size of Mercury word.  Since deciding
whether a C type satisfies this condition requires knowledge of the
Mercury implementation, and violations are very likely to result in the
generated executable silently doing the wrong thing, we do not
recommend the use of assertions unless you are an implementor of the
Mercury system.  The `stable' assertion is meaningful only in the
presence of the `can_pass_as_mercury_type' assertion.  It states that
either the C type is an integer type, or it is a pointer type pointing
to memory that will never change.  Together, these assertions are
sufficient to allow tabling (*note Tabled evaluation::) and the
`compare_representation' primitive to work on values of such types.

   As with discriminated union types, programmers can specify the
unification and/or comparison predicates to use for values of the type
using the following syntax (*note User-defined equality and
comparison::):

     :- pragma foreign_type(LANG, MERCURYTYPENAME, FOREIGNTYPEDESCRIPTOR)
             where equality is EQUALITYPRED, comparison is COMPAREPRED.

   You can use Mercury foreign language interfacing declarations which
specify language X to interface to types that are actually written in a
different language Y provided that X and Y have compatible interface
conventions.  Support for this kind of compatibility is described in
the language specific information below.


File: mercury_ref.info,  Node: Using Mercury enumerations in foreign code,  Next: Using foreign enumerations in Mercury code,  Prev: Using foreign types from Mercury,  Up: Foreign language interface

14.5 Using Mercury enumerations in foreign code
===============================================

Values of Mercury enumeration types can be made available to code in the
bodies of `foreign_proc' and `foreign_code' pragmas via a declaration
of the form:

     :- pragma foreign_export_enum("LANG", MERCURYTYPE,
             ATTRIBUTES, OVERRIDES).

   This causes the compiler to create a symbolic name in language LANG
for each of the constructors of MERCURYTYPE.  The symbolic name allows
the foreign code to create a value corresponding to that of the
constructor it represents.  (The exact mechanism used depends upon the
foreign language; see the language specific information below for
further details.)

   For each foreign language there is a default mapping between the name
of a Mercury constructor and its symbolic name in the language LANG.
This default mapping is not required to map every valid constructor name
to a valid name in language LANG; where it does not the programmer must
specify a valid symbolic name.  The programmer may also choose to map a
constructor to a symbolic name that differs from the one supplied by
the default mapping for language LANG.  OVERRIDES is a list whose
elements are pairs of constructor names and strings.  The latter
specify the name that the implementation should use as the symbolic
name in the foreign language.  OVERRIDES has the following form:

     [cons_I - "symbol_I", ..., cons_J - "symbol_J"]

   This can be used to provide either a valid symbolic name where the
default mapping does not, or to override a valid symbolic name
generated by the default mapping.  This argument may be omitted if
OVERRIDES is empty.

   The argument ATTRIBUTES is a list of optional attributes.  If empty,
it may be omitted from the `pragma foreign_export_enum' declaration.
The following attributes must be supported by all Mercury
implementations.

`prefix(Prefix)'
     Prefix each symbolic name, regardless of how it was generated, with
     the string PREFIX.  At most one `prefix' attribute may be
     specified for a `pragma foreign_export_enum' declaration.

`uppercase'
     Convert any alphabetic characters in a Mercury constructor name to
     uppercase when generating the symbolic name using the default
     mapping.  Symbolic names specified by the programmer using
     OVERRIDES are not affected by this attribute.  If the `prefix'
     attribute is also specified, then the prefix is added to the
     symbolic name _after_ the conversion to uppercase has been
     performed, i.e. the characters in the prefix are not affected by
     the `uppercase' attribute.


   The implementation does not check the validity of a symbolic name in
the foreign language until after the effects of any attributes have
been applied.  This means that attributes may cause an otherwise valid
symbolic name to become invalid or vice versa.

   It is an error if the mapping between constructors and symbolic names
does not form a bijection.  A program can contain multiple `pragma
foreign_export_enum' declarations for a single Mercury type.  The
implementation is not required to check that the symbolic names
generated by separate `pragma foreign_export_enum' declarations are
unique.

   A module may contain `pragma foreign_export_enum' declarations that
refer to imported types, subject to the usual visibility restrictions.

   A `pragma foreign_export_enum' declaration may only occur in the
implementation section of a module.


File: mercury_ref.info,  Node: Using foreign enumerations in Mercury code,  Next: Data passing conventions,  Prev: Using Mercury enumerations in foreign code,  Up: Foreign language interface

14.6 Using foreign enumerations in Mercury code
===============================================

The values used to represent a Mercury enumeration type in a foreign
language may be explicitly assigned by the programmer using a
declaration of the form:

     :- pragma foreign_enum("LANG", MERCURYTYPE, CTORVALUES).

   CTORVALUES is a list of pairs of the form:

     [
         ctor_0 - "ForeignValue_0",
         ctor_1 - "ForeignValue_1",
         ...
         ctor_N - "ForeignValue_N"
     ]

   The first element of each pair is a constructor of the type
MERCURYTYPE, and the second is a value in the language LANG that will
be used to represent that constructor.  The mapping defined by this
list of pairs must form a bijection.

   Mercury implementations may impose further foreign language-specific
restrictions on the form that values used to represent enumeration
constructors may take.  See the language specific information below for
details.

   The Mercury implementation is not required to check the validity of
foreign enumeration values.

   A `pragma foreign_enum' declaration must occur in the implementation
section of the module that defines the type MERCURYTYPE.  It is an
error if the type MERCURYTYPE is the subject of more than one `pragma
foreign_enum' declaration for a given foreign language.

   Note that the default comparison for types that are the subject of a
`pragma foreign_enum' declaration will be defined by the foreign
values, rather than the order of the constructors in the type
declaration (as is usually the case).


File: mercury_ref.info,  Node: Adding foreign declarations,  Next: Adding foreign definitions,  Prev: Data passing conventions,  Up: Foreign language interface

14.7 Adding foreign declarations
================================

Foreign language declarations (such as type declarations, header file
inclusions or macro definitions) can be included in the Mercury source
file as part of a `foreign_decl' declaration of the form

     :- pragma foreign_decl("LANG", DECLCODE).

   This declaration will have effects equivalent to including the
specified DECLCODE in an automatically-generated source file of the
specified programming language, in a place appropriate for declarations,
and linking that source file with the Mercury program (after having
compiled it with a compiler for the specified programming language, if
appropriate).

   Entities declared in `pragma foreign_decl' declarations are visible
in `pragma foreign_code', `pragma foreign_type', `pragma foreign_proc',
and `pragma foreign_enum' declarations that specify the same foreign
language and occur in the same Mercury module.

   By default, the contents of `pragma foreign_decl' declarations are
also visible in the same kinds of declarations in other modules that
import the module containing the `pragma foreign_decl' declaration.
This is because they may be required to make sense of types defined
using `pragma foreign_type' and/or predicates defined using `pragma
foreign_code' in the containing module, and these may be visible in
other modules, especially in the presence of intermodule optimization,

   If you do not want the contents of a `pragma foreign_decl'
declaration to be visible in foreign language code in other modules,
you can use the following variant of the declaration:

     :- pragma foreign_decl("LANG", local, DECLCODE).

   Note: currently only the C and Erlang backends support this variant
of the `pragma foreign_decl' declaration.

   The declarations for Mercury predicates or functions exported to a
foreign language using a `pragma foreign_export' declaration are
visible to foreign code in a `pragma foreign_code' or `pragma
foreign_proc' declaration of the same module and also in those of any
sub-modules.  They are not visible to the foreign code in `pragma
foreign_code' or `pragma foreign_proc' declarations in any other module.
They can be made visible using a declaration of the form:

     :- pragma foreign_import_module("LANG", IMPORTEDMODULE).

where IMPORTEDMODULE is the name of the module containing the `pragma
foreign_export' declarations.

   If LANG is `"C"' this is equivalent to

     :- pragma foreign_decl("C", "#include ""IMPORTEDMODULE.mh""").

where `IMPORTEDMODULE.mh' is the automatically generated header file
containing the C declarations for the predicates and functions exported
to C.

   `pragma foreign_import_module' should be used instead of the
explicit `#include' because `pragma foreign_import_module' tells the
implementation that `IMPORTEDMODULE.mh' must be built before the object
file for the module containing the `pragma foreign_import_module'
declaration.

   A cycle of `pragma foreign_import_module', where the language is
`"C#"' or `"Java"', is not permitted.

   Note that the Melbourne Mercury implementation often implicitly
inserts `pragma foreign_import_module' declarations but programmers
should _not_ write code that depends upon this behaviour; `pragma
foreign_import_module' declarations should always be explicitly
included if needed.


File: mercury_ref.info,  Node: Adding foreign definitions,  Next: Language specific bindings,  Prev: Adding foreign declarations,  Up: Foreign language interface

14.8 Adding foreign definitions
===============================

Definitions of foreign language entities (such as functions or global
variables) may be included using a declaration of the form

     :- pragma foreign_code("LANG", CODE).

   This declaration will have effects equivalent to including the
specified CODE in an automatically-generated source file of the
specified programming language, in a place appropriate for definitions,
and linking that source file with the Mercury program (after having
compiled it with a compiler for the specified programming language, if
appropriate).

   Entities declared in `pragma foreign_code' declarations are visible
in `pragma foreign_proc' declarations that specify the same foreign
language and occur in the same Mercury module.


File: mercury_ref.info,  Node: Language specific bindings,  Prev: Adding foreign definitions,  Up: Foreign language interface

14.9 Language specific bindings
===============================

* Menu:

* Interfacing with C 		:: How to write code to interface with C
* Interfacing with C# 		:: How to write code to interface with C#
* Interfacing with Java 	:: How to write code to interface with Java
* Interfacing with Erlang 	:: How to write code to interface with Erlang

   All Mercury implementations should support interfacing with C.  The
set of other languages supported is implementation-defined.  A suitable
compiler or assembler for the foreign language must be available on the
system.

   The University of Melbourne Mercury implementation supports
interfacing with the following languages:

`C'
     Use the string `"C"' to set the foreign language to C.

`C#'
     Use the string `"C#"' to set the foreign language to C#.

`Java'
     Use the string `"Java"' to set the foreign language to Java.

`Erlang'
     Use the string `"Erlang"' to set the foreign language to Erlang.



File: mercury_ref.info,  Node: Interfacing with C,  Next: Interfacing with C#,  Up: Language specific bindings

14.9.1 Interfacing with C
-------------------------

* Menu:

* Using pragma foreign_type for C 	 :: Declaring C types in Mercury
* Using pragma foreign_export_enum for C :: Using Mercury enumerations in C
* Using pragma foreign_enum for C        :: Assigning Mercury enumerations
                                            values in C
* Using pragma foreign_proc for C 	 :: Calling C code from Mercury
* Using pragma foreign_export for C      :: Calling Mercury code from C
* Using pragma foreign_decl for C 	 :: Including C declarations in Mercury
* Using pragma foreign_code for C 	 :: Including C code in Mercury
* Memory management for C                :: Caveats about passing dynamically
                                            allocated memory to or from C.
* Linking with C object files            :: Linking with C object files and
                                            libraries.


File: mercury_ref.info,  Node: Using pragma foreign_type for C,  Next: Using pragma foreign_export_enum for C,  Up: Interfacing with C

14.9.1.1 Using pragma foreign_type for C
........................................

A C `pragma foreign_type' declaration has the form:

     :- pragma foreign_type("C", MERCURYTYPENAME, "CFOREIGNTYPE").

   For example,

     :- pragma foreign_type("C", long_double, "long double").

   The CFOREIGNTYPE can be any C type name that obeys the following
restrictions.  Function types, array types, and incomplete types are
not allowed.  The type name must be such that when declaring a variable
in C of that type, that no part of the type name is required after the
variable name.  (This rule prohibits, for example, function pointer
types such as `void (*)(void)'.  However, it would be OK to use a
typedef name which was defined as a function pointer type.)

   C preprocessor directives (such as `#if') may not be used in
CFOREIGNTYPE.  (You can however use a typedef name that refers to a
type defined in a `pragma foreign_decl' declaration, and the `pragma
foreign_decl' declaration may contain C preprocessor directives.)

   *With `--gc accurate', foreign_types which are C pointer types must
not point to the Mercury heap.*

   If the MERCURYTYPENAME is the type of a parameter of a procedure
defined using `pragma foreign_proc', it will be passed to the
foreign_proc's foreign language code as CFOREIGNTYPE.

   Furthermore, any Mercury procedure exported with `pragma
foreign_export' will use CFOREIGNTYPE as the type for any parameters
whose Mercury type is MERCURYTYPENAME.

   The builtin Mercury type `c_pointer' may be used to pass C pointers
between C functions which are called from Mercury.  For example:

     :- module pointer_example.
     :- interface.

     :- type complicated_c_structure.

     % Initialise the abstract C structure that we pass around in Mercury.
     :- pred initialise_complicated_structure(complicated_c_structure::uo) is det.

     % Perform a calculation on the C structure.
     :- pred do_calculation(int::in, complicated_c_structure::di,
             complicated_c_structure::uo) is det.

     :- implementation.

     % Our C structure is implemented as a c_pointer.
     :- type complicated_c_structure
         --->    complicated_c_structure(c_pointer).

     :- pragma foreign_decl("C",
        extern struct foo *init_struct(void);
        extern struct foo *perform_calculation(int, struct foo *);
     ");

     :- pragma foreign_proc("C",
         initialise_complicated_structure(Structure::uo),
         [will_not_call_mercury, may_call_mercury],
     "
         Structure = init_struct();
     ").

     :- pragma foreign_proc("C",
         do_calculation(Value::in, Structure0::di, Structure::uo),
         [will_not_call_mercury, may_call_mercury],
     "
         Structure = perform_calculation(Value, Structure0);
     ").

   We strongly recommend the use of `pragma foreign_type' instead of
`c_pointer' as the use of `pragma foreign_type' results in more
type-safe code.


File: mercury_ref.info,  Node: Using pragma foreign_export_enum for C,  Next: Using pragma foreign_enum for C,  Prev: Using pragma foreign_type for C,  Up: Interfacing with C

14.9.1.2 Using pragma foreign_export_enum for C
...............................................

For C the symbolic names generated by a `pragma foreign_export_enum'
must form valid C identifiers.  These identifiers are used as the names
of preprocessor macros.  The body of each of these macros expands to a
value that is identical to that of the constructor to which the
symbolic name corresponds in the mapping established by the `pragma
foreign_export_enum' declaration.

   As noted in the *note C data passing conventions::, the type of these
values is `MR_Word'.

   The default mapping used by `pragma foreign_export_enum'
declarations for C is to use the Mercury constructor name as the base
of the symbolic name.  For example, the symbolic name for the Mercury
constructor `foo' would be `foo'.


File: mercury_ref.info,  Node: Using pragma foreign_enum for C,  Next: Using pragma foreign_proc for C,  Prev: Using pragma foreign_export_enum for C,  Up: Interfacing with C

14.9.1.3 Using pragma foreign_enum for C
........................................

Foreign enumeration values in C must be constants of type `MR_Integer'.
They may be specified as either integer literals or via preprocessor
macros that expand to integer literals.


File: mercury_ref.info,  Node: Using pragma foreign_proc for C,  Next: Using pragma foreign_export for C,  Prev: Using pragma foreign_enum for C,  Up: Interfacing with C

14.9.1.4 Using pragma foreign_proc for C
........................................

The input and output variables will have C types corresponding to their
Mercury types, as determined by the rules specified in *note C data
passing conventions::.

   The C code fragment may declare local variables, up to a total size
of 10kB for the procedure.  If a procedure requires more than this for
its local variables, the code can be moved into a separate function
(defined in a `pragma foreign_code' declaration, for example).

   The C code fragment should not declare any labels or static
variables unless there is also a `pragma no_inline' declaration or a
`may_not_duplicate' foreign code attribute for the procedure.  The
reason for this is that otherwise the Mercury implementation may inline
the procedure by duplicating the C code fragment for each call.  If the
C code fragment declared a static variable, inlining it in this way
could result in the program having multiple instances of the static
variable, rather than a single shared instance.  If the C code fragment
declared a label, inlining it in this way could result in an error due
to the same label being defined twice inside a single C function.

   C code in a `pragma foreign_proc' declaration for any procedure whose
determinism indicates that it can fail must assign a truth value to the
macro `SUCCESS_INDICATOR'.  For example:

     :- pred string.contains_char(string, character).
     :- mode string.contains_char(in, in) is semidet.

     :- pragma foreign_proc("C",
     	string.contains_char(Str::in, Ch::in),
             [will_not_call_mercury, promise_pure],
             "SUCCESS_INDICATOR = (strchr(Str, Ch) != NULL);").

   `SUCCESS_INDICATOR' should not be used other than as the target of
an assignment.  (For example, it may be `#define'd to a register, so
you should not try to take its address.)  Procedures whose determinism
indicates that they cannot fail should not access `SUCCESS_INDICATOR'.

   Arguments whose mode is input will have their values set by the
Mercury implementation on entry to the C code.  If the procedure
succeeds, the C code must set the values of all output arguments.  If
the procedure fails, the C code need only set `SUCCESS_INDICATOR' to
false (zero).

   The behaviour of a procedure defined using a `pragma foreign_proc'
declaration whose body contains a `return' statement is undefined.


File: mercury_ref.info,  Node: Using pragma foreign_export for C,  Next: Using pragma foreign_decl for C,  Prev: Using pragma foreign_proc for C,  Up: Interfacing with C

14.9.1.5 Using pragma foreign_export for C
..........................................

A `pragma foreign_export' declaration for C has the form:

     :- pragma foreign_export("C", MERCURYMODE, "C_NAME").

   For example,

     :- pragma foreign_export("C", foo(in, in, out), "FOO").

   For each Mercury module containing `pragma foreign_export'
declarations for C, the Mercury implementation will automatically
create a header file for that module which declares a C function
C_NAME() for each of the `pragma foreign_export' declarations.  Each
such C function is the C interface to the specified Mercury procedure.

   The type signature of the C interface to a Mercury procedure is
determined as follows.  Mercury types are converted to C types
according to the rules in *note C data passing conventions::.  Input
arguments are passed by value.  For output arguments, the caller must
pass the address in which to store the result.  If the Mercury
procedure can fail, then its C interface function returns a truth value
indicating success or failure.  If the Mercury procedure is a Mercury
function that cannot fail, and the function result has an output mode,
then the C interface function will return the Mercury function result
value.  Otherwise the function result is appended as an extra argument.
Arguments of type `io.state' or `store.store(_)' are not passed at all.
(The reason for this is that these types represent mutable state, and
in C modifications to mutable state are done via side effects, rather
than argument passing.)

   Calling polymorphically typed Mercury procedures from C is a little
bit more difficult than calling ordinary (monomorphically typed)
Mercury procedures.  The simplest method is to just create monomorphic
forwarding procedures that call the polymorphic procedures, and export
them, rather than exporting the polymorphic procedures.

   If you do export a polymorphically typed Mercury procedure, the
compiler will prepend one `type_info' argument to the parameter list of
the C interface function for each distinct type variable in the Mercury
procedure's type signature.  The caller must arrange to pass in
appropriate `type_info' values corresponding to the types of the other
arguments passed.  These `type_info' arguments can be obtained using
the Mercury `type_of' function in the Mercury standard library module
`type_desc'.

   To use the C declarations produced see *note Using pragma
foreign_decl for C::.


File: mercury_ref.info,  Node: Using pragma foreign_decl for C,  Next: Using pragma foreign_code for C,  Prev: Using pragma foreign_export for C,  Up: Interfacing with C

14.9.1.6 Using pragma foreign_decl for C
........................................

Any macros, function prototypes, or other C declarations that are used
in `foreign_code', `foreign_type' or `foreign_proc' pragmas must be
included using a `foreign_decl' declaration of the form

     :- pragma foreign_decl("C", HEADERCODE).

HEADERCODE can be a C `#include' line, for example

     :- pragma foreign_decl("C", "#include <math.h>")

or

     :- pragma foreign_decl("C", "#include ""tcl.h""").

or it may contain any C declarations, for example

     :- pragma foreign_decl("C", "
             extern int errno;
             #define SIZE 200
             struct Employee {
                     char name[SIZE];
             };
             extern int bar;
             extern void foo(void);
     ").

   Mercury automatically includes certain headers such as `<stdlib.h>',
but you should not rely on this, as the set of headers which Mercury
automatically includes is subject to change.

   If a Mercury predicate or function exported using a `pragma
foreign_export' declaration is to be used within a `:- pragma
foreign_code' or `:- pragma foreign_proc' declaration the header file
for the module containing the `pragma foreign_export' declaration
should be included using a `pragma foreign_import_module' declaration,
for example

     :- pragma foreign_import_module("C", exporting_module).


File: mercury_ref.info,  Node: Using pragma foreign_code for C,  Next: Memory management for C,  Prev: Using pragma foreign_decl for C,  Up: Interfacing with C

14.9.1.7 Using pragma foreign_code for C
........................................

Definitions of C functions or global variables may be included using a
declaration of the form

     :- pragma foreign_code("C", CODE).

   For example,

     :- pragma foreign_code("C", "
             int bar = 42;
             void foo(void) {}
     ").

   Such code is copied verbatim into the generated C file.


File: mercury_ref.info,  Node: Memory management for C,  Next: Linking with C object files,  Prev: Using pragma foreign_code for C,  Up: Interfacing with C

14.9.1.8 Memory management for C
................................

Passing pointers to dynamically-allocated memory from Mercury to code
written in other languages, or vice versa, is in general
implementation-dependent.

   The current Mercury implementation supports two different methods of
memory management: conservative garbage collection, or no garbage
collection.  (With the latter method, heap storage is reclaimed only on
backtracking.)

   Conservative garbage collection makes inter-language calls simplest.
When using conservative garbage collection, heap storage is reclaimed
automatically.  Pointers to dynamically-allocated memory can be passed
to and from C without taking any special precautions.

   When using no garbage collection, you must be careful not to retain
pointers to memory on the Mercury heap after Mercury has backtracked to
before the point where that memory was allocated.  You must also avoid
the use of the macros `MR_list_empty()' and `MR_list_cons()'.  (The
reason for this is that they may access Mercury's `MR_hp' register,
which might not be valid in C code.  Using them in the bodies of
procedures defined using `pragma foreign_proc' with
`will_not_call_mercury' would probably work, but we don't advise it.)
Instead, you can write Mercury functions to perform these actions and
use `pragma foreign_export' to access them from C.  This alternative
method also works with conservative garbage collection.

   Future Mercury implementations may use non-conservative methods of
garbage collection.  For such implementations, it will be necessary to
explicitly register pointers passed to C with the garbage collector.
The mechanism for doing this has not yet been decided on.  It would be
desirable to provide a single memory management interface for use when
interfacing with other languages that can work for all methods of
memory management, but more implementation experience is needed before
we can formulate such an interface.


File: mercury_ref.info,  Node: Linking with C object files,  Prev: Memory management for C,  Up: Interfacing with C

14.9.1.9 Linking with C object files
....................................

A Mercury implementation should allow you to link with object files or
libraries that were produced by compiling C code.  The exact mechanism
for linking with C object files is implementation-dependent.  The
following text describes how it is done for the University of Melbourne
Mercury implementation.

   To link an existing object file into your Mercury code, use the
command line option `--link-object'.  For example, the following will
link the object file `my_function.o' from the current directory when
compiling the program `prog':

     mmc --link-object my_functions.o prog

   The command line option `--library' (or `-l' for short) can be used
to link an existing library into your Mercury code.  For example, the
following will link the library file `libfancy_library.a', or perhaps
the shared version `libfancy_library.so', from the directory
`/usr/local/contrib/lib', when compiling the program `prog':

     mmc -R/usr/local/contrib/lib -L/usr/local/contrib/lib --lfancy_library prog

   As illustrated by the example, the command line options `-R', `-L'
and `-l', have the same meaning as they do with the Unix linker.

   For more information, see the "Libraries" chapter of the Mercury
User's Guide.


File: mercury_ref.info,  Node: Interfacing with C#,  Next: Interfacing with Java,  Prev: Interfacing with C,  Up: Language specific bindings

14.9.2 Interfacing with C#
--------------------------

* Menu:

* Using pragma foreign_type for C#	:: Declaring C# types in Mercury
* Using pragma foreign_export_enum for C# :: Using Mercury enumerations in C#
* Using pragma foreign_enum for C#      :: Assigning Mercury enumerations
                                           values in C#
* Using pragma foreign_proc for C# 	:: Calling C# code from Mercury
* Using pragma foreign_export for C#    :: Calling Mercury code from C#
* Using pragma foreign_decl for C# 	:: Including C# declarations in Mercury
* Using pragma foreign_code for C# 	:: Including C# code in Mercury


File: mercury_ref.info,  Node: Using pragma foreign_type for C#,  Next: Using pragma foreign_export_enum for C#,  Up: Interfacing with C#

14.9.2.1 Using pragma foreign_type for C#
.........................................

A C# `pragma foreign_type' declaration has the form:

     :- pragma foreign_type("C#", MERCURYTYPENAME, "C#-TYPE").

   The C#-TYPE can be any accessible C# type.

   The effect of this declaration is that Mercury values of type
MERCURYTYPENAME will be passed to and from C# foreign_procs as having
type C#-TYPE.

   Furthermore, any Mercury procedure exported with `pragma
foreign_export' will use C#-TYPE as the type for any parameters whose
Mercury type is MERCURYTYPENAME.


File: mercury_ref.info,  Node: Using pragma foreign_export_enum for C#,  Next: Using pragma foreign_enum for C#,  Prev: Using pragma foreign_type for C#,  Up: Interfacing with C#

14.9.2.2 Using pragma foreign_export_enum for C#
................................................

For C# the symbolic names generated by a `pragma foreign_export_enum'
must form valid C# identifiers.  These identifiers are used as the
names of static class members.

   The default mapping used by `pragma foreign_export_enum'
declarations for C# is to use the Mercury constructor name as the base
of the symbolic name.  For example, the symbolic name for the Mercury
constructor `foo' would be `foo'.


File: mercury_ref.info,  Node: Using pragma foreign_enum for C#,  Next: Using pragma foreign_proc for C#,  Prev: Using pragma foreign_export_enum for C#,  Up: Interfacing with C#

14.9.2.3 Using pragma foreign_enum for C#
.........................................

Foreign enumeration values in C# must be a constant value expression
which is a valid initializer within an enumeration of underlying type
`int'.


File: mercury_ref.info,  Node: Using pragma foreign_proc for C#,  Next: Using pragma foreign_export for C#,  Prev: Using pragma foreign_enum for C#,  Up: Interfacing with C#

14.9.2.4 Using pragma foreign_proc for C#
.........................................

The C# code from C# pragma foreign_proc declarations will be placed in
the bodies of static member functions of an automatically-generated C#
class.  Since such C# code will become part of a static member function,
it must not refer to the `this' keyword.  It may however refer to
static member variables or static member functions declared with
`pragma foreign_code'.

   The input and output variables for a C# `pragma foreign_proc' will
have C# types corresponding to their Mercury types.  The exact rules
for mapping Mercury types to C# types are described in *note C# data
passing conventions::.

   C# code in a `pragma foreign_proc' declaration for any procedure
whose determinism indicates that it can fail must assign a value of
type `bool' to the variable `SUCCESS_INDICATOR'.  For example:

     :- pred string.contains_char(string, character).
     :- mode string.contains_char(in, in) is semidet.

     :- pragma foreign_proc("C#",
     	string.contains_char(Str::in, Ch::in),
             [will_not_call_mercury, promise_pure],
             "SUCCESS_INDICATOR = (Str.IndexOf(Ch) != -1);").

C# code for procedures whose determinism indicates that they cannot fail
should not access `SUCCESS_INDICATOR'.

   Arguments whose mode is input will have their values set by the
Mercury implementation on entry to the C# code.  If the procedure
succeeds, the C# code must set the values of all output arguments.  If
the procedure fails, the C# code need only set `SUCCESS_INDICATOR' to
false.


File: mercury_ref.info,  Node: Using pragma foreign_export for C#,  Next: Using pragma foreign_decl for C#,  Prev: Using pragma foreign_proc for C#,  Up: Interfacing with C#

14.9.2.5 Using pragma foreign_export for C#
...........................................

A `pragma foreign_export' declaration for C# has the form:

     :- pragma foreign_export("C#", MERCURYMODE, "C#_NAME").

   For example,

     :- pragma foreign_export("C#", foo(in, in, out), "FOO").

   The type signature of the C# interface to a Mercury procedure is as
described in *note C# data passing conventions::.

   Calling polymorphically typed Mercury procedures from C# is a little
bit more difficult than calling ordinary (monomorphically typed)
Mercury procedures.  The simplest method is to just create monomorphic
forwarding procedures that call the polymorphic procedures, and export
them, rather than exporting the polymorphic procedures.

   If you do export a polymorphically typed Mercury procedure, the
compiler will prepend one `type_info' argument to the parameter list of
the C# interface function for each distinct type variable in the
Mercury procedure's type signature.  The caller must arrange to pass in
appropriate `type_info' values corresponding to the types of the other
arguments passed.  These `type_info' arguments can be obtained using
the Mercury `type_of' function in the Mercury standard library module
`type_desc'.

