Let |- be an intersection type system. We say that a term is |-simple (or just simple when the system |- is clear from the context) if system |- can prove that it has a simple type. In this paper we propose new typing rules and algorithms that are able to type (with rank 2 intersection types) recursive definitions that are not simple. Typing rules for assigning intersection types to (nonsimple) recursive definitions have been already proposed in the literature. However, at the best of our knowledge, previous algorithms for typing recursive definitions in the presence of intersection types allow only simple recursive definitions to be typed. The rules and algorithms proposed in this paper are also able to type interesting examples of polymorphic recursion (i.e., recursive definitions rec {x=e} where different occurrences of x in e are used with different types). Moreover, the underlying techniques do not depend on particulars of rank 2 intersection, so they can be applied to other type systems.
Rank 2 Intersection for Recursive Definitions
DAMIANI, Ferruccio
2007-01-01
Abstract
Let |- be an intersection type system. We say that a term is |-simple (or just simple when the system |- is clear from the context) if system |- can prove that it has a simple type. In this paper we propose new typing rules and algorithms that are able to type (with rank 2 intersection types) recursive definitions that are not simple. Typing rules for assigning intersection types to (nonsimple) recursive definitions have been already proposed in the literature. However, at the best of our knowledge, previous algorithms for typing recursive definitions in the presence of intersection types allow only simple recursive definitions to be typed. The rules and algorithms proposed in this paper are also able to type interesting examples of polymorphic recursion (i.e., recursive definitions rec {x=e} where different occurrences of x in e are used with different types). Moreover, the underlying techniques do not depend on particulars of rank 2 intersection, so they can be applied to other type systems.File | Dimensione | Formato | |
---|---|---|---|
FI-2007.pdf
Accesso riservato
Tipo di file:
PDF EDITORIALE
Dimensione
287.11 kB
Formato
Adobe PDF
|
287.11 kB | Adobe PDF | Visualizza/Apri Richiedi una copia |
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.