GADTs Meet Subtyping

DOI10.1007/978-3-642-37036-6_30MaRDI QIDQ5326307zbMATH OpenOpenAlexFDO

Authors Gabriel Scherer, Didier Rémy

Publication date 5 August 2013

Published in Programming Languages and Systems (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1301.2903

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Abstract data types; algebraic specification (68Q65)

Abstract: While generalized algebraic datatypes (GADTs) are now considered well-understood, adding them to a language with a notion of subtyping comes with a few surprises. What does it mean for a GADT parameter to be covariant? The answer turns out to be quite subtle. It involves fine-grained properties of the subtyping relation that raise interesting design questions. We allow variance annotations in GADT definitions, study their soundness, and present a sound and complete algorithm to check them. Our work may be applied to real-world ML-like languages with explicit subtyping such as OCaml, or to languages with general subtyping constraints.

Recommendations

• Automata, Languages and Programming
• Matching MyType to subtyping
• Principal type inference for GADTs
• Logic of subtyping
• scientific article; zbMATH DE number 1156716
• The relevance of semantic subtyping
• A new formalization of subtyping to match subclasses to subtypes

Cited in

(7)

• Dualizing generalized algebraic data types by matrix transposition
• Ambivalent types for principal type inference with GADTs
• Ghostbuster: a tool for simplifying and converting GADTs
• Safe zero-cost coercions for Haskell
• Characterizing functions mappable over GADTs
• A lean specification for gadts: System F with first-class equality proofs
• Transposing G to \(\text{C}^{\sharp}\): expressivity of generalized algebraic data types in an object-oriented language

Describes a project that uses

Uses Software

• OCaml

This page was built for publication: GADTs Meet Subtyping

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5326307)