Filter with any function returning invalid

[aripiprazole]

Reproducing the behavior

(any f xs) = match (filter f xs) {
  List/Nil: 0
  List/Cons: 1
}
(filter f List/Nil) = List/Nil
(filter f (List/Cons x xs)) = switch (f x) {
  0: (filter f xs)
  _: (List/Cons x (filter f xs))
}
s = @xs (any @x 0 xs)
main = (filter s [[1, 2]])

the code that generates

@List/Cons = (a (b ((@List/Cons/tag (a (b c))) c)))

@List/Cons/tag = 1

@List/Nil = ((@List/Nil/tag a) a)

@List/Nil/tag = 0

@any = (a (b c))
  & @filter ~ (a (b (@any__C0 c)))

@any__C0 = (?((0 (* (* (* 1)))) a) a)

@filter = (a ((@filter__C3 (a b)) b))

@filter__C0 = (a (* (b c)))
  & @filter ~ (a (b c))

@filter__C1 = (* (b (a (c e))))
  & @List/Cons ~ (a (d e))
  & @filter ~ (b (c d))

@filter__C2 = (* ({a c} (d ({(a ?((@filter__C0 @filter__C1) (b (c (d e))))) b} e))))

@filter__C3 = (?(((* @List/Nil) @filter__C2) a) a)

@main = d
  & @filter ~ (@s (c d))
  & @List/Cons ~ (b (@List/Nil c))
  & @List/Cons ~ (1 (a b))
  & @List/Cons ~ (2 (@List/Nil a))

@s = (a b)
  & @any ~ ((* 0) (a b))

is returning just:

System Settings

Example:

• OS: Mac OS
• CPU: M3 Pro
• GPU: n/a
• Cuda Version: n/a

Additional context

No response

[nicolas-abril]

In your program filter is a high-order function that duplicates the first argument f.
Unfortunately, the 32bit implementation of HVM has a limitation that causes this application to not reduce correctly if f itself has duplications in its normal form.

In your specific program, filter duplicates f, that receives the value of any which itself contains filter as a subterm, violating the condition above.
This is not an inherent limitation of the HVM model in general, for example hvm64 could do it, as well as hvm1.

In the future we plan on adding further checks and hopefully a type checker (probably on Bend, since a type system on top of interaction nets would be more complicated).

To actually fix your program, you can write something like this:

(any f xs) = match (filter f xs) {
  List/Nil: 0
  List/Cons: 1
}

(filter f List/Nil) = List/Nil
(filter f (List/Cons x xs)) = switch (f x) {
  0: (filter f xs)
  _: (List/Cons x (filter f xs))
}

(filter_s List/Nil) = List/Nil
(filter_s (List/Cons x xs)) = switch (any @y 0 x) {
  0: (filter_s xs)
  _: (List/Cons x (filter_s xs))
}

main = (filter_s [[1, 2]])

Basically inlining s into the filter application to avoid having to duplicate it.