On Isomorphism of 'Functional' Intersection and Union Types
| Autor: | Maddalena Zacchi, Ines Margaria, Mariangiola Dezani-Ciancaglini, Mario Coppo |
|---|---|
| Jazyk: | angličtina |
| Rok vydání: | 2015 |
| Předmět: |
FOS: Computer and information sciences
Computer Science - Logic in Computer Science Pure mathematics Computer science 0102 computer and information sciences Type (model theory) 01 natural sciences lcsh:QA75.5-76.95 Set (abstract data type) Congruence (geometry) Intersection ComputingMethodologies_SYMBOLICANDALGEBRAICMANIPULATION 0101 mathematics lcsh:Mathematics 010102 general mathematics Type isomorphism Union type Function (mathematics) lcsh:QA1-939 F.4.1 F.3.3 16. Peace & justice Type isomorphism Intersection and Union types Logic in Computer Science (cs.LO) TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES 010201 computation theory & mathematics Intersection and Union types lcsh:Electronic computers. Computer science Inverse limit Isomorphism |
| Zdroj: | ITRS Electronic Proceedings in Theoretical Computer Science, Vol 177, Iss Proc. ITRS 2014, Pp 53-64 (2015) |
| Popis: | Type isomorphism is useful for retrieving library components, since a function in a library can have a type different from, but isomorphic to, the one expected by the user. Moreover type isomorphism gives for free the coercion required to include the function in the user program with the right type. The present paper faces the problem of type isomorphism in a system with intersection and union types. In the presence of intersection and union, isomorphism is not a congruence and cannot be characterised in an equational way. A characterisation can still be given, quite complicated by the interference between functional and non functional types. This drawback is faced in the paper by interpreting each atomic type as the set of functions mapping any argument into the interpretation of the type itself. This choice has been suggested by the initial projection of Scott's inverse limit lambda-model. The main result of this paper is a condition assuring type isomorphism, based on an isomorphism preserving reduction. In Proceedings ITRS 2014, arXiv:1503.04377 |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|