Hybrid Intersection Types for PCF (Extended Version)

TL;DR

This paper introduces a novel intersection type system for PCF with a hybrid evaluation strategy, enabling CBN and CBV to coexist without encoding, and provides quantitative bounds on normalization sequences.

Contribution

It presents the first sound, complete, and quantitative intersection type system for a hybrid evaluation model in PCF, combining CBN and CBV behaviors.

Findings

Type system is sound and complete for PCFH evaluation.

Derivation size bounds the length of reduction sequences.

Refined type system gives exact normalization length.

Abstract

Intersection type systems have been independently applied to different evaluation strategies, such as call-by-name (CBN) and call-by-value (CBV). These type systems have been then generalized to different subsuming paradigms being able, in particular, to encode CBN and CBV in a unique unifying framework. However, there are no intersection type systems that explicitly enable CBN and CBV to cohabit together without making use of an encoding into a common target framework. This work proposes an intersection type system for PCF with a specific notion of evaluation, called PCFH. Evaluation in PCFH actually has a hybrid nature, in the sense that CBN and CBV operational behaviors cohabit together. Indeed, PCFH combines a CBV-like operational behavior for function application with a CBN-like behavior for recursion. This hybrid nature is reflected in the type system, which turns out to be sound and complete with respect to PCFH: not only typability implies normalization, but also the converse holds. Moreover, the type system is quantitative, in the sense that the size of typing derivations provides upper bounds for the length of the reduction sequences to normal form. This type system is then refined to a tight one, offering exact information regarding the length of normalization sequences. This is the first time that a sound and complete quantitative type system has been designed for a hybrid computational model.