You’re going to mess up if you use Haskell like this. That’s because you’re lacking proof irrelevance. You cannot do it properly until you solve two issues. The first issue is the unrestricted recursion with no access to induction principle or other well-formed recursion. The second issue is that your types are not specific enough to do this.

Programs that prove the type (a -> b -> b) -> b -> [a] -> b:

Take only the second argument and return it: (f ↦ b ↦ list ↦ b)

Apply partially to the list: (f ↦ b ↦ list ↦ case list of nil → b | cons a r → f a b)

Variations of the previous form.

Apply entirely to the list: (fix (rep ↦ f ↦ b ↦ list ↦ case list of nil → b | cons a r → rep f (f a b) r))

Apply entirely to the list in a different way: (fix (rep ↦ f ↦ b ↦ list ↦ case list of nil → b | cons a r → f a (rep f b r)))

Apply three times to the first element: (f ↦ b ↦ list ↦ case list of nil → b | cons a r → (f a (f a (f a b))))

Abuse of the recursion fix (x ↦ x)

Applying the technique described in the post reveal you one or more of these implementations. One of them is foldr. But you see you also get foldl with arguments flipped there. They are quite different programs that you can verify by giving it a non-commutative non-associative function, eg. zoop4 (-) vs. zoop5 (-) then examine the results. Eg. rep (-) (a2 - (a1 - b)) r vs. a1 - (a2 - (rep (-) b r))

If your type signature is wrong, eg. say you are trying this with b -> [a] -> b, then you’re not going to find foldr among the results. But you still find all the wrong implementations.

Now lets imagine that you’d have a type that describes foldr, then the only proof for it would be the: (fix (rep ↦ f ↦ b ↦ list ↦ case list of nil → b | cons a r → f a (rep f b r))). If you didn’t have all the pieces you wouldn’t get it solved. This would be a reliable way to write software, especially if you restrict the use of fix somehow.

How would you define a type that can be only proven by implementing foldr?

You’re going to mess up if you use Haskell like this. That’s because you’re lacking proof irrelevance. You cannot do it properly until you solve two issues. The first issue is the unrestricted recursion with no access to induction principle or other well-formed recursion. The second issue is that your types are not specific enough to do this.

Programs that prove the type

`(a -> b -> b) -> b -> [a] -> b`

:`(f ↦ b ↦ list ↦ b)`

`(f ↦ b ↦ list ↦ case list of nil → b | cons a r → f a b)`

`(fix (rep ↦ f ↦ b ↦ list ↦ case list of nil → b | cons a r → rep f (f a b) r))`

`(fix (rep ↦ f ↦ b ↦ list ↦ case list of nil → b | cons a r → f a (rep f b r)))`

`(f ↦ b ↦ list ↦ case list of nil → b | cons a r → (f a (f a (f a b))))`

`fix (x ↦ x)`

Applying the technique described in the post reveal you one or more of these implementations. One of them is

`foldr`

. But you see you also get`foldl`

with arguments flipped there. They are quite different programs that you can verify by giving it a non-commutative non-associative function, eg.`zoop4 (-)`

vs.`zoop5 (-)`

then examine the results. Eg.`rep (-) (a2 - (a1 - b)) r`

vs.`a1 - (a2 - (rep (-) b r))`

If your type signature is wrong, eg. say you are trying this with

`b -> [a] -> b`

, then you’re not going to find`foldr`

among the results. But you still find all the wrong implementations.Now lets imagine that you’d have a type that describes

`foldr`

, then the only proof for it would be the:`(fix (rep ↦ f ↦ b ↦ list ↦ case list of nil → b | cons a r → f a (rep f b r)))`

. If you didn’t have all the pieces you wouldn’t get it solved. This would be a reliable way to write software, especially if you restrict the use of`fix`

somehow.How would you define a type that can be only proven by implementing

`foldr`

?