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.
翻译:Featherweight Generic Go(FGG)是一种极小核心演算,用于建模编程语言Go的本质特性。它支持重载方法、接口类型、结构子类型以及泛型。对FGG程序动态行为最直接的语义描述是基于接收者的运行时类型信息解析方法调用。本文提出了一种不同的方法,即通过从FGG-到无类型λ演算的类型导向型翻译。FGG-包含了FGG的所有特性,但不含类型断言。FGG-程序的翻译为方法的可用性提供了证据,这些证据作为额外的字典参数传递,类似于Haskell类型类中已知的字典传递方法。随后,方法调用可通过在字典中简单查找方法定义来解析。翻译结果中的每个程序与其源FGG-程序具有相同的动态语义。该结果的证明基于语法的、阶索引的逻辑关系。阶索引确保了在存在递归接口类型和递归方法时,该关系的定义具有良基性。尽管该翻译是非确定性的,它仍保持一致性。