Thanks everybody, your feedback and replys make me feel less lonely, I really appreciate it.
In case you wanted to steer it in the direction of a beta-optimal runtime like HVM, do note the pathological cases (e.g. the last page of https://sci-hub.hkvisa.net/10.1006/inco.1997.2643) and the other pitfalls which HVM suffers from (; of a fundamental nature of the framework of Interaction nets, I'm afraid, demanding breakthroughs in theory to be overcome https://news.ycombinator.com/item?id=35336113#35340714).
Despite these issues, I am quite strongly convinced that Girard's framework of Geometry of Interaction is the best way forward towards a computational model with local and denotational properties for large scale software.
My current plan is to programming with interaction nets directly, and to view Lamping's "optimal lambda calculus reduction" as an example.
I have not read Lamping's paper yet. But if it uses "Interaction Combinators", maybe I can not even do it in my implementation.
Because there are two version of inet:
(1) Lafont's 1990 paper "Interaction Nets"
(2) Lafont's 1997 paper "Interaction Combinators"
I implemented (1) where a port has a sign (input port v.s. output port). Given two ports, I can only connect them when they have opposite signs.
In (2) there is no input port v.s. output port, ports are not signed (Lafont called the signed version "directed" in (2)).
"Interaction Combinators" uses self interaction (rule about a node interacting with itself), it is not possible in signed version of inet.
Because one node only has one principle port, thus can not connect to it's own principle port, because the same principle port has the same sign, not opposite signs.
------
I said "programming with interaction nets directly", because it seems already a more practical language than lambda calculus, for we do not need lambda encoding to express datatype and pattern matching, we can define rules case by case directly.
By the way, I'm fairly certain that the Interaction Nets is the more general term, encompassing Interaction Combinators as merely some set of nets that happens to be a universal model of computation. They definitely both share the distinctions of principal ports v.s. auxiliary ports.
------
> They definitely both share the distinctions of principal ports v.s. auxiliary ports.
Version (1) and (2) both have principal ports v.s. auxiliary ports.
But only (1) has input ports v.s. output ports.
(I was actually quite shocked by this, when I read the 1997 paper.)
> The choice of an input/output denomination is purely conventional: it does not matter if you call input what I call output, and conversely, but we must agree on matching. [...] typing ensures local correctness of computations
It seems to me that the input/output convention is really just one particular type system, orthogonal to the essential idea of Interaction nets or Interaction combinators. Indeed if iNet requires such a typing discipline, then nets like Interaction combinators cannot be implemented.