First-Class Subtypes
First class type equalities, in the form of generalized algebraic data types (GADTs), are commonly found in functional programs. However, first-class representations of other relations between types, such as subtyping, are not yet directly supported in most functional programming languages. We pres...
| Main Authors: | , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Open Publishing Association
2019-05-01
|
| Series: | Electronic Proceedings in Theoretical Computer Science |
| Online Access: | http://arxiv.org/pdf/1905.06546v1 |
| _version_ | 1818033813084700672 |
|---|---|
| author | Jeremy Yallop Stephen Dolan |
| author_facet | Jeremy Yallop Stephen Dolan |
| author_sort | Jeremy Yallop |
| collection | DOAJ |
| description | First class type equalities, in the form of generalized algebraic data types (GADTs), are commonly found in functional programs. However, first-class representations of other relations between types, such as subtyping, are not yet directly supported in most functional programming languages.
We present several encodings of first-class subtypes using existing features of the OCaml language (made more convenient by the proposed modular implicits extension), show that any such encodings are interconvertible, and illustrate the utility of the encodings with several examples. |
| first_indexed | 2024-12-10T06:29:13Z |
| format | Article |
| id | doaj.art-8388c5ea1abb4de493ae96804dd0a4bc |
| institution | Directory Open Access Journal |
| issn | 2075-2180 |
| language | English |
| last_indexed | 2024-12-10T06:29:13Z |
| publishDate | 2019-05-01 |
| publisher | Open Publishing Association |
| record_format | Article |
| series | Electronic Proceedings in Theoretical Computer Science |
| spelling | doaj.art-8388c5ea1abb4de493ae96804dd0a4bc2022-12-22T01:59:07ZengOpen Publishing AssociationElectronic Proceedings in Theoretical Computer Science2075-21802019-05-01294Proc. ML 2017748510.4204/EPTCS.294.4:7First-Class SubtypesJeremy Yallop0Stephen Dolan1 University of Cambridge University of Cambridge First class type equalities, in the form of generalized algebraic data types (GADTs), are commonly found in functional programs. However, first-class representations of other relations between types, such as subtyping, are not yet directly supported in most functional programming languages. We present several encodings of first-class subtypes using existing features of the OCaml language (made more convenient by the proposed modular implicits extension), show that any such encodings are interconvertible, and illustrate the utility of the encodings with several examples.http://arxiv.org/pdf/1905.06546v1 |
| spellingShingle | Jeremy Yallop Stephen Dolan First-Class Subtypes Electronic Proceedings in Theoretical Computer Science |
| title | First-Class Subtypes |
| title_full | First-Class Subtypes |
| title_fullStr | First-Class Subtypes |
| title_full_unstemmed | First-Class Subtypes |
| title_short | First-Class Subtypes |
| title_sort | first class subtypes |
| url | http://arxiv.org/pdf/1905.06546v1 |
| work_keys_str_mv | AT jeremyyallop firstclasssubtypes AT stephendolan firstclasssubtypes |