Substructural typesystems vs Stack-Oriented languages

Building blocks

Definition of the fundamental operations that define the 2 framework that we are analyzing.

Stack-Oriented languages primitives

Primitive Description Signature (?)
Duplicate Duplicate the element on the top of the stack. 
a -- a a
Swap Exchange the elements on the top of the stack. 
a b -- b a
Drop Drop the element on the top of the stack. 
a --
Other operation that are usually provided like rot, over, ecc... can be defined by using these 3 operations.

Structural Rules

Rule Description Inference rule
Contraction (or Factoring) Two equal (or unifiable) members on the same side of a sequent can be replaced by a single member (or common instance). \[ \begin{prooftree} \AXC{$\Gamma, A, A \vdash \Sigma$} \UIC{$\Gamma, A \vdash \Sigma$} \end{prooftree} \]\[ \begin{prooftree} \AXC{$\Gamma \vdash A, A \Sigma$} \UIC{$\Gamma \vdash A, \Sigma$} \end{prooftree} \]
Exchange Two members on the same side of a sequent can be swapped. \[ \begin{prooftree} \AXC{$\Gamma_1, A, \Gamma_2, B, \Gamma_3 \vdash \Sigma$} \UIC{$\Gamma_1, B, \Gamma_2, A, \Gamma_3 \vdash \Sigma$} \end{prooftree} \]\[ \begin{prooftree} \AXC{$\Gamma \vdash \Sigma_1, A, \Sigma_2, B, \Sigma_3$} \UIC{$\Gamma \vdash \Sigma_1, B, \Sigma_2, A, \Sigma_3$} \end{prooftree} \]
Weakening Hypotheses or conclusion of a sequent may be extended with additional members. \[ \begin{prooftree} \AXC{$\Gamma \vdash \Sigma$} \UIC{$\Gamma , A\vdash \Sigma$} \end{prooftree} \]\[ \begin{prooftree} \AXC{$\Gamma \vdash \Sigma$} \UIC{$\Gamma \vdash \Sigma, A$} \end{prooftree} \]

The relationship

It's pretty obvious that there is a 1 to 1 correspondence between the stack-oriented primitives and the structural rules.
Stack oriented primitive Structural rule
Duplicate Contraction
Swap Exchange
Drop Weakening

Substructural typesystems

Substructural typesystems are typesystem where zero, one or more structural rules are absent.
Type Exchange Weakening Contraction Logic Interpretation
Ordered ❌ ❌ ❌ Noncommutative Use exactly once and in order
Linear ✔️ ❌ ❌ Linear Use exactly once
Affine ✔️ ✔️ ❌ Affine Use at most once
Relevant ✔️ ❌ ✔️ Relevant Use at least once
Normal ✔️ ✔️ ✔️ Standard Use arbitrarly

What does this mean

Modelling substructural typesystems in a stack-based language is a trivial task, just look at the (substructural) type on the top of the stack and disable the corresponding primitives.
Type Swap Drop Duplicate
Ordered ❌ ❌ ❌
Linear ✔️ ❌ ❌
Affine ✔️ ✔️ ❌
Relevant ✔️ ❌ ✔️
Normal ✔️ ✔️ ✔️

Type inference

Also performing type inference should be trivial (TODO: check).