Dictionary-Passing Translation of Featherweight Go

Martin Sulzmann1  Stefan Wehr2

Karlsruhe University of Applied Sciences, Germany

Offenburg University of Applied Sciences, Germany

The Go programming language is an increasingly popular language but some of
its features lack a formal investigation.
This article explains Go's resolution mechanism for overloaded methods and
its support for structural subtyping by
means of translation from Featherweight Go to a simple target language.
The translation employs a form of dictionary passing known from type classes
in Haskell and preserves the
dynamic behavior of Featherweight Go programs.

§ INTRODUCTION

The Go programming language [22], introduced by Google in 2009,
is syntactically close to C and incorporates features
that are well-established in other programming languages.
For example, a garbage collector as found in Java  [6], built-in support for concurrency
and channels in the style of Concurrent ML [17],
higher-order and anonymous functions known from functional languages such as Haskell [12].
Go also supports method overloading for structures where related methods can be grouped together
using interfaces.
Unlike Java, where subtyping is nominal, Go supports structural subtyping among interfaces.

Earlier work by Griesmer and co-authors [7]
introduces Featherweight Go (FG), a minimal core calculus that includes the essential features of Go.
Their work specifies static typing rules and a run-time method lookup semantics for FG.
However, the actual Go implementation appears to employ a different dynamic semantics.
Quoting Griesmer and co-workers:
Go is designed to enable efficient implementation. Structures are laid out in memory as a sequence of fields,
while an interface is a pair of a pointer to an underlying structure and a pointer to a dictionary of methods.

To our knowledge, nobody has so far formalized such a dictionary-passing translation for FG and established its semantic
equivalence with the FG run-time method lookup dynamic semantics.
Hence, we make the following contributions:

* Section <ref> specifies the translation of source FG programs to an
untyped lambda calculus with pattern matching.
We employ a dictionary-passing translation scheme à la type classes [8]
to statically resolve overloaded FG method calls. The translation
is guided by the typing of the FG program.

* Section <ref> establishes the semantic correctness of the dictionary-passing translation.
The proof for this result is far from trivial.
We require step-indexed logical relations [1] as there can be
cyclic dependencies between interfaces and method declarations.

Section <ref> specifies Featherweight Go (FG)
and Section <ref> specifies our target language.
Section <ref> covers related works and concludes.
The upcoming section gives an overview.

§ OVERVIEW

f:fg-equalityEquality and ordering in FG and its translation

We introduce Featherweight Go [7] (FG) by an example
and then present the ideas of our dictionary-passing translation for FG.

§.§ FG by Example

FG is a syntactic subset of the full Go language, supporting structures, methods and interfaces.
The upper part in Figure <ref>, lines 1-22, shows an example slightly
adopted from [7].
The original example covers equality in FG.
We extend the example and include an ordering relation (less or equal than) as well.

FG programs consist of a sequence of declarations defining structures, methods, interfaces and
a main function. Method bodies in FG only consist of a return statement. For clarity,
we sometimes identify subexpressions via variable bindings introduced with
In such a declaration, the name of a variable precedes its type,
the notation  _ (line 21)
indicates that we do not care about the
variable name given to the main expression. The example uses primitive types  and
and several operations on values of these types (, , …).
These are not part of FG.

Structures in FG are similar to structures known from C/.
A syntactic difference is the FG convention that field names precede the types.
In FG, structures and methods are always declared separately, whereas  groups methods
together in a
class declaration. Methods in FG can be overloaded on the receiver.
The receiver is the value on which the method operates on.

Interfaces in FG consist of a set of method declarations that share the same receiver.
For example, interface  introduces method
and interface  introduces methods  and  (line 3 and 4).
The (leading) receiver argument is left implicit and
method names in interfaces must always be distinct.
Interfaces are types and can be used in type declarations for structures and methods.
For example, structure  defines two  fields  and ,
each of type .
Declarations of structures must be non-recursive whereas an interface
may appear in the method declaration of the interface itself.
For example, see interface .

FG uses the keyword  to introduce
methods and functions. Methods can be distinguished from ordinary functions
as the receiver argument always precedes the method name.
In FG, the only function is the main function, all other declarations introduced by
are methods.

Consider the method implementation of  for receiver  of type
starting at line 6. This definition takes care of equality among  values
by making use of primitive equality  among .
We would expect argument  to be of type .
However, to be able to use an  value everywhere an  value is expected (to
be discussed shortly),
the signature of  for  must match exactly the signature declared by
interface .
Hence,  has declared type , and
we resort to a type assertion, written , to convert it to .
Type assertions involve a run-time check that may fail.
The same observation applies to the implementation of  for receiver
(line 9).

FG supports structural subtyping among structures and interfaces.
A structure is a subtype of an interface if the structure implements the methods as declared by the interface.
For example,  and  both implement interface .
This implies the structural subtype relations
(1) $\texttt{Int} \subtypeOfSym\ \texttt{Eq}$ and
(2) $\texttt{Pair} \subtypeOfSym\ \texttt{Eq}$.
Relation (1) ensures that the construction of the pair at line 20 type checks:
variables  and  have type  but can also be viewed
as type  thanks to structural subtyping.
Relation (2) resolves the method call  at line 21
as the  variable  also has the type .
The method definition starting at line 9 will be chosen.

An interface $I$ is a structural subtype of another interface $J$ if
$I$ contains all of $J$'s method declarations.
For example, the set of methods of interface  is a superset of the method set of .
This implies (3) $\texttt{Ord} \subtypeOfSym\ \texttt{Eq}$, which
is used in the method implementation of  for receiver type .
See line 14 where (3) yields that variable  with declared
type  also has type .
Thus, the method call  is resolved via
the method definition from line 6.

§.§ Dictionary-Passing Translation

We translate FG programs by applying a form of dictionary-passing translation known from type classes [8].
As our target language we consider an untyped functional language with pattern matching where
we use Haskell style syntax for expressions and patterns.
Each FG interface translates to a pair consisting of a structure value and a dictionary.
The dictionary holds the set of methods available as specified by the interface
whereas the structure implements these methods.
We refer to such pairs as interface-values.
The translation is type-directed as we need type information to resolve method calls and construct the
appropriate dictionaries and interface values.

Lines 23-49 show the result of applying our dictionary-passing[Technically, we are passing around
interface-values wrapping dictionaries of methods.] translation scheme to the FG program (lines 1-22).
We use a tagged representation to encode FG structures in the target language.
Hence, for each structure $S$, we assume a data constructor ,
where we use pattern matching to represent field access
(lines 23-26). For example, structure  implies the data constructor .
For convenience, we assume tuples and make use of don't care patterns .

A method call on an interface type translates to a lookup of the method in the dictionary
of the corresponding interface-value.
Like structures, interface-values are tagged in the target language.
For example, line 39 introduces the helper function  to perform method lookup
for method  of interface . The constructor for an  interface-value is
. Hence,
we pattern match on  and extract the underlying structure value and method definition.
A method call such as $\ldots$ in the source program (line 10) with receiver
of type  then translates
to  $\ldots$ (line 41).

A method call on a structure translates to the method definition for this receiver type.
For example, we write  to refer to the translation
of the method definition of
for receiver type .
A method call such as $\ldots$ in the source program (line 14) with
receiver  of type  then translates
to  $\ldots$ (line 43).

The construction of interface-values is based on structural subtype relations.
Recall the three structural subtype relations we have seen earlier:
(1) $\texttt{Int} \subtypeOfSym\ \texttt{Eq}$ and
(2) $\texttt{Pair} \subtypeOfSym\ \texttt{Eq}$
and (3) $\texttt{Ord} \subtypeOfSym\ \texttt{Eq}$.
Relation (1) implies the interface-value constructor  (line 29),
which builds an  interface-value via the given structure value  and a dictionary
consisting only of the method .
Relation (2) implies a similar interface-value constructor  (line 30).
Relation (3) gives raise to the interface-value constructor  (line 31),
which transforms some
into an  interface-value.
We assume that in case a dictionary consists of several methods, methods are kept in fixed order.

Type assertions imply interface-value destructors.
For example, the source expression  (line 7) performs a run-time check,
asserting that  has type .
In terms of the dictionary-passing translation, function  (line 34)
performs this check.
Via the pattern ,
we assert that the underlying target structure must result from .
If the interface-value contains a value not tagged with , the pattern
matching fails at run-time, just as the type assertion in FG.
Interface-value destructors  and
(lines 35, 36) result from similar uses of type assertions.

To summarize, each use of structural subtyping implies a interface-value constructor being inserted
in the target program. For example, typing the source expression
in line 21
relies on structural subtyping $\texttt{Pair} \subtypeOfSym \texttt{Eq}$ because argument
has type  but method  requires a parameter of type .
Thus, the translation of this expression is
in line 49.

Similarly, type assertions imply interface-value destructors.
For example, the source expression
in line 10
use a type assertion on , which has type .
Thus, it translates to the target expression
in line 41.

We continue by introducing FG and our target language followed by the full details of the
dictionary-passing translation.

§ FEATHERWEIGHT GO

f:fgFeatherweight Go (FG)

Field name         f

Method name       m

Variable name     x,y

Structure type name        t_S, u_S

Interface type name        t_I, u_I

Type name                  t, u ::= t_S |t_I

Method signature           M ::= (x_i  t_i)  t

Method specification       R, S ::= m M

Expression     d,e ::=

Variable                x     |
Method call             e.m(e)     |
Structure literal       t_S { e }     |
Select                  e.f     |
Type assertion          e.(t)

Type literal     L ::=

Structure        { f  t }     |
Interface        { S }

Declaration     D ::=

Type          t  L     |
Method        (x  t_S)  mM  {  e }

Program     P     ::=
D   () { _ = e }

Dt_S = { m M | (x  t_S)  mM  {  e } ∈D }

t_I   { S } ∈D

Dt_I = { S }

Dt ⊇Du_I

D de

v     ::=     t_S { v }

Evaluation context
::=     []
|t_S { v, , e }
|v.m(v, , e)

Substitution (FG values)
::=     ⦜x_iv_i

D de

D [d][e]

t_S   { f  t } ∈D

D t_S { v }.f_iv_i

v = t_S { v }

(x  t_S)  m (x  t)  t  {  e } ∈D

D v.m(v)⦜xv, x_iv_i e

v = t_S { v }

D v.(t)v

Featherweight Go (FG) [7] is a tiny fragment of Go containing
only structures, methods and interfaces.
Figure <ref> gives the syntax of FG.
With the exception of variable bindings in function bodies, the primitive type  with operations
and , and the primitive type  with operations
and ,
we can represent the example from Figure <ref> in FG.
Compared to the original presentation of FG [7] we use symbol $L$ instead of $T$ (for type literals),
and omit the  keyword at the start of a FG program.
Overbar notation $\sOver[n]{\xi}$ denotes the sequence $\xi_1 \ldots \xi_n$ for some
syntactic construct $\xi$, where in some places commas separate the sequence
If irrelevant, we omit the $n$ and simply write
$\sOver{\xi}$. Using the index variable $i$ under an overbar
marks the parts that vary from sequence item to sequence
item; for example, $\sOver[n]{\xi'\,\xi_i}$ abbreviates
and $\sOver[q]{\xi_j}$ abbreviates

FG is a statically typed language.
For brevity, we omit a detailed description of the FG typing rules
as they will show up in the type-directed translation.
The following conditions must be satisfied.

: Structures must be non-recursive.

: For each struct, field names must be distinct.

: For each interface, method names must be distinct.

: Each method declaration is uniquely identified by the receiver type and method name.

FG supports structural subtyping, written $\fgSub{\foreachN{D}}{t}{u}$.
A struct $t_S$ is a subtype of an interface $t_I$ if $t_S$ implements all the methods
specified by the interface $t_I$. An interface $t_I$ is a subtype of another interface $u_I$ if
the methods specified by $t_I$ are a superset of the methods specified by $u_I$.
The structural subtyping relations are specified in the middle part of Figure <ref>.

Next, we consider the dynamic semantics of FG.
The bottom part of Figure <ref> specifies the reduction of FG programs by making use of structural operational semantics rules
of the form $\foreachN{D} \turnsFG \reduce{d}{e}$
to reduce expression $d$ to expression $e$ under the  sequence $\foreachN{D}$ of declarations.

Rule fg-context makes use of evaluation contexts with holes to apply a reduction inside an expression.
Rule fg-field deals with field access.
Condition  guarantees that field name lookup is unambiguous.
Rule fg-call reduces method calls.
Condition  guarantees that method lookup is unambiguous.
The method call is reduced to the method body $e$ where we map the receiver argument to a concrete value $v$
and method arguments $x_i$ to concrete values $v_i$.
This is achieved by applying the substitution $\Angle{\subst{x}{v}, \foreachN{\subst{x_i}{v_i}}}$ on $e$,
written $\Angle{\subst{x}{v}, \foreachN{\subst{x_i}{v_i}}} e$.

Rule fg-assert covers type assertions.
We need to check that the type $t_S$ of value $v$ is consistent with the type $t$ asserted in the program text.
If $t$ is an interface, then $t_S$ must implement all the methods as specified by this interface.
If $t$ is a struct type, then $t$ must be equal to $t_S$.
Both checks can be carried out by checking that $t_S$ and $t$ are in a structural subtype relation.

We write $\foreachN{D} \turnsFG \reduceN{e}{v}$ to denote that under
the declarations $\foreachN{D}$, expression $e$ reduces to the value $v$
in a finite number of steps.
We write $\reduceFGk{k}{\foreachN{D}}{e}{v}$ to denote that under
the declarations $\foreachN{D}$, expression $e$ reduces to the value $v$
within at most $k$ steps. This means we might need fewer than $k$ steps
but $k$ are clearly sufficient to reduce the expression to some value.
If there is no such $v$ for any number of steps,
we say that $e$ is irreducible w.r.t. $\foreachN{D}$, written $\irred(\foreachN{D},e)$.

§ TARGET LANGUAGE

f:target-langTarget Language (TL)

Expression     ::=

Variable          |    |
Constructor           |
Application            |
Abstraction       λ.     |
Pattern case       []

Pattern clause
::=  →

::= =0pt
_i = λ_i . _i

TL values
::=     |

TL evaluation context
::=     []
| |

Substitution (TL values)
::=     ⦜

Substitution (TL methods)
::=     ⦜λ.

TL expression reductions

(λ. )  ⦜

_in →' ∈[→]

⦜_i_in '

TL reductions

⦜_iλ_i. _i'
_i = λ_i._i_i = λ_i. _i'

Figure <ref> specifies the syntax and dynamic semantics of our target language ().
We use capital letters for constructs of the target language. Target expressions $E$ include
variables $X,Y$, data constructors $K$,
function application, lambda abstraction and case expressions to pattern match against constructors.
In a case expression with only one pattern clause,
we often omit the brackets and just write
$\tcaseof{\expT}{\patT \rightarrow \expT}$.
A program consists of a sequence of function definitions and a (main) expression.
The function definitions are the result of translating FG method definitions.

We assume data constructors for tuples up to some fixed but arbitrary size. The syntax
$(\foreach{E}{n})$ constructs an $n$-tuple when used as an expression, and deconstructs
it when used in a pattern context.
At some places, we use nested patterns as an abbreviation for nested case expressions.
The notation $\lambda \patT. \expT$ stands for
$\lambda X . \tcaseof{X}{[\patT \rightarrow \expT]}$, where $X$ is fresh.

Representing the example from Figure <ref> in the target language
requires some more straightforward extensions:
integers with operations
and , booleans with operations
and , let-bindings inside expressions,
and top-level bindings. The target language can encode the last two features
via lambda-abstractions and
top-level let-bindings.

The structural operational semantics employs two types of substitutions.
Substitution $\vbTL$ records the bindings resulting from pattern matching and function applications.
Substitution $\vbMethTL$ records the bindings for translated method definitions (i.e. for
top-level let-bindings).
Target values consist of constructors and variables.
A variable may be a value if it refers to a yet to be evaluated method binding.

Reduction of programs is mapped to reduction of expressions under a method substitution.
See rule tl-prog.
The remaining reduction rules are standard.

We write $\reduceTLN{\vbMethTL}{\expT}{\uT}$  to denote that under
substitution $\vbMethTL$, expression $\expT$ reduces to the value $\uT$
in a finite number of steps.
We write $\reduceTLk{k}{\vbMethTL}{\expT}{\uT}$ to denote that under substitution $\vbMethTL$,
expression $\expT$ reduces to $\uT$
within at most $k$ steps. This means we might need fewer than $k$ steps
but $k$ are clearly sufficient.
If there is no such $\uT$ for any number of steps,
we say that $\expT$ is irreducible w.r.t. $\vbMethTL$, written $\irred(\vbMethTL,\expT)$.

§ DICTIONARY-PASSING TRANSLATION

We formalize the dictionary-passing translation of FG to TL.
The translation rules are split over two figures.
Figure <ref> covers methods, programs and some expressions.
Figure <ref> covers structural subtyping and type assertions.
The translation rules are guided by type checking the FG program.
The gray shaded parts highlight target terms that are generated.
If these parts are ignored, the translation rules are effectively equivalent
to the FG type checking rules [7].
We assume that conditions FG1-4 hold as well.

We use the following conventions.
We assume that each FG variable $x$ translates to the TL variable $\xT$.
For each structure $t_S$ we introduce a TL constructor $K_{t_S}$.
For each interface $t_I$ we introduce a TL constructor $K_{t_I}$.
In the translation, a source value of an interface type $t_I$ translates to an interface-value tagged by $K_{t_I}$.
The interface-value contains the underlying structure value and a dictionary consisting of the set of methods as specified by the interface.
For each method declaration $\FUNC\ (x \ {t_S}) \ m M \ \{ \RETURN\ e \}$ we introduce
a TL variable $\mT{m}{t_S}$, thereby relying on  which guarantees that $m$ and
$t_S$ uniquely identify this declaration.
We write $\fgEnv$ to denote typing environments where we record the types of FG variables.
The notation $[n]$ is a short-hand for the set $\{1,\dots,n\}$.

§.§ Translating programs, methods and expressions

f:type-directed-meth-prog-decTranslation of methods, programs and expressions
Convention for mapping source to target terms

x   t_S K_t_S
t_I K_t_I
(x  t_S)  m M  {  e } mt_S

::=     { } |{ x : t } |∪

D (x  t_S)  m (x  t)  t

Translating method declarations

D{ x : t_S, x_i : t_in }e : t

(x  t_S)  m (x  tn)  t  {  e }
λ. λ(n).

Translating programs

De : t

D_i' =  (x_i  t_S_i)  m_i M_i  {  e_i }

(for all i ∈[n],
where D'n are the  declarations in D)

; D   () { _ = e }
m_it_S_i = _in

De : t
Translating expressions

(x : t) ∈
Dx : t

t_S   { f  tn } ∈D

De_i : t_i_i  i ∈[n]

Dt_S { en } : t_S _t_S  (n)

De : t_S

t_S   { f  tn } ∈D

e.f_i : t_i
_t_S  (n) →_i

m (x  tn)  t ∈Dt_S

De : t_S

De_i : t_i_i  i ∈[n]

De.m(en) : tmt_S   (n)

De : t_I

t_I   { S } ∈D

S_j = m(x  tn) t

De_i : t_i_i  i ∈[n]

X,Xq fresh

e.m(en) : t
_t_I  (, q) →_j   (n)

f:upcast-downcastTranslation of structural subtyping and type assertions

De : t
Translating structural subtyping and type assertions

De : t_2

De : u_1  _2

De : t_I_2

De.(u) : u_1  _2

Interface-value construction

t_I   { S } ∈D

Dt_S ⊇S

S = m Mn

_t_I  (, m_it_Sn)

t_I   { Rn } ∈D

u_I   { Sq } ∈D

S_i = R_(i)   i ∈[q]

λ.                             _t_I  (, n)
→_u_I  (, _(1), …, _(q))

Interface-value destruction

t_I   { Rn } ∈D

Dt_It_Sλ.                        _t_I  (K_t_S  Y, n)
→K_t_S   Y

X, Y, Y', Xn fresh

t_I   { Rn } ∈D

for all  t_Sj  { f  u } ∈D
with  Dt_Sju_I_j

_j =
_t_Sj  Y' →(_j  (_t_Sj  Y'))

_t_I  (, n) →                               []

The translation of programs and methods boils down to the translation of expressions involved.
Rule td-method translates a specific method declaration,
rule td-prog collects all method declarations and also translates the main expression.
See Figure <ref>.

The translation rules for expressions are of the form
$\tdExpTrans{\pair{\foreachN{D}}{\fgEnv}}{e : t}{\expT}$
where $\foreachN{D}$ refers to the sequence of FG declarations,
$\fgEnv$ refers to type binding of local variables,
$e$ is the to be translated FG expression,
$t$ its type and $\expT$ the resulting target term.
Departing from FG's original typing rules [7],
the translation rules are non-syntax directed due the structural subtyping rule td-sub
defined in Figure <ref>.
We could integrate this rule via the other rules but this would make all
the rules harder to read. Hence, we prefer to have a separate rule td-sub.

We now discuss the translations rules for the expression forms in
Figure <ref>. (The remaining expression forms
are covered in Figure <ref>, to be explained in the next section.)
Rule td-var translates variables and follows our convention that $x$ translates to $\xT$.
Rule td-struct translates a structure creation. The translated field elements $\expT_i$
are collected in a tuple and tagged via the constructor $K_{t_S}$.
Rule td-access uses pattern matching to capture field access in the translation.

Method calls are dealt with by rules td-call-struct and td-call-iface.
Rule td-call-struct covers the case that the receiver $e$ is of the structure type $t_S$.
The first precondition guarantees that an implementation for this specific method call exists.
(See Figure <ref> for the auxiliary $\methodSpecificationsRel$.)
Hence, we can assume that we have available a corresponding definition for $\mT{m}{t_S}$ in our translation.
The method call then translates to applying $\mT{m}{t_S}$ first on the translated receiver $\expT$,
followed by the translated arguments collected in a tuple $(\foreach{\expT}{n})$.

Rule td-call-iface assumes that receiver $e$ is of interface type $t_I$,
so $e$ translates to interface-value $E$.
Hence, we pattern match on $E$
to access the underlying value and the desired method in the dictionary.
We assume that the order of methods in the dictionary corresponds to the order
of method declarations in the interface.
The preconditions guarantee that $t_I$ provides a method $m$ as demanded by the method call,
where $j$ denotes the index of $m$ in interface $t_I$.

§.§ Translating structural subtyping and type assertions

Rule td-sub deals with structural subtyping and yields an interface-value constructor
derived via rules td-cons-struct-iface and td-cons-iface-iface in Figure <ref>.
These rules correspond to the structural subtyping rules in Figure <ref>
but additionally yield an interface-value constructor.

The preconditions in rule td-cons-struct-iface check that structure $t_S$ implements the interface $t_I$.
This guarantees the existence of method definitions $\mT{m_i}{t_S}$.
Hence, we can construct the desired interface-value.

The preconditions in rule td-cons-iface-iface check that $t_I$'s methods are a superset of $u_I$'s methods.
This is done via the total function $\mapPerm : \{1,\ldots,q\} \to \{1,\ldots,n\}$ that matches each (wanted) method in $u_I$ against a (given) method in $t_I$.
We use pattern matching over the $t_I$'s interface-value to extract the wanted methods.
Recall that dictionaries maintain the order of method as specified by the interface.

Type assertions $e.(u)$ are dealt with in rule td-assert and translate to an interface-value destructor.
In the static semantics of FG there are two cases to consider.
Both cases assume that the expression $e$ is of some interface type $t_I$.
The first case asserts the type of a structure and the second case asserts the type of an interface.
Asserting that a structure is
of the type of another structure is not allowed in FG, because such a type assertion would never succeed.

Rule td-destr-iface-struct deals with the case that we assert the type of a structure $t_S$.
If $t_S$ does not implement the interface $t_I$, the assertion can never be successful.
Hence, we find the precondition $\fgSub{\foreachN{D}}{t_S}{t_I}$.
We pattern match over the interface-value that represents $t_I$ to check the underlying value matches $t_S$
and extract the value.
It is possible that some other value has been used to implement the interface-value that represents $t_I$.
In such a case, the pattern match fails and we experience run-time failure.

Rule td-destr-iface-iface deals with the case that we assert the type of an interface $u_I$
on a value of type $t_I$.
The outer case expression extracts the value $Y$ underlying interface-value $t_I$
(this case never fails).
We then check if we can construct an interface-value for $u_I$ via $Y$.
This is done via an inner case expression.
For each structure $t_{Sj}$ implementing $u_I$,
we have a pattern clause $\clsT_j$ that
matches against the constructor $\kT_{t_{Sj}}$ of the structure and then constructs an interface-value for $u_I$.
There are two reasons for run-time failure here.
First, $\yT$ (used to implement $t_I$) might not implement $u_I$;
that is, none of the pattern clauses $\clsT_j$ match.
Second, $[\foreachN{\clsT}]$ might be empty because
no receiver at all implements $u_I$. This case is rather unlikely
and could be caught statically.

§ PROPERTIES

f:reduce-rel-fg-tlRelating FG to  Reduction

FG expressions versus  expressions

∀k_1 < k, k_2 < k, v, .

(k  - k_1 - k_2 > 0 ∧k_1Dev

k- k_1 - k_2tv

FG values versus  values

t_S   { f  tn } ∈D

∀i ∈[n] . kt_iv_i_i

t_S { vn }
_t_S  (n)

= _u_S  '

∀k_1 < k . k_1u_Sv

Dt_I = { m Mn }

∀k_2 < k, i ∈[n] . k_2
m_i M_i

_t_I  (, n)

m M
(x  t_S)  mM  {  e }
FG methods versus  methods

∀k' ≤k,
v', ', v_in, _in.
∧(∀i ∈[n]. k't_iv_i_i))

⦜xv',x_iv_in e
( ')  (n)

m (x  tn)  t
(x  t_S)  m (x  tn)  t  {  e }

FG versus  value bindings

∀(x : t) ∈.

FG declarations versus  method bindings

(x  t_S)  m M  {  e } ∈D :

m M
(x  t_S)  mM  {  e }mt_S

We wish to show that the dictionary-passing translation preserves the dynamic behavior of FG programs.
To establish this property we make use of (binary) logical relations [16, 20].
Logical relations express that related terms behave the same.
We say that source and target terms are equivalent if they are related under the logical relation.
The goal is to show that FG expressions and target expressions resulting from the dictionary-passing translation
are equivalent.

For example, in FG the run-time value associated with an interface type is a structure
that implements the interface
whereas in our translation each interface translates to an interface-value.
To establish that a structure $t_S\{\foreachN{v}\}$ and an interface-value $K_{t_I} (\uT, \foreachN{\uT})$ are equivalent
w.r.t. some interface $t_I$
we need to require that

* (Struct-I-Val-1) $t_S\{\foreachN{v}\}$ and $\uT$ are equivalent w.r.t. $t_S$, and

* (Struct-I-Val-2) method definitions for receiver type $t_S$ are equivalent to $\foreachN{\uT}$.

Because signatures in method specifications of an interface may refer to the interface itself,
there may be cyclic dependencies that then result in well-foundness issues of the definition of logical relations.
To solve this issue we include a step index [1].
We explain this technical point via the example in Figure <ref>.
We will write $\LR{k}{t}{e}{\expT}$ to denote that FG expression $e$ and TL expression $\expT$
are in a logical relation w.r.t. the FG type $t$, where $k$ is the step index.
Similarly, $\LR{k}{R}{\FUNC\ (x \ t_S) \ R \ \{ \RETURN\ e \}}{\uT}$ expresses
that a FG method declaration and a TL value $\vT$ are in a logical relation w.r.t. the FG method
specification $R$.

Consider the FG expression Int{1} from example in Figure <ref>.
When viewed at type Eq,
our translation yields the interface-value K$_{\textit{Eq}}$ (K$_{\textit{Int}}$ 1, eq$_{\textit{Int}}$).
We need to establish $\LRt{k_1}{\mathtt{Eq}}
{K$_{\textit{Eq}}$ (K$_{\textit{Int}}$ 1, eq$_{\textit{Int}}$)}$.
ll(1)     k_1𝙴𝚚
K$_{\textit{Eq}}$ (K$_{\textit{Int}}$ 1, eq$_{\textit{Int}}$)

K$_{\textit{Int}}$ 1

func (x Int) eq(y Eq) bool {return $e$}

∀k_4$v_1$$\uT_1$, k_4$v_2$$\uT_2$.

eq$_{\textit{Int}}$ $\uT_1$ $\uT_2$

Following (Struct-I-Val-1) and (Struct-I-Val-2), (1) holds if we can establish (2) and (3).
(2) is easy to establish.
(3) holds if we can establish (4).
(4) states that for equivalent inputs the respective method definitions are equivalent as well.
Without the step index, establishing $\LRt{}{\texttt{Eq}}{.}{.}$
would reduce to establishing $\LRt{}{\texttt{Eq}}{.}{.}$.
We are in a cycle. With the step index,
reduces to $\LRt{k_4}{\texttt{Eq}}{.}{.}$ where $k_4 < k_1$.
The step index represents the number of reduction steps we can take
and will be reduced for each reduction step.
Thus, we can give a well-founded definition of our logical relations.

Figure <ref> gives the step-indexed logical relations
to relate FG and TL terms.
Rule red-rel-exp relates FG and TL expressions.
The expressions are in a relation assuming that the resulting values are in a relation
where we impose a step limit on the number of reduction steps that can be taken.
We additionally find
parameters $\foreachN{D}$ and $\vbMethTL$ as FG and TL expressions refer to method definitions.

Rule red-rel-struct is straightforward.
Rule red-rel-iface has been motivated above.
We make use of the following helper function to lookup up the method definition
for a specific pair of method name and receiver type.
c  (x  t_S)  mM  {  e } ∈D
D(m,t_S) =  (x  t_S)  mM  {  e }

Rule red-rel-method covers method definitions.
Rule red-rel-vb ensures that the substitutions from free variables to values are related.
Rule red-rel-decls ensures that our labeling for the translation of method definitions is consistent.

A fundamental property of step-indexed logical relations is that
if two expressions are in a relation for $k$ steps then they are also in a relation
for any smaller number of steps.

Let $\redLRConfk{k}{t}{e}{\expT}$ and $k' \leq k$.
Then, we find that $\redLRConfk{k'}{t}{e}{\expT}$.

By induction over the derivation $\redLRConfk{k}{t}{e}{\expT}$.

Case red-rel-exp:

∀k_1 < k, k_2 < k, v, .

(k  - k_1 - k_2 > 0 ∧k_1Dev

k- k_1 - k_2tv

If either $e$ or $\expT$ is irreducible, $\redLRConfk{k'}{t}{e}{\expT}$
holds immediately because the universally quantified statement in the premise holds vacuously.

Otherwise, we find
for some $k_1$ and $k_2$. If $k' - k_1 - k_2 \leq 0$, $\redLRConfk{k'}{t}{e}{\expT}$ holds again immediately.

Otherwise, by induction applied on the premise of rule red-rel-exp
we find that $\redLRConfk{k'- k_1 - k_2}{t}{v}{\uT}$ and we are done for this case.

Case red-rel-struct:

t_S   { f  tn } ∈D

∀i ∈[n]. kt_iv_i_i

t_S { vn }
_t_S  (n)

Follows immediately by induction.

Case red-rel-iface:

= _u_S  '

(1)  ∀k_1 < k . k_1u_Sv

Dt_I = { m Mn }

(2)  ∀k_2 < k, i ∈[n] . k_2
m_i M_i

_t_I  (, n)

Consider the first premise (1).
If there exists $k_1 < k'$ then $\redLRConfk{k_1}{u_S}{v}{\uT}$. Otherwise,
this premise holds vacuously.
The same argument for $k_2 < k'$ applies to the second premise (2).
$\redLRConfk{k'}{t_I}{v}{\kT_{t_I} \ (\uT, \foreach{\uT_i}{n})}$.

A similar monotonicity result applies to method definitions and declarations.
Monotonicity is an essential property to obtain the following results.

Interface-value constructors and destructors preserve equivalent expressions via logical relations
as stated by the following results.

Let $\tdUpcast{\foreachN{D}}{\subtypeOf{t}{u}}{\expT_1}$
and $\redLRk{k}{}{}{\foreachN{D}}{\vbMethTL}$
and $\redLRConfk{k}{t}{e}{\expT_2}$.
Then, we find that $\redLRConfk{k}{u}{e}{\expT_1 \ \expT_2}$.

Let $\tdDowncast{\foreachN{D}}{\assertOf{t}{u}}{\expT_1}$
and $\redLRk{k}{}{}{\foreachN{D}}{\vbMethTL}$
and $\redLRConfk{k}{t}{e}{\expT_2}$.
Then, we find that $\redLRConfk{k}{u}{e.(u)}{\expT_1 \ \expT_2}$.

Based on the above we can show that target expressions resulting from FG expressions
and target methods resulting from FG methods are equivalent.

Let $\tdExpTrans{\pair{\foreachN{D}}{\fgEnv}}{e : t}{\expT}$
and $\vbFG$, $\vbTL$, $\vbMethTL$
such that
$\redLRk{k}{}{}{\foreachN{D}}{\vbMethTL}$ for some $k$.
Then, we find that $\redLRConfk{k}{t}{\vbFG(e)}{\vbTL(\expT)}$.

Let $\tdMethTrans{\foreachN{D}}
{\FUNC\ (x \ t_S) \ m (\foreach{x \ t}{n}) \ t \ \{ \RETURN\ e \}}
{\lambda \xT . \lambda (\foreach{\xT }{n}). \expT}$.
Then, we find that $\redLRk{k}{}{}{\foreachN{D}}{\vbMethTL}$ where $\vbMethTL(\mT{m}{t_S}) = \lambda \xT . \lambda (\foreach{\xT }{n}). \expT$ for any $k$.

The lengthy proofs of the above results are given in the appendix.

From Lemmas <ref> and <ref>
we can derive our main result that the dictionary-passing translation preserves the dynamic behavior of FG programs.

Let $\tdProgTrans{\ignore{\PACKAGE\ \MAIN;} \foreachN{D} \ \FUNC\ \MAIN () \{ \_ = e \}}
{\LET\ \foreach{\mT{m_i}{{t_S}_i} = \expT_i}{n} \ \IN\ \expT}$
where we assume that $e$ has type $t$.
Then, we find that
for any $k$
where $\vbMethTL = \Angle{\foreach{\subst{\mT{m_i}{{t_S}_i}}{\expT_i}}{n}}$.

Follows from Lemmas <ref> and <ref>.

Our main result also implies that our translation is coherent.
Recall that the translation rules are non-syntax directed because of rule  td-sub.
Hence, we could for example insert an (albeit trivial) interface-value constructor resulting from
Hence, there might be different target terms for the same source term.
Our main result guarantees that all targets obtained
preserve the meaning of the original program.

§ RELATED WORK AND CONCLUSION

The dictionary-passing translation is well-studied in the context of
Haskell type classes [24]. A type class
constraint translates to an extra function parameter, constraint resolution
provides a dictionary with the methods of the type class for this parameter.
In our translation from Featherweight Go [7], dictionaries are not
supplied as separate parameters because FG does
not support parametric polymorphism. Instead, a dictionary is always passed as part
of an interface-value, which combines the dictionary with the concrete
value implementing the interface. Thus, interface-values can be viewed as
representations of
existential types [13, 10, 23].
How to adapt our dictionary-passing translation scheme to FG extended with parametric polymorphism (generics)
is something we plan to consider in future work.

In the context of type classes it is common to show
that resulting target programs are well-typed.
For example, see the work by Hall and coworkers [8].
Typed target terms in this setting require System F
and richer variants depending on the kind of type class extensions
that are considered [19].
Our target terms are untyped and
we pattern match over constructors to check for “run-time types”.
For example, see rule td-destr-iface-struct in Figure <ref>.
There are various ways to support dynamic typing in a typed setting.
For example, we could employ GADTs as described by
Peyton Jones and coworkers [9].
A simply-typed first order functional language with GADTs appears then to be sufficient
as a typed target language for Featherweight Go.
This will require certain adjustments to our dictionary-passing translation.
We plan to study the details in future work.

Another important property in the type class context is coherence.
Bottu and coworkers [3] make use of logical relations
to state equivalence among distinct target terms resulting
from the same source type class program.
Thanks to our main result Theorem <ref>, we get coherence for free.
We believe it is worthwhile to establish a property similar to Theorem <ref> for type classes.
We could employ a simple denotational semantics
for source type class programs
such as [21, 14]
which is then related to target programs obtained via the dictionary-passing translation.
This is something that has not been studied so far
and another topic for future work.

Method dictionaries bear some resemblance to virtual method tables
(vtables) used to implement virtual method dispatch in
object-oriented languages [5].
The main difference between vtables and
dictionaries is that there is a fixed connection between an object and its
vtable (via the class of the object), whereas the connection between a
value and a dictionary may change at runtime, depending on the type
the value is used at. Dictionaries allow access to a method at a fixed
offset, whereas vtables in the presence of multiple inheritance require
a more sophisticated lookup algorithm [2].

Subtyping for interfaces in Go is based purely on width subtyping,
there is no support for depth subtyping [15]: a subtype
might provide more methods than the super-interface, but method signatures
must match invariantly. Method dispatch in Go is performed only
on the receiver of the method call. Multi-dispatch [18, 4]
refers to the ability to dispatch on multiple arguments, but this approach
turns out to be difficult in combination with structural subtyping [11].

To summarize the results of the paper at hand: we defined a dictionary-passing
translation from Featherweight Go to a untyped lambda calculus with pattern matching.
The compiler for the full Go language [22] employs a similar
dictionary-passing approach. We proved that the translation preserves
the dynamic semantics of Featherweight Go, using step-indexed logical

[1]
A. Ahmed.
Step-indexed syntactic logical relations for recursive and quantified
In Proc. of ESOP'06, LNCS. Springer-Verlag, 2006.

[2]
B. Alpern, A. Cocchi, S. J. Fink, D. Grove, and D. Lieber.
Efficient implementation of Java interfaces: Invokeinterface
considered harmless.
In Proc. of OOPSLA 2001. ACM, 2001.

[3]
G.-J. Bottu, N. Xie, K. Marntirosian, and T. Schrijvers.
Coherence of type class resolution.
Proc. ACM Program. Lang., 3(ICFP), July 2019.

[4]
C. Chambers.
Object-oriented multi-methods in cecil.
In Proc. of ECOOP 1992, volume 615 of LNCS. Springer,

[5]
K. Driesen and U. Hölzle.
The direct cost of virtual function calls in C++.
In Proc. of OOPSLA 1996. ACM, 1996.

[6]
J. Gosling, B. Joy, G. Steele, G. Bracha, A. Buckley, D. Smith, and G. Bierman.
The Java language specification, Java SE 16 edition.
Feb. 2021.

[7]
R. Griesemer, R. Hu, W. Kokke, J. Lange, I. L. Taylor, B. Toninho, P. Wadler,
and N. Yoshida.
Featherweight Go.
Proc. ACM Program. Lang., 4(OOPSLA), Nov. 2020.

[8]
C. V. Hall, K. Hammond, S. L. Peyton Jones, and P. L. Wadler.
Type classes in Haskell.
ACM Trans. Program. Lang. Syst., 18(2), Mar. 1996.

[9]
S. P. Jones, S. Weirich, R. A. Eisenberg, and D. Vytiniotis.
A reflection on types.
In S. Lindley, C. McBride, P. W. Trinder, and D. Sannella, editors,
A List of Successes That Can Change the World - Essays Dedicated to
Philip Wadler on the Occasion of His 60th Birthday, volume 9600 of LNCS. Springer, 2016.

[10]
K. Läufer.
Type classes with existential types.
Journal of Functional Programming, 6(3), 1996.

[11]
D. Malayeri and J. Aldrich.
Integrating nominal and structural subtyping.
In Proc. of ECOOP 2008, volume 5142 of LNCS. Springer,

[12]
S. Marlow.
Haskell 2010 language report.
<https://www.haskell.org/onlinereport/haskell2010/>, 2010.

[13]
J. C. Mitchell and G. D. Plotkin.
Abstract types have existential type.
ACM Trans. Program. Lang. Syst., 10(3), 1988.

[14]
J. G. Morris.
A simple semantics for Haskell overloading.
In Proc. of Haskell'14, Haskell '14, New York, NY, USA, 2014.

[15]
B. Pierce.
Types and Programming Languages.
The MIT Press, 1st edition, 2002.

[16]
G. Plotkin.
Lambda-definability and logical relations.
Unpublished manuscript, 1973.

[17]
J. H. Reppy.
Concurrent ML: Design, application and semantics.
In Functional Programming, Concurrency, Simulation and Automated
Reasoning, number 693 in LNCS. Springer-Verlag, New York, NY, 1993.

[18]
G. L. Steele.
Common LISP: The Language (2nd Ed.).
Digital Press, USA, 1990.

[19]
M. Sulzmann, M. M. T. Chakravarty, S. P. Jones, and K. Donnelly.
System F with type equality coercions.
In Proc. of TLDI'07, TLDI '07, New York, NY, USA, 2007. ACM.

[20]
W. W. Tait.
Intensional interpretations of functionals of finite type I.
J. Symb. Log., 32(2), 1967.

[21]
S. R. Thatte.
Semantics of type classes revisited.
In Proc. of LISP'94, pages 208–219. ACM, 1994.

[22]
The Go programming language.
<https://golang.org>, 2021.

[23]
P. Thiemann and S. Wehr.
Interface types for Haskell.
In Proc. of APLAS 2008, volume 5356 of LNCS, Bangalore,
India, 2008. Springer.

[24]
P. Wadler and S. Blott.
How to make ad-hoc polymorphism less ad hoc.
In Proc. of POPL 1989, New York, NY, USA, 1989. ACM.

§ PROOFS FOR PROPERTIES STATED IN THE MAIN TEXT

§.§ Monotonicity for Method Definitions and Declarations

Let $\redLRConfk{k}{m M}{\FUNC\ (x \ t_S) \ mM \ \{ \RETURN\ e \}}{\uT}$ and $k' \leq k$.
Then, we find that $\redLRConfk{k'}{m M}{\FUNC\ (x \ t_S) \ mM \ \{ \RETURN\ e \}}{\uT}$.

Follows immediately by observing the premise of rule red-rel-method.

Let $\redLRk{k}{}{}{\foreachN{D}}{\vbMethTL}$ and $k' \leq k$.
Then, we find that $\redLRk{k'}{}{}{\foreachN{D}}{\vbMethTL}$.

Follows via Lemma <ref>.

§.§ Lemma <ref>

We show that $\redLRConfk{k}{u}{e}{\expT_1 \ \expT_2}$ by
making use of the following auxiliary statement.

Let $\tdUpcast{\foreachN{D}}{\subtypeOf{t}{u}}{\expT}$
and $\redLRk{k}{}{}{\foreachN{D}}{\vbMethTL}$
and $\redLRConfk{k}{t}{v}{\uT}$.
Then, we find that $\redLRConfk{k}{u}{v}{\expT \ \uT}$.

Suppose $k_1 < k$ and $k_2 < k$ and $k - k_1 - k_2 > 0$
and (1) $\reduceFGk{k_1}{\foreachN{D}}{e}{v}$ for some $v$
and (2) $\reduceTLk{k_2}{\vbMethTL}{\expT_2}{\uT}$ for some $\uT$.
Based on the assumption that $\redLRConfk{k}{t}{e}{\expT_2}$
and via rule red-rel-exp we conclude that
$\redLRConfk{k - k_1 - k_2}{t}{v}{\uT}$.

Via the auxiliary statement we conclude that
(3) $\redLRConfk{k - k_1 - k_2}{u}{v}{\expT_1 \ \uT}$.

Via rule red-rel-exp making use of (1), (2) and (3)
we conclude that $\redLRConfk{k}{u}{e}{\expT_1 \ \expT_2}$ and we are done.

Proof of auxiliary statement.

We have to show that for all $k_2 < k$
where $k - k_2 > 0$ and $\reduceTLk{k_2}{\vbMethTL}{\expT \ \uT}{\uT'}$
we have that $\redLRConfk{k-k_2}{t}{v}{\uT'}$.

We perform a case analysis of the derivation for $\tdUpcast{\foreachN{D}}{\subtypeOf{t}{u}}{\expT}$
and label the assumptions
(1) $\redLRk{k}{}{}{\foreachN{D}}{\vbMethTL}$
and (2) $\redLRConfk{k}{t}{v}{\uT}$ for later reference.

Case td-cons-struct-iface:

t_I   { S } ∈D

Dt_S ⊇S

S = m Mn

_t_I  (, m_it_Sn)

Set $\expT = \lambda \xT. \kT_{t_I} \ (\xT, \foreach{\mT{m_i}{t_S}}{n})$.
Then, (3) $\reduceTLk{1}{\vbMethTL}{\expT \ \uT}{\uT'}$
where $\uT' = \kT_{t_I} \ (\uT, \foreach{\mT{m_i}{t_S}}{n})$.

From (1) and Lemma <ref> we obtain
(4) $\forall k_1 < k. \redLRk{k_1}{}{}{\foreachN{D}}{\vbMethTL}$.

From (2) and Lemma <ref> we obtain
(5) $\forall k_2 < k. \redLRConfk{k_2}{t_S}{v}{\uT}$ (for this case $t = t_S$).

From (4), (5) and via rule red-rel-iface we obtain
(6) $\redLRConfk{k}{t_I}{v}{\uT'}$.

From (3), (6) and via rule red-rel-exp we obtain
$\redLRConfk{k}{t_I}{v}{\expT \ \uT}$ and we are done for this case.

Case td-cons-iface-iface:

t_I   { R_in } ∈D

u_I   { S_iq } ∈D

S_i = R_(i)   i ∈[q]

λ.                             _t_I  (, _in)
→_u_I  (, _(i)q)

From (2) and for this case we can conclude via rule red-rel-iface
that (3) $\uT = \kT_{t_I} \ (\uT', \foreach{\uT_i}{n})$
for some $u_S$, $\uT'$ and $\foreach{\uT_i}{n}$
$\methodSpecifications{\foreachN{D}}{t_I} = \{ \foreach{m_i M_i}{n} \}$
(4) $\forall k_1 < k . \redLRConfk{k_1}{u_S}{v}{\uT'}$
(5) $\forall k_2 < k, i \in [n] . \redLRConfk{k_2}{m_i M_i}{\methodLookup{\foreachN{D}}{(m_i,u_S)}}{\uT_i}$.

Set $\expT = \lambda \xT. \CASE\,\xT\,\OF\
\kT_{t_I} \ (\xTval, \foreach{\xT_i}{n})
\rightarrow
\kT_{u_I} \ (\xTval, \foreach{\xT_{\mapPerm(i)}}{q})$.
Then, (6) $\reduceTLk{1}{\vbMethTL}{\expT \ \uT}{\uT''}$
where (7) $\uT'' = \kT_{u_I} \ (\uT', \foreach{\uT_{\mapPerm(i)}}{q})$.

From (4), (5) and (7) via rule red-rel-iface we obtain that
(8) $\redLRConfk{k}{u_I}{v}{\uT''}$.

From (6), (8) and via rule red-rel-exp we obtain
$\redLRConfk{k}{u_I}{v}{\expT \ \uT}$ and we are done.

§.§ Lemma <ref>

We first introduce an auxiliary statement.

Let $\redLRConfk{k}{t}{e'}{\expT'}$
and $\reduceFGk{k_1}{\foreachN{D}}{e}{e'}$
and $\reduceTLk{k_2}{\vbMethTL}{\expT}{\expT'}$.
Then, we find that $\redLRConfk{k + k_1 + k_2}{t}{e}{\expT}$

If either $e'$ or $\expT'$ are irreducible the result follows immediately.

Otherwise, based on rule red-rel-exp we find that
and $\reduceTLk{k_2'}{\vbMethTL}{\expT'}{\uT}$
and $\redLRConfk{k-k_1' - k_2'}{t}{v}{\uT}$.

Based on the above, our assumptions and rule red-rel-exp
we find that $\redLRConfk{k + k_1 + k_2}{t}{e}{\expT}$ and we are done.

Here comes the proof of Lemma <ref>.

We perform a case analysis of the derivation $\tdDowncast{\foreachN{D}}{\assertOf{t}{u}}{\expT_1}$
and label the assumptions
(1) $\redLRk{k}{}{}{\foreachN{D}}{\vbMethTL}$
and (2) $\redLRConfk{k}{t}{e}{\expT_2}$ for later reference.

Case td-destr-iface-struct:

t_I   { Sn } ∈D

Dt_It_Sλ.                        _t_I  (K_t_S  , n)

We set $\expT_1  = \lambda \xT.  \CASE\,\xT\,\OF\
\kT_{t_I} \ (K_{t_S} \ \foreachN{\yT}, \foreach{\xT}{n})
\rightarrow K_{t_S} \ \foreachN{\yT}$.

From (2) and via rule red-rel-exp we conclude that
forall  $k_1 < k$, $k_2 < k$, $v$, $\uT$ where
(3) $k  - k_1 - k_2 > 0$
(4) $\reduceFGk{k_1}{\foreachN{D}}{e}{v}$
(5) $\reduceTLk{k_2}{\vbMethTL}{\expT_2}{\uT}$
we have that
(6) $\redLRConfk{k- k_1 - k_2}{t_I}{v}{\uT}$.

From (6) and rule red-rel-iface we conclude that
(7) $\uT = \kT_{t_I} \ (\RepK{u_S}, \uT, \foreach{\uT_i}{n})$
where $\uT = \kT_{u_S} \ \foreachN{\uT'}$ and for all (8) $k_1' < k- k_1 - k_2$ we have that
(9) $\redLRConfk{k_1'}{u_s}{v}{\uT}$.

Subcase $t_S \not = u_S$:
Neither $e.(t_S)$ nor $\expT_1 \ \expT_2$ are reducible and
therefore we immediately can conclude that
$\redLRConfk{k}{t_S}{e}{\expT_1 \ \expT_2}$ holds.

Subcase $t_S = u_S$:
From (4) we conclude that
(10) $\reduceFGk{k_1 + 1}{\foreachN{D}}{e.(t_S)}{v}$.

From (5) and (7) we conclude that
(11) $\reduceTLk{k_2 + 3}{\vbMethTL}{\expT_1 \ \expT_2}{\uT}$.
There are three additional reduction steps
as we have one extra lambda and two extra pattern match applications.

From (8) and (9) and the Monotonicity Lemma <ref> we conclude that
$\redLRConfk{k- (k_1+1) - (k_2 + 3)}{t_s}{v}{\uT}$ and via rule red-rel-exp
we obtain that $\redLRConfk{k}{t_S}{e}{\expT_1 \ \expT_2}$ and we are done for this case.

Case td-destr-iface-iface:

t_I   { Sn } ∈D

[ _t_S   →( )
|Dt_Su_I ]

_t_I  (, n) →

We set $\expT_1 = \lambda \xT.
\CASE\ \ \xT \ \OF\
\kT_{t_I} \ (\xTval, \foreach{\xT}{n}) \rightarrow \CASE\ \xTrep \ \OF\ \foreachN{\clsT}$.

We apply similar reasoning as in case of td-destr-iface-struct.

From (2) and via rule red-rel-exp we conclude that
forall  $k_1 < k$, $k_2 < k$, $v$, $\uT$ where
(3) $k  - k_1 - k_2 > 0$
(4) $\reduceFGk{k_1}{\foreachN{D}}{e}{v}$
(5) $\reduceTLk{k_2}{\vbMethTL}{\expT_2}{\uT}$
we have that
(6) $\redLRConfk{k- k_1 - k_2}{t_I}{v}{\uT}$.

From (6) and rule red-rel-iface we conclude that
(7) $\uT = \kT_{t_I} \ (\uT, \foreach{\uT_i}{n})$
where $\uT = \kT_{t_S} \ \foreachN{\uT'}$ and for all (8) $k_1' < k- k_1 - k_2$ we have that
(9) $\redLRConfk{k_1'}{t_s}{v}{\uT}$.
We use here $t_S$ (instead of $u_S$) to match the naming conventions
in the premise of rule td-destr-iface-iface.

Subcase $\fgSub{\foreachN{D}}{t_S}{u_I}$ does not hold:
Neither $e.(t_S)$ nor $\expT_1 \ \expT_2$ are reducible and
therefore we immediately can conclude that
$\redLRConfk{k}{t_S}{e}{\expT_1 \ \expT_2}$ holds.

Subcase $\fgSub{\foreachN{D}}{t_S}{u_I}$ does hold:
From (4) we conclude that
(10) $\reduceFGk{k_1}{\foreachN{D}}{e.(u_I)}{v}$.

From (5) and (7) we conclude that
(11) $\reduceTLk{k_2 + 3}{\vbMethTL}{\expT_1 \ \expT_2}{\expT \ \uT}$
where (12) $\tdUpcast{\foreachN{D}}{\subtypeOf{t_S}{u_I}}{\expT}$.
There are three additional reduction steps
as we have one extra lambda and two extra pattern match applications.
The upcast $\expT$ has not been applied.

From (6) and (12) and Lemma <ref> we obtain that
(13) $\redLRConfk{k_1'}{u_I}{v}{\expT \ \uT}$.

Via the Monotonicity Lemma <ref> and Lemma <ref> we obtain that
$\redLRConfk{k}{u_I}{e.(u_I)}{\expT_1 \ \expT_2}$ and we are done.

§.§ Lemma <ref>

By induction over the derivation $\tdExpTrans{\pair{\foreachN{D}}{\fgEnv}}{e : t}{\expT}$.
We label the assumptions   (1) $\redLRk{k}{\triple{\foreachN{D}}{\vbMethTL}{\fgEnv}}{}{\vbFG}{\vbTL}$
(2) $\redLRk{k}{}{}{\foreachN{D}}{\vbMethTL}$ as well as the to be proven
statement (3) $\redLRConfk{k}{t}{\vbFG(e)}{\vbTL(\expT)}$ for some later reference.

Case td-var:

(x : t) ∈
Dx : t

(3) follows immediately from (1).

Case td-struct:

t_S   { f_i  t_in } ∈D

De_i : t_i_i  i ∈[n]

Dt_S { e_in } : t_S _t_S  (_in)

Suppose there exists $k_1 < k$ and $k_2 < k$ and $v$ and $\uT$
such that
$(k  - k_1 - k_2 > 0$
(4) $\reduceFGk{k_1}{\foreachN{D}}{\vbFG(t_s \{ \foreach{e_i}{n} \})}{t_s \{ \foreach{v_i}{n} \}}$
(5) $\reduceTLk{k_2}{\vbMethTL}{\vbTL(\kT_{t_S} \ (\foreach{\expT_i}{n}))}{\kT_{t_S} \ (\foreach{\uT_i}{n})}$
for $i \in [n]$.

From (4) and (5) we conclude that
(6) $\reduceFGk{k_1'}{\foreachN{D}}{\vbFG(e_i)}{v_i}$
(7) $\reduceTLk{k_2'}{\vbMethTL}{\vbTL(\expT_i)}{\uT_i}$
for $i \in [n]$ where we pick $k_1'$ and $k_2$' such that $k_1' < k_1$ and $k_2' < k_2$
and all the subreductions yield some value.

By induction (8) $\redLRConfk{k}{t_i}{\vbFG(e_i)}{\vbTL(\expT_i)}$ for $i \in [n]$.

From (6), (7), (8) and via rule red-rel-exp we conclude that
(9) $\redLRConfk{k-k_1'-k_2'}{t_i}{v_i}{\uT_i}$ for $i \in [n]$.

From (9) and rule red-rel-struct we conclude that
(10) $\redLRConfk{k-k_1'-k_2'}{t_S}{t_S \{ \foreach{v_i}{n} \}}{\kT_{t_S} \ (\foreach{\uT_i}{n})}$.

From (10) and Lemma <ref> we conclude that
(11) $\redLRConfk{k-k_1-k_2}{t_S}{t_S \{ \foreach{v_i}{n} \}}{\kT_{t_S} \ (\foreach{\uT_i}{n})}$.

From (4), (5), (11) and via rule red-rel-exp we conclude that
$\redLRConfk{k}{t_S}{\vbFG(t_s \{ \foreach{e_i}{n} \})}{\vbTL(\kT_{t_S} \ (\foreach{E_i}{n}))}$
and we are done for this case.

Case td-access:

De : t_S

t_S   { f_j  t_jn } ∈D

e.f_i : t_i
_t_S  (_jn) →_i

Similar reasoning as in case of td-struct.

Case td-call-struct:

m (x_i  t_in)  t ∈Dt_S

De : t_S

De_i : t_i_i  i ∈[n]

De.m(e_in) : tmt_S   (_in)

Suppose there exists $k_1 < k$ and $k_2 < k$ and $v$ and $\uT$
such that
$(k  - k_1 - k_2 > 0$
(4) $\reduceFGk{k_1}{\foreachN{D}}{\vbFG(e.m(\foreach{e_i}{n}))}{v}$
(5) $\reduceTLk{k_2}{\vbMethTL}{\vbTL(\mT{m}{t_S} \ \expT \ (\foreach{\expT_i}{n}))}{\uT}$.

From the assumptions and (4) we conclude that
(4a) $\reduceFGk{1}{\foreachN{D}}{\vbFG(e.m(\foreach{e_i}{n}))}{\Angle{\subst{x}{\vbFG(e)},\foreach{\subst{x_i}{\vbFG(e_i)}}{n}} e'}$
(4b) $\reduceFGk{k_1 - 1}{\foreachN{D}}{\Angle{\subst{x}{\vbFG(e)},\foreach{\subst{x_i}{\vbFG(e_i)}}{n}} e'}{v}$
where (4c) $\FUNC\ (x \ t_S) \ m (\foreach{x_i \ t_i}{n}) \ t \ \{ \RETURN\ e' \} \in \foreachN{D}$.

From (4) we conclude that
(6) $\reduceFGk{k_1'}{\foreachN{D}}{\vbFG(e)}{v'}$
(7) $\reduceFGk{k_1'}{\foreachN{D}}{\vbFG(e_i)}{v_i}$
for some $v'$ and $v_i$ for $i \in [n]$ where $k_1' < k_1$.
We pick again some large enough $k_1'$ such that all subreductions yields some value.

Similarly, from (5) we conclude that
(8) $\reduceTLk{k_2'}{\vbMethTL}{\vbTL(\expT)}{\uT'}$
(9) $\reduceTLk{k_2'}{\vbMethTL}{\vbTL(\expT_i)}{\uT_i}$
for some $\uT'$ and $\uT_i$ for $i \in [n]$ where $k_2' < k_2$.

By induction we have that
(10) $\redLRConfk{k}{t_S}{\vbFG(e)}{\vbTL(\expT)}$
(11) $\redLRConfk{k}{t_i}{\vbFG(e_i)}{\vbTL(\expT_i)}$ for $i \in [n]$.

From (6), (8), (10) and via rule red-rel-exp we conclude that
(12) $\redLRConfk{k-k_1'-k_2'}{t_S}{v'}{\uT'}$.

Similarly, from (7), (9), (11) and via rule red-rel-exp we conclude that
(13) $\redLRConfk{k-k_1'-k_2'}{t_i}{v_i}{\uT_i}$ for $i \in [n]$.

From (4c), (12), (13), (3) and via rule red-rel-method we conclude that
(14) $\redLRConfk{k-k_1'-k_2'}{t}{\Angle{\subst{x}{v},\foreach{\subst{x_i}{v_i}}{n}} e'}{\mT{m}{t_S} \ \uT' \ (\foreach{\uT_i}{n})}$.

Based on our choice of $k_1'$ and $k_2'$ we conclude that
(15) $\reduceFGk{k_1 - k_1'}{\foreachN{D}}{\Angle{\subst{x}{v},\foreach{\subst{x_i}{v_i}}{n}} e'}{v}$
(16) $\reduceTLk{k_2 - k_2'}{\vbMethTL}{\mT{m}{t_S} \ \uT' \ (\foreach{\uT_i}{n})}{\uT}$.
That is, with $k_1 - k_1'$ steps or less we reach $v$ because $k_1$ is the overall number of steps required
and $k_1'$ is the maximum number of one of the subcomputation steps.
The same applies to $k_2 - k_2'$.

From (14), (15), (16) and via rule red-rel-exp we conclude that
$\redLRConfk{k - k_1 - k_2}{t}{v}{\uT}$ where we make use of the fact that
$k - k_1' - k_1' - (k_1 - k_1') - (k_2 - k_2') = k - k_1 - k_2$.
Thus, we are done for this case.

Case td-call-iface:

De : t_I

t_I   { S_iq } ∈D

S_j = m(x_i  t_in)  t  (for some j ∈[q])

De_i : t_i_i  i ∈[n]

e.m(e_in) : t
_t_I  (, _iq) →_j   (_in)

Similar reasoning as in case of td-call-struct.
We set

$$\expT' = \CASE\ \ \expT \ \OF\ \kT_{t_I} \ (\_, \xTval, \foreach{\xT_i}{q}) \rightarrow \xT_j \ \xTval \ (\foreach{\expT_i}{n}).$$

Suppose there exists $k_1 < k$ and $k_2 < k$ and $v$ and $\uT$
such that
$(k  - k_1 - k_2 > 0$
(4) $\reduceFGk{k_1}{\foreachN{D}}{\vbFG(e.m(\foreach{e_i}{n}))}{v}$
(5) $\reduceTLk{k_2}{\vbMethTL}{\vbTL(\expT')}{\uT}$.

From the assumptions and (4) we conclude that
(4a) $\reduceFGk{1}{\foreachN{D}}{\vbFG(e.m(\foreach{e_i}{n}))}{\Angle{\subst{x}{\vbFG(e)},\foreach{\subst{x_i}{\vbFG(e_i)}}{n}} e'}$
(4b) $\reduceFGk{k_1 - 1}{\foreachN{D}}{\Angle{\subst{x}{\vbFG(e)},\foreach{\subst{x_i}{\vbFG(e_i)}}{n}} e'}{v}$
where (4c) $\FUNC\ (x \ t_S) \ m (\foreach{x_i \ t_i}{n}) \ t \ \{ \RETURN\ e' \} \in \foreachN{D}$.

From (4) we conclude that
(6) $\reduceFGk{k_1'}{\foreachN{D}}{\vbFG(e)}{v'}$
(7) $\reduceFGk{k_1'}{\foreachN{D}}{\vbFG(e_i)}{v_i}$
for some $v'$ and $v_i$ for $i \in [n]$ where $k_1' < k_1$.
We pick again some large enough $k_1'$ such that all subreductions yields some value.

Similarly, from (5) we conclude that
(8) $\reduceTLk{k_2'}{\vbMethTL}{\vbTL(\expT)}{\uT'}$
(9) $\reduceTLk{k_2'}{\vbMethTL}{\vbTL(\expT_i)}{\uT_i}$
for some $\uT'$ and $\uT_i$ for $i \in [n]$ where $k_2' < k_2$.

By induction we have that
(10) $\redLRConfk{k}{t_S}{\vbFG(e)}{\vbTL(\expT)}$
(11) $\redLRConfk{k}{t_i}{\vbFG(e_i)}{\vbTL(\expT_i)}$ for $i \in [n]$.

From (6), (8), (10) and via rule red-rel-exp we conclude that
(12) $\redLRConfk{k-k_1'-k_2'}{t_I}{v'}{\uT'}$.

Similarly, from (7), (9), (11) and via rule red-rel-exp we conclude that
(13) $\redLRConfk{k-k_1'-k_2'}{t_i}{v_i}{\uT_i}$ for $i \in [n]$.

From (12) and via red-rel-iface we conclude that
(13) $\uT' = \kT_{t_I} \ (\uT'', \foreach{\uT'_i}{p})$
$\uT'' = \kT_{t_S} \ \foreachN{\uT'''}$
(14) $\redLRConfk{k''}{t_S}{v'}{\uT''}$
(15) $\redLRConfk{k''}{m(\foreach{x_i \ t_i}{n})}{\FUNC\ (x \ t_S) \ m (\foreach{x_i \ t_i}{n}) \ t \ \{ \RETURN\ e' \}}{\uT'_j}$ for some $k''$
where $k'' < k - k_1' - k_2'$ and $j \in [q]$ is the same $j$ as in the premise of rule td-call-iface.

From (15) via rule red-rel-method and (14) and (13) plus the Monotonicity Lemma <ref>
we conclude that
(16) $\redLRConfk{k''}{t}{\Angle{\subst{x}{v'},\foreach{\subst{x_i}{v_i}}{n}} e'}{\uT'_j \ \uT'' \ (\foreach{\uT_i}{n})}$.

For concreteness, we can assume $k'' = k - k_1' - k_2' - 1$.
Based on our choice of $k_1'$ and $k_2'$ we conclude that
(17) $\reduceFGk{k_1 - k_1'}{\foreachN{D}}{\Angle{\subst{x}{v},\foreach{\subst{x_i}{v_i}}{n}} e'}{v}$
(18) $\reduceTLk{k_2 - k_2' + 1}{\uT'_j \ \uT'' \ (\foreach{\uT_i}{n})}{\uT}$.
The argument is the same as in case of td-call-struct.

From (16), (17), (18) and via rule red-rel-exp we conclude that
$\redLRConfk{k - k_1 - k_2}{t}{v}{\uT}$ and we are done for this case.

Case td-sub:

De : t_2

De : u_1  _2

By induction we obtain that
(4) $\redLRConfk{k}{t}{\vbFG(e)}{\vbTL(\expT_2)}$.
From (3), (4) and Lemma <ref>  we obtain that
$\redLRConfk{k}{u}{\vbFG(e)}{\expT_1 \ \vbTL(\expT_2)}$.

We have that $\vbTL(\expT_1) = \expT_1$ and thus we are done for this case.

Case td-assert:

De : u_2

De.(t) : t_1  _2

By induction we obtain that
(4) $\redLRConfk{k}{u}{\vbFG(e)}{\vbTL(\expT_2)}$.
From (3), (4) and Lemma <ref>  we obtain that
$\redLRConfk{k}{t}{\vbFG(e).(t)}{\expT_1 \ \vbTL(\expT_2)}$.

We have that $\vbTL(\expT_1) = \expT_1$ and thus we are done for this case.

§.§ Lemma <ref>

Based on rules red-rel-decls and red-rel-method,

$$\FUNC\ (x \ t_S) \ m (\foreach{x_i \ t_i}{n}) \ t \ \{ \RETURN\ e \} \in \foreachN{D}$$

we have to show that

∀k' ≤k,
v', ', v_in, _in.
∧(∀i ∈[n]. k't_iv_i_i))

(1)  k'
⦜xv',x_iv_in e
(xt_S  ')  (_in)

We verify the result by induction on $k$.

Case $k=1$: We must perform several reductions on $(\mT{x}{t_S} \ \uT') \ (\foreach{\uT_i}{n})$
to obtain a value. Due to $k=1$ the premise of rule red-rel-exp holds vacuously.
Therefore, we can immediately establish (1).

Case $k \implies k+1$:
Suppose $k' \leq k+1$
and (2) $\redLRConfk{k'}{t_S}{v'}{\uT'}$
and (3) $\redLRConfk{k'}{t_i}{v_i}{\uT_i}$
for some $v'$, $\uT'$, $v_i$, $\uT_i$ for $i \in [n]$.

Suppose $\Angle{\subst{x}{v'},\foreach{\subst{x_i}{v_i}}{n}} e$
and $(\mT{x}{t_S} \ \uT') \ (\foreach{\uT_i}{n})$ are reducible.
Otherwise, the result holds immediately.

We have to show that for
(4) $\reduceFGk{k_1}{\foreachN{D}}{\Angle{\subst{x}{v'},\foreach{\subst{x_i}{v_i}}{n}} e}{v''}$
(5) $\reduceTLk{k_2}{\vbMethTL}{(\mT{x}{t_S} \ \uT') \ (\foreach{\uT_i}{n})}{\uT''}$
and $k+1-k_1 - k_2 > 0$
we have that
(6) $\redLRConfk{k + 1 - k_1 - k_2}{t}{v''}{\uT''}$.

From (5) we can conclude that
(7) $\vbMethTL \turnsTL (\mT{x}{t_S} \ \uT') \ (\foreach{\uT_i}{n})
\reduceSym^{1}
\lambda X . \lambda (\foreach{X_i }{n}). \expT
\reduceSym^{2} \Angle{\subst{\xT}{\uT'},\foreach{\subst{\xT_i}{\uT_i}}{n}} \expT
\reduceSym^{k_2'} \uT''$ where (8) $k_2 = k_2' + 3$.

By induction we have that (9) $\redLRk{k}{}{}{\foreachN{D}}{\vbMethTL}$.

From (2) and (3) and the Monotonicity Lemma <ref>
we find that
(10) $\redLRConfk{k''}{t_S}{v'}{\uT'}$
and (11) $\redLRConfk{k''}{t_i}{v_i}{\uT_i}$
where $k'' \leq k$ for $i \in [n]$.

By making use of (9), (10) and (11) we apply Lemma <ref>

{\FUNC\ (x \ t_S) \ m (\foreach{x_i \ t_i}{n}) \ t \ \{ \RETURN\ e \}}
{\lambda \xT . \lambda (\foreach{\xT_i }{n}). \expT}$$

and thus obtain that
(12) $\redLRConfk{k}{t}{\Angle{\subst{x}{v'},\foreach{\subst{x_i}{v_i}}{n}} e}{\Angle{\subst{\xT}{\uT'},\foreach{\subst{\xT_i}{\uT_i}}{n}} \expT}$.

From (12), (4) and (7) via rule red-rel-exp we conclude that
(11) $\redLRConfk{k-k_1-k_2'}{t}{v''}{\uT''}$.

From (8) we conclude that
(12) $k + 1 - k_1 - k_2 = k - k_1 - k_2' - 2$.

From (11), (12) and the Monotonicity Lemma <ref> we conclude that
$\redLRConfk{k-k_1-k_2'-2}{t}{v''}{\uT''}$ and we are done.