Checker for the derivatives of `(λx(x x) λx(x x))`

[steinerkelvin]

If a lambda that clones its argument is itself cloned, then its clones aren't allowed to clone each-other.

See https://github.com/Kindelia/HVM/issues/44 for more information, as well as the superposed duplication section on HOW.md.

Example of what is not allowed:

let f = λs λz (s (s z)) # a lambda that clones its argument
let g = f               # a clone of that lambda
(g f)                   # the clone will clone the original

[nothingnesses]

@quleuber Where would be a good place to add this check? I'm thinking either in rulebook::sanitize_rule or builder::build_dynfun, but what do you think?

[ken-okabe]

@nothingnesses Is this the first type-checker in HVM? If my understanding is correct, I wish it will be designed for future enhancement.

[Ekdohibs]

For information, some terms a lot more natural than (λx(x x) λx(x x)) are forbidden as well, for instance (Map l1 (λf(Map l2 f))) (however, (Map l1 (λl2(Map l2 f))) is allowed and very common in functional programs, so the distinction to be made will have to be subtle).

[VictorTaelin]

Why do you think (Map l1 (λf(Map l2 f))) is forbidden?

[Ekdohibs]

Because it breaks the "clones must not clone their own clone" rule and produces incorrect results, see the comment in the other thread.

[VictorTaelin]

@Ekdohibs it doesn't! But I see HVM can't reduce it now. That is actually due to a temporary HVM's limitation (it isn't generating labels for rhs dups), but this program doesn't actually hit the cloning limit (not even close). It is a relatively easy fix that should be patched in a few days.

[Andrew-Fryer]

Hi! I'm really interested in this, but am still trying to understand this entirely. I'm taking a grad course on semantics for programming languages and would love to do my final project on HVM. I don't see any good first issue right now, but in the future please tag me :smile:

[VictorTaelin]

This is a very complex subject though, definitely not a good "first issue". We plan to make this repo more contribution friendly soon! Now if you do want a PhD-level challenge, let me know and I can give you pointers on how this could be done.

[Andrew-Fryer]

@VictorTaelin I caught that :laughing: I'm going to at least get my head around builder.rs and maybe have a chat with my prof first. Thanks!

[lukaszlew]

The algorithm is described here: https://arxiv.org/pdf/cs/0305011

Appendix has a good example of type checking, although the term there does not type check.

In general though HVM could handle ALL lambda terms by inserting Lamping level-changing terms very very rarely in the places where the Coppola type checking algorithm proves it is necessary.

[VictorTaelin]

@lukaszlew yep, that sounds like an awesome approach. I think that paper is too restrictive though, since it only allows EAL-typeable terms. There are many, even simple, terms that aren't EAL typeable yet are perfectly fine.