Putting gradual types to work

TL;DR

This paper explores incorporating gradual types into a statically typed functional language, emphasizing dynamic checking to enhance flexibility and safety, with practical benefits demonstrated in an industrial context.

Contribution

It presents a novel approach to gradual typing that promotes dynamic checks in a statically typed language, addressing implementation challenges and practical applications.

Findings

Successfully integrated gradual types with Hindley-Milner inference

Identified challenges in applying gradual rules to recursive types

Demonstrated practical benefits in an industrial setting

Abstract

In this paper, we describe our experience incorporating gradual types in a statically typed functional language with Hindley-Milner style type inference. Where most gradually typed systems aim to improve static checking in a dynamically typed language, we approach it from the opposite perspective and promote dynamic checking in a statically typed language. Our approach provides a glimpse into how languages like SML and OCaml might handle gradual typing. We discuss our implementation and challenges faced -- specifically how gradual typing rules apply to our representation of composite and recursive types. We review the various implementations that add dynamic typing to a statically typed language in order to highlight the different ways of mixing static and dynamic typing and examine possible inspirations while maintaining the gradual nature of our type system. This paper also discusses our motivation for adding gradual types to our language, and the practical benefits of doing so in our industrial setting.