Zero-Cost Constructor Subtyping

Andrew Marmaduke; Christopher Jenkins; Aaron Stump

doi:10.1145/3462172.3462194

Back

Conference proceeding

Open access

Zero-Cost Constructor Subtyping

Andrew Marmaduke, Christopher Jenkins and Aaron Stump

IFL '20: Proceedings of the 32nd Symposium on Implementation and Application of Functional Languages, pp.93-103

IFL 2020: 32nd Symposium on Implementation and Application of Functional Languages (Canterbury, United Kingdom, 09/02/2020–09/04/2020)

07/23/2021

DOI: 10.1145/3462172.3462194

Appears in UI Libraries Support Open Access

Files and links (1)

url

https://doi.org/10.1145/3462172.3462194View

Published (Version of record) Open Access

Abstract

Constructor subtyping is a form of subtyping where two inductive types can be related as long as the inductive signature of one is a subsignature of the other. To be a subsignature requires every constructor of the smaller datatype be present in the larger datatype (modulo subtyping of the constructors’ types). In this paper, we describe a method for impredicatively encoding datatype signatures in Cedille (a dependently typed programming language) that supports highly flexible constructor subtyping, with the subtyping relation given by a derived notion of type inclusion witnessed by a heterogeneously typed identity function. Specifically, the conditions under which constructor subtyping is possible between datatypes are fully independent of the order in which constructors are listed in their declarations. After examining some extended case studies, we formulate generically a sufficient condition for constructor subtyping in Cedille using our technique.

generic programming

impredicative encodings

constructor subtyping

Cedille

UIOWA OA Agreement

Details

Title: Subtitle: Zero-Cost Constructor Subtyping
Creators: Andrew Marmaduke - University of Iowa
Christopher Jenkins - University of Iowa
Aaron Stump - University of Iowa, Computer Science
Resource Type: Conference proceeding
Publication Details: IFL '20: Proceedings of the 32nd Symposium on Implementation and Application of Functional Languages, pp.93-103
Conference: IFL 2020: 32nd Symposium on Implementation and Application of Functional Languages (Canterbury, United Kingdom, 09/02/2020–09/04/2020)
DOI: 10.1145/3462172.3462194
Publisher: Association for Computing Machinery (ACM)
Grant note: DOI: 10.13039/100000181, name: Air Force Office of Scientific Research, award: FA9550-16-1-0082
Language: English
Date published: 07/23/2021
Academic Unit: Computer Science
Record Identifier: 9984473238102771

Metrics

9 Record Views