##
**Inheritance and explicit coercion.**
*(English)*
Zbl 0716.68012

Logic in computer science, Proc. 4th Annual Symp., Pacific Grove/CA (USA) 1989, 112-129 (1989).

Summary: [For the entire collection see Zbl 0713.00018.]

We present a method for providing semantic interpretations for languages which feature inheritance in the framework of statically checked, rich type disciplines. We illustrate our approach on an extension of the language Fun of Cardelli and Wegner, which we interpret via a translation into an extended polymorphic lambda calculus. Our approach interprets inheritances in Fun as coercion functions already definable in the target of the translation. Existing techniques in the theory of semantic domains can be then used to interpret the extended polymorphic lambda calculus, thus providing many models for the original language. Our method allows the simultaneous modeling of parametric polymorphism, recursive types, and inheritance, something that was regarded as problematic because of the seemingly contradictory characteristics of inheritance and type recursion on higher types.

We identify the main difficulty in providing interpretations for explicit type disciplines featuring inheritance,namely that programs can type- check in more than one way. Since interpretations follow the type- checking derivations, coherence theorems are required, (that is, one must prove that the meaning of a program does not depend on the way it was type-checked), and we do prove them for our semantic method. Interestingly, proving coherence in the presence of recursive types, variants, and abstract types forced us to reexamine fundamental equational properties that arise in proof theory (in the form of commutative reductions) and domain theory (in the form of strict vs. nonstrict functions).

We present a method for providing semantic interpretations for languages which feature inheritance in the framework of statically checked, rich type disciplines. We illustrate our approach on an extension of the language Fun of Cardelli and Wegner, which we interpret via a translation into an extended polymorphic lambda calculus. Our approach interprets inheritances in Fun as coercion functions already definable in the target of the translation. Existing techniques in the theory of semantic domains can be then used to interpret the extended polymorphic lambda calculus, thus providing many models for the original language. Our method allows the simultaneous modeling of parametric polymorphism, recursive types, and inheritance, something that was regarded as problematic because of the seemingly contradictory characteristics of inheritance and type recursion on higher types.

We identify the main difficulty in providing interpretations for explicit type disciplines featuring inheritance,namely that programs can type- check in more than one way. Since interpretations follow the type- checking derivations, coherence theorems are required, (that is, one must prove that the meaning of a program does not depend on the way it was type-checked), and we do prove them for our semantic method. Interestingly, proving coherence in the presence of recursive types, variants, and abstract types forced us to reexamine fundamental equational properties that arise in proof theory (in the form of commutative reductions) and domain theory (in the form of strict vs. nonstrict functions).

### MSC:

68N01 | General topics in the theory of software |

68N15 | Theory of programming languages |

03B40 | Combinatory logic and lambda calculus |

68Q55 | Semantics in the theory of computing |