This paper gives a complete characterisation of type isomorphism definable by terms of a λ-calculus with intersection and union types. Unfortunately, when union is considered the Subject Reduction property does not hold in general. However, it is well known that in the λ-calculus, independently of the considered type system, the isomorphism between two types can be realised only by invertible terms. Notably, all invertible terms are linear terms. In this paper, the isomorphism of intersection and union types is investigated using a relevant type system for linear terms enjoying the Subject Reduction property. To characterise type isomorphism, a similarity between types and a type reduction are introduced. Types have a unique normal form with respect to the reduction rules and two types are isomorphic if and only if their normal forms are similar.

Isomorphism of intersection and union types

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

Abstract

This paper gives a complete characterisation of type isomorphism definable by terms of a λ-calculus with intersection and union types. Unfortunately, when union is considered the Subject Reduction property does not hold in general. However, it is well known that in the λ-calculus, independently of the considered type system, the isomorphism between two types can be realised only by invertible terms. Notably, all invertible terms are linear terms. In this paper, the isomorphism of intersection and union types is investigated using a relevant type system for linear terms enjoying the Subject Reduction property. To characterise type isomorphism, a similarity between types and a type reduction are introduced. Types have a unique normal form with respect to the reduction rules and two types are isomorphic if and only if their normal forms are similar.
27
5
603
625
http://journals.cambridge.org/article_S0960129515000304
Lambda-calculus, Intersection and union types, Isomorphism.
Coppo, Mario; Dezani-Ciancaglini, Mariangiola; Margaria, Ines; Zacchi, Maddalena
File in questo prodotto:
File Dimensione Formato  
mscs.pdf

Accesso aperto

Tipo di file: POSTPRINT (VERSIONE FINALE DELL’AUTORE)
Dimensione 276.52 kB
Formato Adobe PDF
276.52 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/1577838
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 2
  • ???jsp.display-item.citation.isi??? 2
social impact