Curry programming language
Encyclopedia
Curry is an experimental functional
logic
programming language
, based on the Haskell
language. It merges elements of functional and logic programming, including constraint programming
integration.
It is nearly a superset of Haskell, lacking support mostly for overloading using type classes, which some implementations provide anyway as a language extension, such as the Münster Curry Compiler.
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 subexpression to be replaced are quoted):
'double (1+2)' → '(1+2)'+(1+2) → 3+'(1+2)' → '3+3' → 6
There is also another order of evaluation if we replace the arguments of operators from right to left:
'double (1+2)' → (1+2)+'(1+2)' → '(1+2)'+3 → '3+3' → 6
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 the reasoning about and maintenance of pure functional programs.
Functional logic programs, however, are not always referentially transparent. Encapsulated searches can depend on the order of evaluation.
As 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:
data Bool = True | False
Functions on Booleans can be defined by pattern matching, i.e., by providing several equations for different argument values:
not True = False
not False = 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 “e:l” consisting of a first element e and a list l:
data List a = [] | a : List a
The type “List a” is usually written as [a] and finite lists e1:e2:...:en:[] are written as [e1,e2,...,en]. 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 l and elements e, last l = e iff ∃xs:xs++[e] = l.
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 xs++[e] = [1,2,3] is solved by instantiating xs to the list [1,2] and e to the value 3. In Curry one can define the operation last as follows:
last l | xs++[e] =:= l = e where xs,e free
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.
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 previous 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. 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 programming
In computer science, functional programming is a programming paradigm that treats computation as the evaluation of mathematical functions and avoids state and mutable data. It emphasizes the application of functions, in contrast to the imperative programming style, which emphasizes changes in state...
logic
Logic programming
Logic programming is, in its broadest sense, the use of mathematical logic for computer programming. In this view of logic programming, which can be traced at least as far back as John McCarthy's [1958] advice-taker proposal, logic is used as a purely declarative representation language, and a...
programming language
Programming language
A programming language is an artificial language designed to communicate instructions to a machine, particularly a computer. Programming languages can be used to create programs that control the behavior of a machine and/or to express algorithms precisely....
, based on the Haskell
Haskell (programming language)
Haskell is a standardized, general-purpose purely functional programming language, with non-strict semantics and strong static typing. It is named after logician Haskell Curry. In Haskell, "a function is a first-class citizen" of the programming language. As a functional programming language, the...
language. It merges elements of functional and logic programming, including constraint programming
Constraint programming
Constraint programming is a programming paradigm wherein relations between variables are stated in the form of constraints. Constraints differ from the common primitives of imperative programming languages in that they do not specify a step or sequence of steps to execute, but rather the properties...
integration.
It is nearly a superset of Haskell, lacking support mostly for overloading using type classes, which some implementations provide anyway as a language extension, such as the Münster Curry Compiler.
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 regards 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 bydouble 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 subexpression to be replaced are quoted):
'double (1+2)' → '(1+2)'+(1+2) → 3+'(1+2)' → '3+3' → 6
There is also another order of evaluation if we replace the arguments of operators from right to left:
'double (1+2)' → (1+2)+'(1+2)' → '(1+2)'+3 → '3+3' → 6
In this case, both derivations lead to the same result, a property known as confluence
Confluence (term rewriting)
In computer science, confluence is a property of rewriting systems, describing that terms in this system can be rewritten in more than one way, to yield the same result. This article describes the properties in the most abstract setting of an abstract rewriting system.- Motivating example :Consider...
. 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 the reasoning about and maintenance of pure functional programs.
Functional logic programs, however, are not always referentially transparent. Encapsulated searches can depend on the order of evaluation.
As functional languages like Haskell
Haskell (programming language)
Haskell is a standardized, general-purpose purely functional programming language, with non-strict semantics and strong static typing. It is named after logician Haskell Curry. In Haskell, "a function is a first-class citizen" of the programming language. As a functional programming language, the...
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:
data Bool = True | False
Functions on Booleans can be defined by pattern matching, i.e., by providing several equations for different argument values:
not True = False
not False = 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 “e:l” consisting of a first element e and a list l:
data List a = [] | a : List a
The type “List a” is usually written as [a] and finite lists e1:e2:...:en:[] are written as [e1,e2,...,en]. 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 l and elements e, last l = e iff ∃xs:xs++[e] = l.
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 xs++[e] = [1,2,3] is solved by instantiating xs to the list [1,2] and e to the value 3. In Curry one can define the operation last as follows:
last l | xs++[e] =:= l = e where xs,e free
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 boundName binding
In programming languages, name binding is the association of objects with identifiers. An identifier bound to an object is said to reference that object. Machine languages have no built-in notion of identifiers, but name-object bindings as a service and notation for the programmer is implemented...
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 previous 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. 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
SLD resolution
SLD resolution is the basic inference rule used in logic programming. It is a refinement of resolution, which is both sound and refutation complete for Horn clauses.-The SLD inference rule:...
strategy of Prolog
Prolog
Prolog is a general purpose logic programming language associated with artificial intelligence and computational linguistics.Prolog has its roots in first-order logic, a formal logic, and unlike many other programming languages, Prolog is declarative: the program logic is expressed in terms of...
.
External links
- Curry - The home page of Curry
- MCC - The Münster Curry Compiler, which uses CC (programming language)C is a general-purpose computer programming language developed between 1969 and 1973 by Dennis Ritchie at the Bell Telephone Laboratories for use with the Unix operating system....
as the target - PAKCS A major Curry implementation with a WWW interface, which uses Prolog as the target
- KiCS A Curry implementation, which uses HaskellHaskell (programming language)Haskell is a standardized, general-purpose purely functional programming language, with non-strict semantics and strong static typing. It is named after logician Haskell Curry. In Haskell, "a function is a first-class citizen" of the programming language. As a functional programming language, the...
as the target - Curry Mailing List
- Michael Hanus's home page
- Purely Functional Lazy Non-deterministic Programming, Transforming Functional Logic Programsinto Monadic Functional Programs on modeling lazy non-deterministic (logic) programming (like in Curry) in a purely functional language (HaskellHaskell (programming language)Haskell is a standardized, general-purpose purely functional programming language, with non-strict semantics and strong static typing. It is named after logician Haskell Curry. In Haskell, "a function is a first-class citizen" of the programming language. As a functional programming language, the...
); such approach might give the programmer more flexibility in the control over the strategies that, in the case of Curry, are built-in.