Content deleted Content added
Plankalkuel (talk | contribs) |
|||
Line 58:
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 <tt>a</tt>), is either the empty list “<tt>[]</tt>” or the non-empty list “<tt>e:l</tt>” consisting of a first element <tt>e</tt> and a list <tt>l:</tt>
data List a = [] | a : List a
The type “<tt>List a</tt>” is usually written as <tt>[a]</tt> and finite lists e1<tt>:</tt>e2<tt>:</tt>...<tt>:</tt>en<tt>:[]</tt> are written as <tt>[</tt>e1<tt>,</tt>e2<tt>,</tt>...<tt>,</tt>en<tt>]</tt>. 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 “<tt>++</tt>” on polymorphic lists can be defined as follows (the optional type declaration in the first line specifies that “<tt>++</tt>” 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 “<tt>++</tt>” 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, <tt>last</tt> l = e iff ∃xs<tt>:</tt>xs<tt>++[</tt>e<tt>]</tt> = 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<tt>++[</tt>e<tt>]</tt> = <tt>[1,2,3]</tt> is solved by instantiating xs to the list <tt>[1,2]</tt> and e to the value <tt>3</tt>. In Curry one can define the operation last as follows:
last l | xs++[e] =:= l = e where xs,e free
Here, the symbol “<tt>=:=</tt>” 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 “<tt>where...free</tt>” in order to provide some opportunities to detect bugs caused by typos. A conditional equation of the form l <tt>|</tt> c <tt>=</tt> 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===
| |||