Lecture 4: Natural Recursion

Recall our description of natural recursion on lists from Lecture 2:

One way to think of this is that we'll take a constructed term (e.g., a list), and replace each of the constructors one-for-one with a function. For example, consider the pedantic form of the list [1..5],

1 : (2 : (3 : (4 : (5 : []))))

If we want to sum the numbers from 1 through 5, we can imagine replacing each : in the list structure by a +, and [] by 0, i.e.,

1 : (2 : (3 : (4 : (5 : [])))) ↓ ↓ ↓ ↓ ↓ ↓ 1 + (2 + (3 + (4 + (5 + 0))))

If we generalize away from the specifics of addition and zero, we arrive at the general purpose recursive definition function for lists, traditionally known as foldr, for “fold right”:

foldr combiner base [] = base foldr combiner base (x:xs) = combiner x (foldr combiner base xs)

The foldr function can be used to give concise definitions of other standard functions, e.g.,

sum = foldr (+) 0 filter p = foldr p' [] where p' x xs = if p x then x:xs else xs

(Note that ghc 8.0.1 complains about these definitions -- an issue that we can fix by adding appropriate types.)

There are a few new things here:

This is, by the way, a very common use of where, i.e., setting up a definition of a special-purpose function to pass as an argument to one of the standard higher-order functions. Note that we didn't ask you to note the $\eta$-reduced first line ;-).

Exercise 4.1 Give an alternative definition of filter, based on the definition above, using guarded equations rather than an if ... then ... else ... to implement the locally defined p'.

*Exercise 4.2 Provide foldr-based implementations of product and map.

Standard Functions

There are a number of extremely useful list-manipulation functions to be found in the Prelude (and more still in Data.List). We'll point specifically to

Many of these functions can be implemented by natural recursions over list structure, although a common technique involves creating a local function with addition “register” variables, e.g., consider

import Prelude hiding ((!!)) (!!) :: [a] -> Int -> a xs !! n | n < 0 = error "(!!): negative index" | otherwise = step xs n where step [] _ = error "(!!): index too large" step (a:_) 0 = a step (_:as) n = step as (n-1)

Let's take this apart, beginning with the import statement. Haskell's Prelude is included by default. Unfortunately, if we're doing the school exercise of re-implementing standard Prelude functions, but then our new definitions will clash with the old ones. There are a few workarounds:

We can (and usually do) use infix notation when defining infix functions, as we do here, but that their type ascriptions all follow a prefix form.

In doing indexing, we have to account for two erroneous possibilities:

We encounter these two possibilities at different times, but we'll deal with them in a similar way: by calling the error function, which raises an exception that is caught by the top-level read-eval-print loop.

The “heavy lifting” is done by the step function, which does lock-step natural recursions on the list structure of original argument, and the inductive (Peano) structure of the index as a natural number, in effect, doing a “count-down” to find the result.

An alternative approach is to use the zip function to create a list that embodies that countdown, and then to do a simple natural recursion on that list:

(!!) :: [a] -> Int -> a xs !! n | n < 0 = error "(!!): negative index" | otherwise = search $ zip [n,n-1..] xs where search [] = error "(!!): index too large" search ((0,a):_) = a search (_:as) = search as

Exercise 4.3 Implement concat by a naïve natural recursion, and via foldr. Which implementation is used by GHC? (Hint: follow the source link from the haddock documentation for concat.)

Recursive Algebraic Data Types

Consider the following recursive data structure, which is intended to describe a finite function from keys of type String to values of type Int:

data Bindings = None | Bind String Int Bindings

Yes, there are other ways to do this, but let's stick with this representation.

To manipulate this data structure, we'll use two functions: bind and lookup. First, and most simply, let's consider lookup:

lookup :: String -> Bindings -> Int lookup _ None = error "value: key is not bound." lookup key (Bind k v bs) | k == key = v | otherwise = lookup key bs

This is a classic natural recursion, in which the function calls itself on a constituent of it's argument (bs), which has the same type, albeit only along the computational path where the immediate lookup (at the current binding) fails.

The setup function is a bit trickier. We can implement this naïvely via:

bind :: String -> Int -> Bindings -> Bindings bind key value bs = Bind key value bs

or even $\eta$-reduce three times obtaining:

bind = Bind

This works, but if we build a Binding that involves multiple bindings of the same key, we may find our lookup function runs unnecessarily slowly. So we'll approach this somewhat differently, looking for a binding we can alter.

bind :: String -> Int -> Bindings -> Bindings bind key value None = Bind key value None bind key value (Bind k v bs) | k == key = Bind key value bs | otherwise = Bind k v (bind key value bs)

*Exercise 4.4 A simple approach to the problem of building a finite function from keys of type String to values of type Int is to compose lists and tuples:

type Bindings = [(String,Int)]

In effect, using the tuple to associate a key with a value, all contained in a recursive list structure.

Implement bind and lookup using this list representation. Note that there is a pre-existing version of lookup defined in the Prelude which will need to be hidden, which has a slightly different type associated with a different approach to handling missing-key errors.