Comment by qazxcvbnm
1 year ago
Indeed, I see that Lafont's 1990 paper introduces 'input' and 'output' denominations under Section 2 "Type Discipline".
> 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.
No comments yet
Contribute on Hacker News ↗