我将一步一步地对你的例子进行评估：

insert' :: Ord a => a -> [a] -> [a]
insert' x = foldr insx [x]
  where
    insx y ys@(z:zs) | z==x && x<y = z:y:zs
                     | otherwise   = y:ys

insert' 6 [5, 7, 8]等效于(insert' 6) [5, 7, 8]，因为函数应用程序关联到左侧。
根据insert'的定义，insert' 6等于foldr insx [6]，其中x = 6。
这就是所谓的 * eta-约简 *，以lambda演算中的“eta规则”命名，基本上它的意思是，如果你有一个函数，它可以这样写：

f x = g x

其中g是某个表达式，如果g不包含x，则可以将其简化为f = g，因为f只是沿着其参数直接传递给g。例如：

add x y = x + y

-- by definition of infix operators:
add x y = (+) x y

-- by left-association of function application:
add x y = ((+) x) y

-- eta-reduce:
add x   = (+) x

-- eta-reduce again:
add     = (+)

因此，Int -> Int -> Int类型的“双参数”定义也可视为单参数定义（返回单参数函数Int -> (Int -> Int)）或零参数定义（一个变量），它是一个“双参数”函数(Int -> Int -> Int)。关键是 * 所有函数实际上只有一个参数 *，我们只是有一些多参数函数链的语法糖。
所以你的例子中的整个表达式等于(foldr insx [6]) [5, 7, 8]。因为函数应用是左结合的，括号是多余的，所以这和foldr insx [6] [5, 7, 8]是一样的。所以foldr在这里是完全应用的。
foldr的评估然后扩展为以下内容：

insx 5 (insx 7 (insx 8 [6]))

你可以扩展insx的定义，使其适用于每一种参数组合，我将从最右边的insx调用开始，即insx 8 [6]，它在列表语法上等价于insx 8 (6:[])。
根据定义，第一个守卫是，因此结果是z:y:zs = 6:8:[] = [6, 8]。
最右边的调用insx 7 [6, 8]设置y = 7，ys = [6, 8]，z = 6，以及zs = [8]。守护函数的值为6 == 6 && 6 < 7，这也是真的，给出6:7:[8] = [6, 7, 8]。
最后我们得到insx 5 [6, 7, 8]。现在y = 5，ys = [6, 7, 8]，z = 6，以及zs = [7, 8]。保护函数是6 == 6 && 6 < 5，它是 false，所以我们继续下一个保护函数。otherwise总是true，所以我们返回y:ys = 5:[6, 7, 8] = [5, 6, 7, 8]。
注意我们总是有z == x;作为一个练习，试着通过一个示例输入，其中条件的这一部分在计算过程中的某个点评估为假。
您可以使用任何类型的值作为foldr的“accumulator”参数，在本例中它是一个列表。具体来说，foldr具有以下类型：

foldr :: Foldable t => (a -> b -> b) -> b -> t a -> b

专门指定为t = []，因为 input 是一个列表，即：

foldr :: (a -> b -> b) -> b -> [a] -> b

在你的例子中，它被进一步特殊化为b = [a]，因为 output 也是一个相同类型的列表：

foldr :: (a -> [a] -> [a]) -> [a] -> [a] -> [a]

a -> [a] -> [a]参数用insx填充，初始累加器是[x] = [6]，结果是函数[a] -> [a]，然后将其应用于输入[5, 7, 8]。并且由于类型类约束，a可以是集合Num和Ord中的任何类型。例如X1 M80 N1 X或X1 M81 N1 X。

TDD和逐步细化可用于理解此程序的作用，如下所示：

insert' :: Ord a => a -> [a] -> [a]
f y []                 = [y]
-- Follows to:
f y (z:[]) | (y <= z)  = y : z : []
           | otherwise = z : y : []
-- Follows to:
f y (z:zs) | (y <= z)  = y : z : zs
           | otherwise = z : y : zs
-- Follows to:
insert' y = foldr f [y]
   where
   f y ys@(z:zs) | (y <= z)  = y : ys
                 | otherwise = z : y : zs
-- Follows to:
insert' x = foldr insx [x]
  where
    insx y ys@(z:zs) | z==x && x<y = z:y:zs
                     | otherwise   = y:ys