HVM

HVM copied to clipboard

HVM produces incorrect results on some inputs, one of which being:

(Main arg) = ((λa (a (λb ((λc (λd (b (c d)))) a)))) (λe (e e)))

On this input, HVM produces the result λx1 λx2 ((x1 x2) (x1 x2)) while the correct result is λx1 λx2 ((x1 x1) (x2 x2)) (as verified by https://crypto.stanford.edu/~blynn/lambda/, with the corresponding input syntax by adding dots after the variable of each lambda: ((λa. (a (λb. ((λc. (λd. (b (c d)))) a)))) (λe. (e e)))).

Besides, on other inputs such as:

((λa λb ((b a) λc λd (λe (d a) a)) λf (f f)) λz z)

HVM produces the result λx1 (x1 λx2 (x2 _)) which is not even well-formed.

This seems to be violating the "clones can't clone their own clones" limitation, explained here. HVM is just a (much) faster functional runtime based on the abstract algorithm, not a full λ-calculator. Attempting to make a clone clone its own clone is considered undefined behavior. I stress that this only happens in highly artificial examples (like these!).

Edit: I now consider HVM should be seen as an Interaction Net runtime that happens to be a suitable as a functional back-end, as long as compatibility is ensured by a type-checker or something equivalent. But there is no such a thing as UB, as these reductions are correct w.r.t. INet semantics. See below for more info.

This limitation should probably be noted in the README. You probably also want to add more information on the limitation to make clear under what situations this is (im)possible. I assume this limitation is impossible to hit if the type system precludes applying a function to itself?

While I agree it is ok if there are limitations, I find it a completely different matter to have limitations and to silently return an incorrect result! Besides, it seems to me that this limitation could be easily violated in a "natural" program such as mapping over a list of lists: map2 f l = map (map f) l. The function map has to clone the function given to it (as it needs to call it several times), but map f contains a clone of map itself!

@L-as yes, but that is still too restrictive. Applying a function to itself is fine (and even usual). For example, the Y-Combinator relies on applying r to itself: Y = λf (λr(f (r r)) λr(f (r r))). That is completely fine. What is not allowed is for a cloned function to apply its own clone to itself. That is a much more rare situation. I'd bet there isn't a single occurrence of this in any of the Rust's top 1000 libraries, for example. There could be a note on the README, but is it really necessary. This, again, is way less restrictive than Rust's borrow checker, so I find it really confusing that people make a big deal of this.

@Ekdohibs map (map f) l is completely fine! As is basically anything you'll come up with in practice. I think this is the main reason people get scared, they don't realize what the limitation really entails!

As to silently failing, that's just like every other undefined behavior, not unlike adding a number and a string, or reading arrays out of bounds. HVM is an untyped compile target, not meant to be a user-facing language. Obviously languages that compile to it will prevent these programs during type checking.

Hmmm, I think I don't understand why map (map f) l is fine, at least if map is a lambda-bound function. (Imagine we are in Haskell and this function map2 is defined for any functor).

Victor gave an example of what isn't allowed on the Telegram channel:

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

He said:

this is a limitation of the runtime and should raise a type error, just like you can't have two concurrent &mut references in Rust

I think people (myself included!) misread the meaning of "a clone cloning its own clone". The map function just creates copies of f. Then the outer map creates copies of map f. There is no cloned function attempting to clone itself. That would happen, perhaps, if Map called (f f), and was applied to a function that called its argument on itself. Like this:

(Map f Nil) = Nil
(Map f (Cons x xs)) = (Map ((f f) x) xs)

(Main) = (Map λx(x x) (Cons 1 (Cons 2 (Cons 3 Nil)))))

But that's not the definition of map. Even if that was the definition of map... most mapped functions are linear (like λx(+ x 1)). And even if the mapped function wasn't linear, it would probably not be calling its input on itself. Do you see how far your example is from reaching the limit? The program above doesn't even make sense. It is difficult to even come up with well-typed examples that reach this limitation. Church Nat is the only one I know, actually. And if once in a blue moon an user happens to reach this limitation, fine; just let the clone-of-clone-checker show him/her a type error (on the input language, not HVM). Should be an easy fix. Rust shows us 50 borrow-checker complaints every time we compile anything, and everyone is fine!

Ah, I thought creating copies of map f would create copies of map, but I guess I'm mistaken about it. I've seen more than once your example above of writing the double function and calling it on itself, but it was mainly to test that compilers were correct. I'm still not sure about the precise conditions of "a clone cloning its own clone". Supposing f clones its argument, f f is not allowed. However, is f 0 f allowed if f clones its second argument? Is f (\x. f x) allowed? What about f (f g) and f (g f) depending on g? In any case, it seems non-obvious to me to come with a type system to forbid such clones, and I fear such a type system might be as difficult to understand as Rust's borrow checker...

EDIT: actually, I think I don't even understand why the Y combinator would be fine. r is applied to (a clone of) itself, which is fine for the first step of reduction. However, for the second step, the two occurences of r are both clones of the rightmost lambda-term. Applying r to itself then is a violation of the "clone cloning its own clone" rule, I would have thought?

@Ekdohibs think about it like this:

1. Every duplicator on the source (dup x y = term) has a unique label.

2. A duplicator can't copy a term that has a duplicator with the same label as itself.

For example:

(λf(dup#0 x y = f; (x y)) λg(dup#1 a b = g; (a b)))
---------------------------------------------------
dup#0 x y = λg(dup#1 a b = g; (a b)); (x y)
---------------------------------------------------
(λg(dup#1 a b = g; (a b)) λg(dup#1 a b = g; (a b)))
---------------------------------------------------
dup#1 a b = λg(dup#1 a b = g; (a b)); (a b)

The last line is undefined behavior, because it has a dup with a #1 label attempting to copy a function which has a dup with a #1 label. Notice that the first level of self-copying is fine. It is when clones clone clones that you get a problem.

This can only happen when a function copies itself, and then the copy also copies itself. Emphasis on the "self". Functions copying other functions is fine. Repeated self-copying is the only way, because, otherwise, it would be impossible for two identical labels to collide, since every dup has a globally unique label.

In general, any program that isn't allowed is similar to (λx(x x) λx(x x)) in shape. For example, the first program you posted is just a larger version of it:

(Main arg) = ((λa (a (λb ((λc (λd (b (c d)))) a)))) (λe (e e)))
(Main arg) = ((λa (a ........................ a..)) (λe (e e)))

And the second one expands to it after a few steps.

It is not hard to come up with a static checker for this requirement. For example, the old Formality-Core had one, but it was too restrictive, because it stratified programs in levels, so that a dup on level X could only copy terms on level X+1, avoiding this problem. A much better solution, I believe, would be to just track a function's lifecycle and make sure it isn't cloning itself, followed by its clones also cloning themselves.

Ah, that makes it clearer, thank you! However, with this definition, I still think the Y-combinator will be undefined behavior.

No, because the Y-combinator just creates infinite copies of the function it receives, but it never actually copies itself, nor does the function it receives copy itself. But applying the Y-combinator to itself is undefined behavior.

I understand your point that it might be annoying to demand such a checker for any language interested to compile to HVM, though. Perhaps we could provide a checker as part of HVM, somehow. I'll think about that.

I'll close this issue and link to it on the needed improvements thread, in case anyone is interested in contributing with this in particular.

(@Ekdohibs feel free to re-open if you want to ask more questions!)

In the Y-combinator case, it is neither the function it receives nor the Y-combinator which copies itself, but the (\r. f (r r)) subterm. If we expand the body of the Y-combinator to (\r. dup#0 s t =r ; f (s t)) (\r. dup#1 s t = r; f (s t)), after a reduction it becomes (\r. dup#1 s t = r; f (s t)) (\r. dup#1 s t = r; f (s t)), and the dup#1 needs to copy a dup#1.

@VictorTaelin (it seems like I can't reopen the issue, since you were the one to close it, however).

Ah, that is a fair point, a sub-term of the Y-combinator does clone itself, and then that clone clones itself again. That should be undefined behavior according to my explanation, so you're right. What happens, though, is that the duplication process is never finished, because (r r) gets pushed infinitely down the recursion, so it actually works fine. The Y-Combinator is a pretty peculiar term. It even has a normal form:

dup#1 s t = r; 
dup#1 S T = R;
(λr(f (s t)) λR(f (S T)))
-------------------------
dup#1 s t = λR(f (S T)); 
dup#1 S T = R;
(f (s t))
-------------------------
dup#1 s t = (f (S T)); 
dup#1 S T = #1{R0 R1};
(f (λR0(s) λR1(t)))
-------------------------
dup#1 s t = (f (S T)); 
dup#1 S T = #1{λR1(t) R1};
(f s)
-------------------------
dup#1 s t = (f (λR1(t) R1)); 
(f s)
-------------------------
dup#1 s t = (f t); 
(f s)

Note that this "normal form" represents (f (f (f (f (f ....))))). Anyway, you're right, a complete criteria for acceptance would be a little complex. But the description I provided gives us a fairly reasonable language already, I think. A "clone checker" doesn't need to cover all programs that don't produce undefined behavior, it just must result in a practical language. It is a similar situation with Rust: there are many correct programs that the borrow checker simply can't identify as such. A clone checker would perhaps be a whitelist of patterns which we know to be safe.

I agree, the Y-combinator works correctly, even if it is undefined behaviour. In fact, what I think happens is that we get a duplication confusion (which often produces errors), but here instead, since the Y-combinator has a rather peculiar form, gives us the correct result, albeit with a term containing loops(!). I also found a slightly unsual example, but one that you could see in a real program that should cause a clone error: imagine you have a list of functions, and you want to map each of these functions over a list (that could happen with a list monad for instance). You would have a term of the form map (\f. map f values) functions, and if I'm not mistaken, in this case, map will duplicate its argument, which contains itself a clone of map that will be duplicated (the difference with before being that since the function is statically unknown, the duplication will wait for each call of the function, thus keeping an unreduced dup).

@VictorTaelin When would you ever apply a function to itself in a standard functional language like Haskell or OCaml?

I don't think that case is problematic, but I can try later.

@L-as applying a function to itself is not that rare. I can think of Church-Nats, and the Y-Combinator. Having to do that once again with the result is quite rare.

Well, this should be checked somehow. Which rules do you think are necessary to add to typechecker to catch it?

Should the (f f) application simply emit linearity for the lambda that bounds f?

With the following code I get incorrect results (as expected):

(Map Nil f) = Nil
(Map (Cons x xs) f) = (Cons (f x) (Map xs f))

(Main arg) =
  let l1 = (Cons (λx(x)) (Cons (λx(+ x 2)) Nil))
  let l2 = (Cons 0 (Cons 1 Nil))
  (Map l1 (λf(Map l2 f)))

The result given by HVM is (Cons (Cons 0 (Cons 3 (Nil))) (Cons (Cons 0 (Cons 3 (Nil))) (Nil))) while (Cons (Cons 0 (Cons 1 (Nil))) (Cons (Cons 2 (Cons 3 (Nil))) (Nil))) is expected and is what we get if we replace an instance of Map by an identical copy.

However, I (personally) find this code to be very reasonable: no self-application, only the classic "Map" function is used, and the most unusual part is arguably the list of functions (which is not even that unusual).

@Ekdohibs the abstract algorithm handles your program fine, it doesn't hit "the limit". It hits it on HVM due to a temporary peculiarity: HVM currently does not assign different labels to different uses of the same global function. That will be patched soon, and your program will work. As a temporary fix, you could just have two map functions:

(Map0 Nil         f) = Nil
(Map0 (Cons x xs) f) = (Cons (f x) (Map0 xs f))

(Map1 Nil         f) = Nil
(Map1 (Cons x xs) f) = (Cons (f x) (Map1 xs f))

(Main arg) =
  let l1 = (Cons (λx(x)) (Cons (λx(+ x 2)) Nil))
  let l2 = (Cons 0 (Cons 1 Nil))
  (Map0 l1 (λf(Map1 l2 f)))

But again, that's not necessary, since it will be patched soon. I'll notify this issue when that happens.

To be more specific, these lines on compiler.rs will just assign labels defined at compile time to a global function's dup nodes. Instead, we should dynamically generate fresh labels. The only issue with that is that the space for labels is small (2 ** 16), because we use 8 bits for the atomic_flag synchronization operation. This would be easily exhausted if we generate new labels dynamically. So we either need to change the atomic_flag to use 1 bit, or avoid generating the same labels by some external mean, or just increase the space for it, perhaps storing it separately.

While i completely agree that this fixes the issue (which is what I meant by "replacing one instance by an indentical function" above), this would not work if Map was a function argument instead of a global function (think functors and monads for instance: in the case of monads, This very function, of type Monad m => m (a -> b) -> m a -> m b exists in Haskell and is the well-known and very used function <*>!).

@Ekdohibs I don't think that is true. Even if Map was built locally with Fix, the Fix function itself would give it brand new labels every time it is generated; right? Or what else you have in mind?

What I had in mind was a function whose body was the expression above that took Map as an argument, sorry for the confusion.

In Haskell the code might be

x :: Applicative m => m [[Int]]
x =
  let l1 = ((\x -> x) : (\x -> x + 2) : []) in
  let l2 = (0 : 1 : []) in
  pure $ pure (\f -> pure f <*> l2) <*> l1

While not entirely natural, it goes to show that completely legal Haskell exists, while not being valid in HVM.

Unfortunately I don't think HVM will be usable for Haskell unless all legal Haskell is covered, or at the very least a large subset that tells you when you step outside it.

I just realised that my code accidentally uses the Applicative for lists.

The following is perhaps a better example:

x :: (forall a b. (a -> b) -> [a] -> [b]) -> [[Int]]
x mymap =
  let l1 = ((\x -> x) : (\x -> x + 2) : []) in
  let l2 = (0 : 1 : []) in
  mymap (\f -> mymap f l2) l1

The code I had in mind was something like:

f :: Monad m -> m (a -> b) -> m a -> m b
f x1 x2 = join $ fmap (\f -> fmap f x2) x1

x = f ((\x -> x) : (\x -> x+ 2) : []) (0 : 1 : [])

Notice how the Monad m in the definition of f has a side-effect that the fmap is passed as an argument once typeclasses are lowered, so that the function f makes two clones and applies one to the other.

I just want to say that apparently the original issue has been fixed. The following program:

(Map Nil f) = Nil
(Map (Cons x xs) f) = (Cons (f x) (Map xs f))

(Main arg) =
  let l1 = (Cons (λx(x)) (Cons (λx(+ x 2)) Nil))
  let l2 = (Cons 0 (Cons 1 Nil))
  (Map l1 (λf(Map l2 f)))

Evaluates to

(Cons (Cons 0 (Cons 1 (Nil))) (Cons (Cons 2 (Cons 3 (Nil))) (Nil)))

Moreover, the following program (which I conjecture has been working correctly all the time):

(Map Nil f) = Nil
(Map (Cons x xs) f) = (Cons (f x) (Map xs f))

(Mapping mymap) =
  let l1 = (Cons (λx(x)) (Cons (λx(+ x 2)) Nil))
  let l2 = (Cons 0 (Cons 1 Nil))
  (mymap l1 (λf(mymap l2 f)))

(Main arg) =
  (Mapping (λlλf(Map l f)))

Evaluates to:

(Cons (Cons 0 (Cons 1 (Nil))) (Cons (Cons 2 (Cons 3 (Nil))) (Nil)))

As a meta remark, I am completely with Victor here as I do not understand why this whole thing is so important to some people. It really is a very very obscure corner case that untyped lambda calculus unfortunately has.

The issue is that HVM is fundamentally unusable for most functional programming languages unless this is fixed at its root. Supporting the full LC is not a necessity, but when you go from e.g. GHC Core to HVM, there must be a way of detecting whether this GHC Core term can be translated to HVM. It is possible to make a naïve "type checker" for this, but it's very hard to make one that supports a language expressive enough to support common Haskell idioms AFAIK. If you can not guarantee that, then it's not useful in real-world applications. Why would you build a program that maybe works, when hitting the limit is possible with trivial and standard Haskell code?