Semantic subtyping for non-strict languages

TL;DR

This paper extends semantic subtyping to non-strict, call-by-need functional languages by explicitly representing divergence in types, enabling sound subtyping relations in non-strict semantics.

Contribution

It introduces a novel type system that incorporates divergence explicitly, adapting semantic subtyping to non-strict languages for the first time.

Findings

Successfully defined a type system for non-strict languages

Demonstrated soundness of subtyping with divergence representation

Applicable to call-by-need functional languages

Abstract

Semantic subtyping is an approach to define subtyping relations for type systems featuring union and intersection type connectives. It has been studied only for strict languages, and it is unsound for non-strict semantics. In this work, we study how to adapt this approach to non-strict languages: in particular, we define a type system using semantic subtyping for a functional language with a call-by-need semantics. We do so by introducing an explicit representation for divergence in the types, so that the type system distinguishes expressions that are results from those which are computations that might diverge.