Featherweight Generic Go 中方法重载与结构子类型化的类型导向字典传递翻译
A Type-Directed, Dictionary-Passing Translation of Method Overloading and Structural Subtyping in Featherweight Generic Go
AI总结：
本文提出一种从 FGG- 到无类型 lambda 演算的类型导向字典传递翻译，通过字典参数解析重载方法调用，并证明翻译保持动态语义且具有连贯性。
摘要：
Featherweight Generic Go（FGG）是一个最小核心演算，用于建模编程语言 Go 的基本特性。它支持重载方法、接口类型、结构子类型化和泛型。对 FGG 程序动态行为最直接的语义描述是基于接收者的运行时类型信息来解析方法调用。本文展示了一种不同的方法，通过定义从 FGG- 到无类型 lambda 演算的类型导向翻译。FGG- 包含 FGG 除类型断言之外的所有特性。FGG- 程序的翻译为方法的可用性提供证据，作为额外的字典参数，类似于 Haskell 类型类中已知的字典传递方法。然后，方法调用可以通过在字典中简单查找方法定义来解析。翻译映像中的每个程序与其源 FGG- 程序具有相同的动态语义。该结果的证明基于一个语法化的、步进索引的逻辑关系。步进索引确保了在存在递归接口类型和递归方法的情况下该关系的良基定义。尽管翻译是非确定性的，但它是连贯的。
英文摘要：
Featherweight Generic Go (FGG) is a minimal core calculus modeling the essential features of the programming language Go. It includes support for overloaded methods, interface types, structural subtyping and generics. The most straightforward semantic description of the dynamic behavior of FGG programs is to resolve method calls based on runtime type information of the receiver. This article shows a different approach by defining a type-directed translation from FGG- to an untyped lambda-calculus. FGG- includes all features of FGG but type assertions. The translation of an FGG- program provides evidence for the availability of methods as additional dictionary parameters, similar to the dictionary-passing approach known from Haskell type classes. Then, method calls can be resolved by a simple lookup of the method definition in the dictionary. Every program in the image of the translation has the same dynamic semantics as its source FGG- program. The proof of this result is based on a syntactic, step-indexed logical relation. The step-index ensures a well-founded definition of the relation in the presence of recursive interface types and recursive methods. Although being non-deterministic, the translation is coherent.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
