Ambivalent Types for Principal Type Inference with GADTs (extended version)

Abstract : GADTs, short for Generalized Algebraic DataTypes, which allow constructors of algebraic datatypes to be non-surjective, have many useful applications. However, pattern matching on GADTsintroduces local type equality assumptions, which are a source of ambiguities that may destroy principal types---and must be resolved by type annotations. We introduce ambivalent types to tighten the definition of ambiguities and better confine them, so that type inference has principal types, remains monotonic, and requires fewer type annotations.
Document type :
Preprints, Working Papers, ...
Complete list of metadatas

Cited literature [17 references]  Display  Hide  Download

https://hal.inria.fr/hal-00914493
Contributor : Didier Rémy <>
Submitted on : Tuesday, December 10, 2013 - 10:02:41 PM
Last modification on : Friday, May 25, 2018 - 12:02:07 PM
Long-term archiving on : Saturday, April 8, 2017 - 5:43:04 AM

File

Garrigue-Remy_gadts_long2013.p...
Files produced by the author(s)

Identifiers

  • HAL Id : hal-00914493, version 2

Collections

Citation

Jacques Garrigue, Didier Rémy. Ambivalent Types for Principal Type Inference with GADTs (extended version). 2013. ⟨hal-00914493v2⟩

Share

Metrics

Record views

174

Files downloads

154