This article is about the programming language Curry (named in honour of a mathematician and logician). For the mathematician and logician, see Haskell Curry. For the computer science technique, see Currying.
It is nearly a superset of Haskell but does not support all language extensions of Haskell. In contrast to Haskell, Curry has built-in support for non-deterministic computations involving search.
Foundations of functional logic programming
Basic concepts
A functional program is a set of functions defined by equations or rules. A functional computation consists of replacing subexpressions by equal (with regard to the function definitions) subexpressions until no more replacements (or reductions) are possible and a value or normal form is obtained. For instance, consider the function double defined by
double x = x+x
The expression “double 1” is replaced by 1+1. The latter can be replaced by 2 if we interpret the operator “+” to be defined by an infinite set of equations, e.g., 1+1 = 2, 1+2 = 3, etc. In a similar way, one can evaluate nested expressions (where the subexpressions to be replaced are quoted):
In this case, both derivations lead to the same result, a property known as confluence. This follows from a fundamental property of pure functional languages, termed referential transparency: the value of a computed result does not depend on the order or time of evaluation, due to the absence of side effects. This simplifies reasoning about, and maintaining, pure functional programs.
As many functional languages like Haskell do, Curry supports the definition of algebraic data types by enumerating their constructors. For instance, the type of Boolean values consists of the constructors True and False that are declared as follows:
dataBool=True|False
Functions on Booleans can be defined by pattern matching, i.e., by providing several equations for different argument values:
notTrue=FalsenotFalse=True
The principle of replacing equals by equals is still valid provided that the actual arguments have the required form, e.g.:
not '(not False)' → 'not True' → False
More complex data structures can be obtained by recursive data types. For instance, a list of elements, where the type of elements is arbitrary (denoted by the type variable a), is either the empty list “[]” or the non-empty list “x:xs” consisting of a first element x and a list xs:
dataLista=[]|a:Lista
The type “List a” is usually written as [a] and finite lists x1:x2:...:xn:[] are written as [x1,x2,...,xn]. We can define operations on recursive types by inductive definitions where pattern matching supports the convenient separation of the different cases. For instance, the concatenation operation “++” on polymorphic lists can be defined as follows (the optional type declaration in the first line specifies that “++” takes two lists as input and produces an output list, where all list elements are of the same unspecified type):
(++)::[a]->[a]->[a][]++ys=ys(x:xs)++ys=x:xs++ys
Beyond its application for various programming tasks, the operation “++” is also useful to specify the behavior of other functions on lists. For instance, the behavior of a function last that yields the last element of a list can be specified as follows: for all lists xs and elements e, last xs = e if ∃ys:ys++[e] = xs.
Based on this specification, one can define a function that satisfies this specification by employing logic programming features. Similarly to logic languages, functional logic languages provide search for solutions for existentially quantified variables. In contrast to pure logic languages, they support equation solving over nested functional expressions so that an equation like ys++[e] = [1,2,3] is solved by instantiating ys to the list [1,2] and e to the value 3. In Curry one can define the operation last as follows:
lastxs|ys++[e]=:=xs=ewhereys,efree
Here, the symbol “=:=” is used for equational constraints in order to provide a syntactic distinction from defining equations. Similarly, extra variables (i.e., variables not occurring in the left-hand side of the defining equation) are explicitly declared by “where...free” in order to provide some opportunities to detect bugs caused by typos. A conditional equation of the form l | c = r is applicable for reduction if its condition c has been solved. In contrast to purely functional languages where conditions are only evaluated to a Boolean value, functional logic languages support the solving of conditions by guessing values for the unknowns in the condition. Narrowing as discussed in the next section is used to solve this kind of conditions.
Narrowing
Narrowing is a mechanism whereby a variable is bound to a value selected from among alternatives imposed by constraints. Each possible value is tried in some order, with the remainder of the program invoked in each case to determine the validity of the binding. Narrowing is an extension of logic programming, in that it performs a similar search, but can actually generate values as part of the search rather than just being limited to testing them.
Narrowing is useful because it allows a function to be treated as a relation: its value can be computed "in both directions". The Curry examples of the previous section illustrate this.
As noted in the prior section, narrowing can be thought of as reduction on a program term graph, and there are often many different ways (strategies) to reduce a given term graph. Antoy et al.[5] proved in the 1990s that a particular narrowing strategy, needed narrowing, is optimal in the sense of doing a number of reductions to get to a "normal form" corresponding to a solution that is minimal among sound and complete strategies. Needed narrowing corresponds to a lazy strategy, in contrast to the SLD-resolution strategy of Prolog.
Functional patterns
The rule defining last shown above expresses the fact that the actual argument must match the result of narrowing the expression ys++[e]. Curry can express this property also in the following more concise way:
last(ys++[e])=e
Haskell does not allow such a declaration since the pattern in the left-hand side contains a defined function (++). Such a pattern is also called functional pattern.[6] Functional patterns are enabled by the combined functional and logic features of Curry and support concise definitions of tasks requiring deep pattern matching in hierarchical data structures.
Non-determinism
Since Curry is able to solve equations containing function calls with unknown values, its execution mechanism is based on non-deterministic computations, similarly to logic programming. This mechanism supports also the definition of non-deterministic operations, i.e., operations that delivers more than one result for a given input. The archetype of non-deterministic operations is the predefined infix operation ?, called choice operator, that returns one of its arguments. This operator is defined by the following rules:
x ? y = x x ? y = y
Thus, the evaluation of the expression 0? 1 returns 0 as well as 1. Computing with non-deterministic operations and computing with free variables by narrowing has the same expressive power.[7]
The rules defining ? show an important feature of Curry: all rules are tried in order to evaluate some operation. Hence, one can define by
insertxys=x:ysinsertx(y:ys)=y:insertxys
an operation to insert an element into a list at an indeterminate position so that the operation perm defined by
perm[]=[]perm(x:xs)=insertx(permxs)
returns any permutation of a given input list.
Strategies
Due to the absence of side effects, a functional logic program can be executed with different strategies. To evaluate expressions, Curry uses a variant of the needed narrowing strategy which combines lazy evaluation with non-deterministic search strategies. In contrast to Prolog, which uses backtracking to search for solutions, Curry does not fix a particular search strategy. Hence, there are implementations of Curry, like KiCS2, where the user can easily select a search strategy, like depth-first search (backtracking), breadth-first search, iterative deepening, or parallel search.
Related Research Articles
In computer science, functional programming is a programming paradigm where programs are constructed by applying and composing functions. It is a declarative programming paradigm in which function definitions are trees of expressions that map values to other values, rather than a sequence of imperative statements which update the running state of the program.
In programming language theory, lazy evaluation, or call-by-need, is an evaluation strategy which delays the evaluation of an expression until its value is needed and which also avoids repeated evaluations.
ML is a functional programming language. It is known for its use of the polymorphic Hindley–Milner type system, which automatically assigns the data types of most expressions without requiring explicit type annotations, and ensures type safety; there is a formal proof that a well-typed ML program does not cause runtime type errors. ML provides pattern matching for function arguments, garbage collection, imperative programming, call-by-value and currying. While a general-purpose programming language, ML is used heavily in programming language research and is one of the few languages to be completely specified and verified using formal semantics. Its types and pattern matching make it well-suited and commonly used to operate on other formal languages, such as in compiler writing, automated theorem proving, and formal verification.
Prolog is a logic programming language that has its origins in artificial intelligence, automated theorem proving and computational linguistics.
Miranda is a lazy, purely functional programming language designed by David Turner as a successor to his earlier programming languages SASL and KRC, using some concepts from ML and Hope. It was produced by Research Software Ltd. of England and was the first purely functional language to be commercially supported.
Standard ML (SML) is a general-purpose, modular, functional programming language with compile-time type checking and type inference. It is popular for writing compilers, for programming language research, and for developing theorem provers.
Oz is a multiparadigm programming language, developed in the Programming Systems Lab at Université catholique de Louvain, for programming language education. It has a canonical textbook: Concepts, Techniques, and Models of Computer Programming.
In computer science, pattern matching is the act of checking a given sequence of tokens for the presence of the constituents of some pattern. In contrast to pattern recognition, the match usually has to be exact: "either it will or will not be a match." The patterns generally have the form of either sequences or tree structures. Uses of pattern matching include outputting the locations of a pattern within a token sequence, to output some component of the matched pattern, and to substitute the matching pattern with some other token sequence.
In computer programming, especially functional programming and type theory, an algebraic data type (ADT) is a kind of composite type, i.e., a type formed by combining other types.
In computer science, conditionals are programming language commands for handling decisions. Specifically, conditionals perform different computations or actions depending on whether a programmer-defined Boolean condition evaluates to true or false. In terms of control flow, the decision is always achieved by selectively altering the control flow based on some condition . Although dynamic dispatch is not usually classified as a conditional construct, it is another way to select between alternatives at runtime. Conditional statements are the checkpoints in the programme that determines behaviour according to situation.
In computer science, a programming language is said to have first-class functions if it treats functions as first-class citizens. This means the language supports passing functions as arguments to other functions, returning them as the values from other functions, and assigning them to variables or storing them in data structures. Some programming language theorists require support for anonymous functions as well. In languages with first-class functions, the names of functions do not have any special status; they are treated like ordinary variables with a function type. The term was coined by Christopher Strachey in the context of "functions as first-class citizens" in the mid-1960s.
In a programming language, an evaluation strategy is a set of rules for evaluating expressions. The term is often used to refer to the more specific notion of a parameter-passing strategy that defines the kind of value that is passed to the function for each parameter and whether to evaluate the parameters of a function call, and if so in what order. The notion of reduction strategy is distinct, although some authors conflate the two terms and the definition of each term is not widely agreed upon.
In computer programming, append is the operation for concatenating linked lists or arrays in some high-level programming languages.
Tacit programming, also called point-free style, is a programming paradigm in which function definitions do not identify the arguments on which they operate. Instead the definitions merely compose other functions, among which are combinators that manipulate the arguments. Tacit programming is of theoretical interest, because the strict use of composition results in programs that are well adapted for equational reasoning. It is also the natural style of certain programming languages, including APL and its derivatives, and concatenative languages such as Forth. The lack of argument naming gives point-free style a reputation of being unnecessarily obscure, hence the epithet "pointless style".
In computer programming, a pure function is a function that has the following properties:
the function return values are identical for identical arguments, and
the function has no side effects.
In many programming languages, map is a higher-order function that applies a given function to each element of a collection, e.g. a list or set, returning the results in a collection of the same type. It is often called apply-to-all when considered in functional form.
In functional programming, fold refers to a family of higher-order functions that analyze a recursive data structure and through use of a given combining operation, recombine the results of recursively processing its constituent parts, building up a return value. Typically, a fold is presented with a combining function, a top node of a data structure, and possibly some default values to be used under certain conditions. The fold then proceeds to combine elements of the data structure's hierarchy, using the function in a systematic way.
Algebraic Logic Functional (ALF) programming language combines functional and logic programming techniques. Its foundation is Horn clause logic with equality, which consists of predicates and Horn clauses for logic programming, and functions and equations for functional programming.
This article describes the features in the programming language Haskell.
Idris is a purely-functional programming language with dependent types, optional lazy evaluation, and features such as a totality checker. Idris may be used as a proof assistant, but is designed to be a general-purpose programming language similar to Haskell.
↑ Sergio, Antoy; Hanus, Michael (2006). "Declarative Programming with Function Patterns". Logic Based Program Synthesis and Transformation. Lecture Notes in Computer Science. Vol.3901. pp.6–22. doi:10.1007/11680093_2. ISBN978-3-540-32654-0.
↑ Sergio, Antoy; Hanus, Michael (2006). "Overlapping Rules and Logic Variables in Functional Logic Programs". Logic Programming. Lecture Notes in Computer Science. Vol.4079. pp.87–101. doi:10.1007/11799573_9. ISBN978-3-540-36635-5.
This page is based on this Wikipedia article Text is available under the CC BY-SA 4.0 license; additional terms may apply. Images, videos and audio are available under their respective licenses.
