Sage: Unified Hybrid Checking for First-Class Types, General Refinement Types, and Dynamic (Extended Report)

Abstract

This paper presents Sage, a functional programming language with a rich type system that supports a broad range of typing paradigms, from dynamically-typed Scheme-like programming, to decidable ML-like types, to precise refinement types. This type system is a synthesis of three general concepts — first-class types, general refinement types, and the type Dynamic — that add expressive power in orthogonal and complementary ways. None of these concepts are statically decidable. The Sage compiler uniformly circumvents this limitation using hybrid type checking, which inserts occasional run-time casts in particularly complicated situations that cannot be statically checked. We describe a prototype implementation of Sage and preliminary experimental results showing that most or all types are enforced via static type checking — the number of compiler-inserted casts is very small or zero on all our benchmarks.