4 ms·
So let me see if I follow the definition of append there, using Fexl notation which doesn't use pattern matching (all data items such as lists are just function
by fexl 17y ago
So let me see if I follow the definition of append there, using Fexl notation which doesn't use pattern matching (all data items such as lists are just functions applied normally).
Here's the fold function:
\fold = (\func\val\list list val \head\tail func head (fold func val tail))
And here's the traditional definition of append, not using fold:
\append = (\xs\ys xs ys \head\tail cons head (append tail ys))
The article alleges that append can be defined in terms of fold as:
\append = (\xs\ys fold cons ys xs)
So now I'll try to prove the equivalence as follows.
: append xs ys
= fold cons ys xs
= (\func\val\list list val \head\tail func head (fold func val tail)) cons ys xs
= \func=cons \val=ys \list=xs list val \head\tail func head (fold func val tail)
= xs ys \head\tail cons head (fold cons ys tail)
= xs ys \head\tail cons head (append tail ys)
Looks right!