Type isomorphism is useful for retrieving library components, since a function in a library can have a type dierent 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 -model. The main result of this paper is a condition assuring type isomorphism, based on an isomorphism preserving reduction.

On Isomorphism of "Functional" Intersection and Union Types.

COPPO, Mario;DEZANI, Mariangiola;MARGARIA, Ines Maria;ZACCHI, Maddalena
2015-01-01

Abstract

Type isomorphism is useful for retrieving library components, since a function in a library can have a type dierent 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 -model. The main result of this paper is a condition assuring type isomorphism, based on an isomorphism preserving reduction.
7-th workshop on intersection types and related systems
Vienna
18 luglio 2014
EPTCS177
53
64
Type isomorphism, Intersection and Union types.
Coppo, Mario; Dezani-Ciancaglini, Mariangiola; Margaria, Ines; Zacchi, Maddalena
File in questo prodotto:
File Dimensione Formato  
cdmz-31-10-14.pdf

Accesso aperto

Tipo di file: PDF EDITORIALE
Dimensione 180.07 kB
Formato Adobe PDF
180.07 kB Adobe PDF Visualizza/Apri

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/2318/1522433
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus ND
  • ???jsp.display-item.citation.isi??? 1
social impact