Understanding Haskell function in a lambda calculus way

Question

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

What helper are you talking about? filter' is filter. This is just a straightforward recursive function, with filter' calling itself on the tail of its list input. — chepner
– chepner, Commented Dec 25, 2018 at 19:37
@chepner I think helper is the function given to filter. filter' is used to distinguish it from the real filter. — schuelermine
– schuelermine, Commented Dec 26, 2018 at 0:10
@MarkNeu He talks about the helper function evaluating a, which is the predicate passed to filter. — chepner
– chepner, Commented Dec 28, 2018 at 2:44

bergey · Accepted Answer · 2018-12-25 22:05:14Z

2

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".

answered Dec 25, 2018 at 22:05

bergey

3,10113 silver badges17 bronze badges

Sign up to request clarification or add additional context in comments.

4 Comments

Jung Over a year ago

Why does f doesnt have the type a -> [a] -> Bool because it would make more sense to evaluate the predicate a on list [a]. Its illogical that a on itself can be determined as True or False, isnt it? The filter' function also takes in a list (second parameter) to give back a list. Is the first [a] in the type denotation xs and the second [a] represents x:filter' f xs. Thanks a lot. I find your explanation most comprehensible.

bergey Over a year ago

In every Haskell function type signature, the part after the last arrow is the result of the function. Here, the second [a] is the result - the list of elements for which the predicate is True. This filter' is the same as filter in the standard library. It works for predicates on single elements. For example, filter even or filter (not . null). This is also efficient - the function considers each a exactly once.

Jung Over a year ago

I think you have missed my point. i understand that the second [a] is the result filter' f (x:xs) | f x == True = x:filter' f xs What i dont get is the fourth line, we already have the function f and x as a in (a-> Bool) but im not sure where the first [a] is implemented.

bergey Over a year ago

The second argument to filter has the type [a]. This list matches either [] or (x:xs). The line filter _ [] = [] defines what to do if passed the empty list. The 3 lines beginning filter f (x:xs) defines what to do if passed a non-empty list, and bind the two variables x and xs. These two cases cover all possible lists.

Will Ness · Accepted Answer · 2018-12-26 08:30:34Z

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])

Collectives™ on Stack Overflow

Understanding Haskell function in a lambda calculus way

2 Answers 2

4 Comments

Comments

Your Answer

Hot Network Questions

Collectives™ on Stack Overflow

2 Answers 2

4 Comments

Comments

Your Answer

Sign up or log in

Post as a guest

Related