Jung
Jung

Reputation: 139

Understanding Haskell function in a lambda calculus way

Im trying to define the filter function. Based on the function's definition, the filter' function is a function (say help function to differ from the main filter' function) that takes in a function and a list to give a list. The help function takes in a variable and gives back a Bool value. But according the line 4, the help function evaluates a along with [x] to give a Bool Value which then finally gives back a list.

So can I understand the help function as a function that takes in a and [a] to give a Bool value. The main filter' function then takes in this Bool value to give back a list?

Im aware that the function's definition does not suggest this but it's kinda logical based on the code. Thanks

filter' :: (a -> Bool) -> [a] -> [a]
filter' _ [] = []
filter' a (x:xs)
  | a x == True = x:filter' a xs
  | otherwise = filter' a xs

Upvotes: 0

Views: 231

Answers (2)

Will Ness
Will Ness

Reputation: 71119

You can use the syntax even more to aid your understanding:

filter' :: (a -> Bool) -> [a] -> [a]
filter' p [] = []
filter' p (x:xs)
     | (p  x) == True   = x : ( filter' p xs )
     | otherwise        =     ( filter' p xs )

Which is

filter' :: (a -> Bool) -> [a] -> [a]
filter' p [] = []
filter' p (x:xs)
     | (p  x)     = x : ( filter' p xs )
     | otherwise  =     ( filter' p xs )

Or translate it to the more basic constructs,

filter' :: (a -> Bool) 
          ->   [a] -> [a]
filter' p = ( \ xs -> case xs of 
             {  []            ->  []
             ;  (x:ys) | p x  ->  x : ( filter' p ys )
             ;  (x:ys)        ->      ( filter' p ys )  } )

" p" is for "predicate". It is used by filter' to test each x in the input xs, to decide whether to include that x or not in the output, according to the Boolean value that the testing has produced.

p is just passed around unchanged from one invocation of filter' to the next. This is usually coded away with the so called "worker-wrapper" transformation,

filter' :: (a -> Bool) -> [a] -> [a]
filter' p xs = go xs where
   go [] = []
   go (x:xs) | p x   = x : go xs
             | otherwise = go xs

Lastly, a simpler-looking definition could also be

filter' :: (a -> Bool) -> [a] -> [a]
filter' p xs = go xs where
   go []     = []
   go (x:xs) = [x | p x] ++ go xs

which corresponds nicely with the foldMap-based definition

filter' p = foldMap (\ x -> [x | p x])

Upvotes: 2

bergey
bergey

Reputation: 3081

I think this will be clearer if we give the function of type a -> Bool a name other than a.

filter' :: (a -> Bool) -> [a] -> [a]
filter' _ [] = []
filter' f (x:xs)
  | f x == True = x:filter' f xs
  | otherwise = filter' f xs

Now f has type a -> Bool, x :: a, and xs :: [a].

I like your description of (a -> Bool) -> [a] -> [a] as "takes in a function and a list to give a list". The recursive calls to filter' in lines 4 & 5 have the same type. f is passed along unchanged. xs is a list of as, but it's one a shorter than the input list. There is only one function filter'. The definition of the function refers to itself - that's an essential part of what we mean by "recursive function".

Upvotes: 2

Related Questions