[Question] Doesn't Fold from README.md duplicate its function-argument?

[Heimdell]

The Fold:

// Folds over a list
(Fold  Nil        c n) =  n
(Fold (Cons x xs) c n) = (c x (Fold xs c n))

The 2:

let g = λf(λx(f (f x)))
(g g)

How is it possible that (g g) is a no-no, but the Fold, supposedly, is able to be used twice?

P.S.: Are the following scenarios possible and correct:

1. (Fold lst (\x y. ... (Fold ...) ...) 5);
2. (Fold lst Plus (... (Fold ...) ...))?

The limitation seem to be there to prevent 2 non-annihilating Dup nodes to go one through another and becoming 4, isn't it?

[VictorTaelin]

(g g) is not a no-no! It is fine and very useful. What is not fine is g g when g is itself a function that has g g. Like, this is okay: (λg(g g) λg g), but this is not okay: (λg(g g) λg(g g)). The Fold function just uses the c argument twice, which is even-more-okay than g g, since c isn't applied itself. So, if we rank terms based on how much they stress HVM's cloning limits, we have:

1. (λx(x) λx(x)) (completely linear, so ez)

2. (λx(Pair x x) λx x) (non-linear, but not self-applying... acceptable)

3. (λx(x x) λx x) (non-linear and self-applying, but nothing else... that hurts, but we're fine)

4. (λfλx(f (f x)) λfλx(f (f x))) (okay, we're reaching our limits, but no f f so still okay)

5. (λx(x x) λfλx(f (f x))) (game over, that's too much for us to handle)

On this scale, HVM deals fine with 1-4. Fold is more around 2. And 5 is basically problematic useless stuff. (I challenge anyone to come up with a good example that HVM can't handle, that has any relevant application, or that isn't a contrived way to express a program that just needs to be refactored to not suck.)

[Heimdell]

A-ha, so a function that directly self-apply an argument can't be used twice?

In this case, self-applying stuff like (f f) is a type error in most type systems to begin with.

[VictorTaelin]

It can! For example, this is fine:

let i = λx x
let g = λf (f f)
((g i) (g i))

Here, g is a function that self-applies its argument, and it is used twice. But the clones aren't self-applied. Instead, each clone is applied to λx x, which makes it fine. Since this is too confusing, I've been thinking about some ideas on how to incorporate an "ill clone checker" on HVM, that isn't as restrictive as the old Fm-Core checker.