Report on Curry

Since the design and implementation of Curry is under development, the language definition contained in the report should be considered as preliminary in various aspects. Nevertheless, the report is the main reference on Curry so that implementations of Curry should refer to this report to explain restrictions or differences.

If you are interested in a general introduction to programming in Curry, please look at the tutorial on Curry.

Here you can also find a Java applet for showing syntax diagrams for Curry which can be easily traversed by clicking on the corresponding grammar symbols.

• Curry: An Integrated Functional Logic Language (Version 0.8.3 of September 11, 2012)
  This is the current report describing the language Curry

  Changes to the previous version:

  • Section 2.3 (Function declarations):
    • The restrictions on higher-order rules (i.e., which were considered as syntactic sugar for eta expanded rules) has been omitted (since eta expansion changes the sharing behavior). See also the discussion in the Curry mailing list.
    • Restrictions on linear left-hand sides in function definitions removed. See the discussion in the Curry mailing list.
  • Section 2.5 (Free variables): Anonymous free variables are allowed in expressions. Thus, an occurrence of "_" in an expression is an abbreviation of "let x free in x". See the discussion in the Curry mailing list.
  • New Section 5.4 (Flexible case expressions): fcase expressions for denoting flexible pattern matching without explicitly introducing an auxiliary function added. Thus, fcase is now also a keyword (see Section C.1). See the discussion in the Curry mailing list.
  • Appendix B (Prelude): definition of failed changed to external function
  • Appendix D.7 (Eliminating local declarations): semantics of left and right sections defined in a symmetric way. See also the discussion in the Curry mailing list.

• Version 0.8.2 of March 28, 2006
  Changes to the previous version:
  • Section 2.3: As-patterns added.
  • Section 2.5 and C.3: Restriction of "let...free" to constraints removed.
  • Section 3 and D.6: Default evaluation strategy of functions defined as flexible. Notion of "rigid" functions omitted since all defined functions are flexible. Description of operational semantics adapted to suspension of case/ensureNotFree.
  • Section 4.1.7: "backslash" notation for character constants discussed.
  • Section 5: Definition of case expressions extended with guards and local declarations in the alternatives. Description of ensureNotFree/ensureSpine added (also in the prelude).
  • Section 6 (Modules) updated:
    • A module M (without dots in M) must be stored in file M.curry
    • The default head for a module in file M.curry is "module M where"
    • The prelude is only implicitly imported if it is not explicitly imported.
    • Module "prelude" renamed to "Prelude"
    • Top-level declarations inside a module M are always accessible by qualification.
  • Sections 8.4 and D.3 (Committed Choice) deleted. Furthermore, "eval choice" annotation omitted (and also from the list of reserved words).
  • Appendix C.1: "eval" added to list of keywords, as/hiding/qualified/rigid removed.
  • Appendix C.3: Syntax of type expressions and patterns corrected.
  • Appendix B (Prelude):
    • Definition of non-deterministic operator "?" added.
    • Definition of specific application operators $!!, $#, $## added
    • Definition of "unknown" added.
    • Definition of datatype "Ordering" and operation "compare" added.
    • (<), (<=), (>) and (>=) defined polymorphic in terms of compare.
    • Definition of "min" and "max" added.
    • Definition of "negate" added.
    • Definition of take/drop/splitAt changed so that they behave on negative numbers similar to 0.
    • if_then_else defined by case expression
    • Type of (&>) generalized
  • Appendix D.2: Semantics of "ensureNotFree" added.
  • "undefined" replaced by "failed" in the definition of the semantics of rules with multiple guards.
  • Syntax of list comprehensions extended to allow local let declarations
• Version 0.8.0 of April 15, 2003
  Changes to the previous version:
  • Sect. 2.3: Rules with multiple guards must contain Boolean guards, i.e., multiple guards of type Success are no longer allowed.
  • Sect. 5 on expressions introduced and new subsection on case expressions added.
  • Appendix B (Prelude): Functions sequenceIO, sequenceIO_, mapIO, mapIO_ added.
  • Appendix C.3: Syntax of identifiers extended: single quotes are allowed as digits or underscores.
  • Appendix C.3: Syntax of "do" expressions corrected: the last element must be an expression and not a statement.
  • Appendix C.3: Syntax of "case" expressions added.
  • Appendix D.8: Multiple constraint guards eliminated.
  • Appendix D.8: Transformation to eliminate local patterns changed to support lazy pattern matching.
• Version 0.7.2 of September 16, 2002
  Changes to the previous version:
  • Sect. 3: Defaults for flexible and rigid functions changed. Only IO actions are rigid, all others are flexible. Consequently, pragmas are no longer necessary (i.e., the section on pragmas has been deleted) as well as the evaluation annotation "eval flex". The syntax has been adapted accordingly.
  • Appendix B (Prelude): Definition of zip/zip3 changed so that it is compatible with Haskell.
  • Appendix B (Prelude): Functions error, failed, zipWith, zipWith3, unzip, unzip3, words, unwords, reverse, and, or, any, all, elem, notElem, doSolve, seq, $! added
  • Appendix B (Prelude): Search operator "all" renamed to "solveAll" (to avoid name clash with Haskell's "all")
  • Appendix B (Prelude): Bug in definition of "one" eliminated (dfs -> solveAll)
  • Appendix B (Prelude): Explicit definitions for >> and browse provided.
  • Appendix B (Prelude): Definition of !! slightly changed so that it is only defined on the correct bounds
• Version 0.7.1 of June 6, 2000
  Changes to the previous version:
  • Sect. 2.2: Type synonym declarations added.
  • Sect. 4.1.2: Explanation of type "Success" slightly improved.
  • Sect. 4.1.7: Notation for arithmetic sequences and list comprehensions added.
  • Sect. 6.2: Do notation added.
  • Appendix B (Prelude): Operators >> and >>= defined as left associative to be compatible with Haskell.
  • Appendix B (Prelude): Generator functions for arithmetic sequences (enumFrom...), if_then_else, null, and print added to the prelude.
  • Appendix C.3: Curry grammar extended for the new syntactic sugar (see above).
  • Appendix C.3 and Sect. 5: Syntactic ambiguities between module qualification and function composition resolved by clarifying the positioning of blanks.
• Version 0.7 of February 2, 2000
  Changes to the previous version:
  • Name of type constructor "Constraint" replaced by "Success", i.e., a constraint is now a function with result type "Success".
  • The old pragma "optmatch" has been omitted and this is now the default strategy.
  • Sect. 2.1: Restriction on arities in applications omitted since this is not intended in higher-order functions like twice. Actually, current implementations of Curry already dropped this restriction.
  • Sect. 4.1: Tuple constructors defined as "(,...,)" to be compatible with Haskell.
  • Sect. 4.2: Precise definition of type expressions added so that it is clear that partial type constructor applications are not allowed.
  • New Section 11 about literate programming included.
  • Appendix D.6: Description of optmatch strategy for generating definitional trees added.
  • Appendix D.8: Elimination of local patterns corrected: a local let should not be moved to the top-level before eliminating it, otherwise there are problems with let's in branches of conditionals.
• Version 0.6 of October 22, 1999
  Changes to the previous version:
  • Section 2.6: Footnote about instantiation of unbound functional variables added.
  • Section 4.2: Typing rules for existentials and defining equations corrected.
  • Section 5: Definition of module system changed so that it is almost compatible with Haskell (e.g., renaming is replaced by qualification and hiding)
  • Section 10: Command ":type" shows the type of an expression instead of a function
  • Appendix B: standard prelude extended (const, /=, lines, unlines, either, maybe,...)
  • Syntax: bugs w.r.t. infix operators and unary minus corrected
  • Syntax: module syntax slightly changed, list of keywords updated Changes: qualified infix operators allowed, renaming is replaced by qualification and hiding
  • Appendix D: "pattern" replaced by "call pattern" to avoid confusion with patterns in the syntax of Curry (which are defined as expressions without defined functions).
  • Typo in Figure 3 corrected.
  • Section 2.2.1 and Appendix D.2: Explanation of sharing made more precise.
  • Appendix D: Section about the elimination of local declarations (let/where) included. This lifting of local declarations is necessary to explain the operational semantics and the type system of the entire language. Concrete implementations are free to choose other techniques if they are conform with this specification.
• Draft of January 13, 1999
  Changes to the previous version:
  • Section 2.2.2: special case of single Boolean guard removed.
  • Section 2.4:
    • implicit declarations of free variables deleted (see email of January 7, 1999)
    • discussion of mutally recursive "free" declarations added
  • Section 4.1: explanation added that "predicates" in the logic programming sense should be considered as constraints rather than Boolean functions in Curry.
  • Section 4.2: Definition of well-typed programs added by means of typing rules.
  • Section 10: ".curry" defined as the standard extension for loading Curry programs and full command names for the interactive environment added.
  • Some fixity declarations in the prelude corrected.
  • Section B (Prelude):
    • function "tryone" (cf. Section 7.4) added since it is necessary to define search operator "one"
    • "unpack" modified so that it extracts only a single search goal (the previous "unpack" on lists is now equivalent to "map unpack")
  • Section C.1:
    • Characters "\:" added to valid OpID characters
    • Keywords of Curry defined
  • Section C.3:
    • rules for type expressions and patterns corrected (for compatibility with Haskell)
    • order in function declarations relaxed: signature, eval annotation and equations can come in any order
    • Expression syntax extended (sections and unary minus included)
  • Section C.4 about handling of infix operators added.
  • Section D.2: evaluation of conditional rules directly integrated in the operational semantics of Curry. Thus, Section D.3 is deleted since the special handling of conditional rules by a syntactic transformation caused some confusion.
  • Section D.4: Inference rule 6 for solving equational constraints corrected.
• Draft of November 23, 1998
  Changes to the previous version:
  • Constraints are expressions from a syntactic point of view, i.e., the curly brackets around constraints are omitted.
  • The symbol "=:=" is used for unification, i.e., the unification of two expressions e1,e2 is written as "e1 =:= e2" instead of "e1 = e2". The use of "=" for unification was originally intended to be conform with unification in Prolog but causes some trouble in the context of a Haskell syntax. On the other hand, the use of "=:=" for unification can be also seen as conform with Prolog since the ISO standard uses "=:=" for arithmetic equality (including the evaluation of both sides) and several Prolog systems uses this symbol for equational constraints.
  • The concurrent conjunction is written with the infix operator "&" and "success" denotes the always satisfiable constraint. Moreover, the sequential conjunction of constraints ("&>") is added to the prelude.
  • In expressions of the form "let x1,...,xn free in c", c must be an expression of type "Constraint".
  • The scoping rules for implicitly declared extra-variables have been simplified (Section 2.4). Since constraints are no longer syntactically distinguishable from other expressions, the "smallest constraint enclosing an expression" is not directly recognizable. Therefore, all extra-variables (identifiers starting with an underscore) in a rule are now always considered as declared at the top-level of the condition.
  • In conditional rules of the form "l | c = r", the condition c is an expression of type "Constraint".
    In order to be compatible with Haskell, we allow the following syntactic sugar:
    • a rule of the form "l | b = r" where b is of type "Bool" is considered as an abbreviation for "l | b=:=True = r"
    • a rule with multiple guards of Boolean type, i.e.,

               l | b1 = r1
                 | b2 = r2
                 ...
                 | bn = rn
      

      where each bi has type "Bool", is considered as an abbreviation for

               l = if b1 then r1 else
                   if b2 then r2 else
                   ...
                   if bn then rn else undefined
      

      (where "undefined" is a non-reducible function). This means that Booleans guards have a sequential reading rather than a parallel one which is reasonable for constraints. For convenience, the function "otherwise" (=True) is predefined.
  • Note that this has a subtle consequence for the type inference. In contrast to Miranda or Haskell, the type inferencer cannot assume that the guard has always type Bool, but it must type

          l | g1 = r1
            | ...
            | gn = rn
    

    by typing each gi separately without any further assumptions, yielding type ti for gi. After that, all ti must be unifiable to either "Constraint" (default case) or "Bool". Thus, a mixture between Constraint and Bool guards is not allowed (see Section 2.2.2).
  • Defaults for flex/rigid: Functions of type "Constraint" (previously: Bool) are flexible, all others are rigid by default. There are reasonable arguments for this default and it also simplifies the use of encapsulated search (where Constraint functions are assumed to be the source of non-determinism).
  • The choice construct is deleted. Instead of this committed choice, there is a new evaluation annotation "choice" which declares a function as a committed choice function. For instance, the indeterministic merge can be defined as follows:

        merge eval choice
        merge [] l2    = l2
        merge l1 []    = l1
        merge (e:r) l2 = e : merge r l2
        merge l1 (e:r) = e : merge l1 r
    

    This definition is simpler and really lazy in contrast to the old use of the "choice" construct. The following operational behavior for a function call with evaluation annotation "choice" is informally defined as follows:
    Evaluate this function call as usual (with a fair evaluation of alternatives) but
    • do not bind variables occurring in this call
    • ignore all alternatives if one rule matches and its guard is entailed (i.e., satisfiable without binding goal variables)
    The first restriction is similar to the rigid annotation but requires a rigid evaluation also for all subcalls (as in the old "choice"). Thus, the new evaluation annotation has the same power as the old "choice" construct but avoids the special syntax and scoping rules in the "choice".
  • A clarification about the role of variables and functions w.r.t. sharing introduced (2.2.1). In Section 2.3 it is added that local variable declarations are considered as those and not as 0-ary functions. End of Section D.2: Remark about the necessity of sharing added.
• Draft of June 29, 1998
  Changes to the previous version:
  • Evaluation annotations simplified: only rigid or flex are still allowed, the more complicated tree annotations are omitted.
  • Grammar slightly corrected.
  • Description of the layout rules inserted (Section C.2).
• Draft of February 2, 1998
  Changes to the previous version:
  • and alternatives in evaluation annotations dropped, i.e., concurrent evaluation is expressed through concurrent conjunction of constraints, which seems enough in practice and is also used in Goffin or Oz.
  • Section 2.3 on local declarations (describing let and where) added.
  • Section 2.4 on free variables added. Free variables can be declared similarly to other local objects by let and where declarations.
  • Section 2.5 on constraints and equality updated (in particular, references to the internal constant Valid dropped and and evaluation annotations omitted).
  • Section 3 on the operational semantics simplified (usually, only the evaluation annotations flex and rigid are important; thus, the explanation of the other more specialized annotations has been moved into the appendix).
  • Section 5 on the module system added.
  • Section 7 describing the encapsulated search facilities added.
  • Pragmas (Section 9) slightly modified.
  • Prelude updated.
  • Syntax updated.
  • Operational semantics (Appendix D) updated according to the new features (equational constraints, concurrent conjunction, encapsulated search).
• Draft of June 6, 1997
  Changes to the previous version:
  • equational constraints and concurrent conjunction introduced
  • restriction to confluent programs dropped, i.e., non-deterministic functions are allowed, but sufficient criteria to ensure "well-definedness" of functions in the traditional sense are given
  • meaning of committed choice modified (now it is compatible with concurrent constraint languages)
  • Prelude added
  • Syntax added
• Draft of January 10, 1997
  Changes to the previous version: syntax made compatible with Haskell
• Draft of December 5, 1996
  This was the first proposal