The lambda calculus is an untyped language that is often extended with logical frameworks such as the vertices of the λ-cube. Is there something similar to it, but for interaction nets? What about interaction combinators?
5
$\begingroup$
$\endgroup$
-
1$\begingroup$ I doubt it. There is not much research on interaction nets. It should be possible to look at it all. $\endgroup$ – Martin Berger Feb 4 '16 at 11:24
1
-
$\begingroup$ Maybe, but I'm not so sure I make the connection between what is presented on this paper and my understanding of the λ-cube and dependent types. For example, how'd you express dependent types, things like the
λ (t : *) -> λ (x : t) -> xterm (Morte syntax)? $\endgroup$ – MaiaVictor Sep 22 '17 at 23:58
4
$\begingroup$
$\endgroup$
Like Martin said, nothing like an equivalent for the $\lambda$-cube has ever been developed for interaction nets or interaction combinators.
The only work that considers types for interaction nets is Lafont's original paper [1]. (My own CONCUR 2005 paper also considers types but adds nothing new to what Lafont did). It is an extremely simple system: only basic types plus a polarity, no type constructors at all. Nevertheless, it is enough to obtain a desirable safety property: a well typed net cannot reduce to a net containing a "clash" (an active pair which does not have a corresponding reduction rule and is therefore "stuck").
Of course, since multiplicative linear logic proof nets are a particular system of interaction nets, it is defintely possible to equip certain systems of interaction nets with more complex types, using non-trivial type constructors. But nothing has ever been studied, mostly because the interest of such an endevour is unclear.
[1] Yves Lafont, Interaction Nets. In Proceedings of POPL, 1990.
answered Feb 4 '16 at 12:14
-
1$\begingroup$ One more thing: this year at POPL, Stéphane Gimenez and Georg Moser had a paper using interaction nets (for studying complexity properties). I missed their talk and haven't yet seen the paper, but it's possible that it contains some new work on types for interaction nets, although I doubt it is anything in the style of the $\lambda$-cube types. $\endgroup$ – Damiano Mazza Feb 4 '16 at 12:17
-
$\begingroup$ So my question is more in the lines - interaction nets aren't as useful for proofs and related as the λ-calculus, I guess? $\endgroup$ – MaiaVictor Feb 4 '16 at 12:26
-
1$\begingroup$ @DamianoMazza Lafont's POPL paper is available electronically here and, if you can access the ACM library, here. $\endgroup$ – Martin Berger Feb 5 '16 at 8:37
-
$\begingroup$ @MartinBerger That's great, thank you! The last time I checked there was no electronic copy freely available, but it was a long time ago, somebody must have scanned it in the meantime! $\endgroup$ – Damiano Mazza Feb 5 '16 at 10:01
