Generic programming of all kinds

Alejandro Serrano; V. Cacciari Miraldo

doi:10.1145/3242744.3242745

Generic programming of all kinds

Alejandro Serrano
, V. Cacciari Miraldo

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

Abstract

Datatype-generic programming is a widely used technique to define functions that work regularly over a class of datatypes. Examples include deriving serialization of data, equality or even functoriality. The state-of-the-art of generic programming still lacks handling GADTs, multiple type variables, and some other features. This paper exploits modern GHC extensions, including <pre>TypeInType</pre>, to handle arbitrary number of type variables, constraints, and existentials. We also provide an Agda model of our construction that does not require Russel’s paradox, proving the construction is consistent.

Original language	English
Title of host publication	Proceedings of the 11th ACM SIGPLAN International Symposium on Haskell
Publisher	Association for Computing Machinery
Pages	41-54
Number of pages	14
ISBN (Electronic)	9781450349116
ISBN (Print)	978-1-4503-5835-4
DOIs	https://doi.org/10.1145/3242744.3242745
Publication status	Published - 17 Sept 2018

Keywords

Generic programming
Haskell

Access to Document

10.1145/3242744.3242745Licence: Unspecified

serranoFinal published version, 593 KBLicence: Taverne

Cite this

@inproceedings{59ac102f5aaf4d5f9435fc30fab353a9,

title = "Generic programming of all kinds",

abstract = "Datatype-generic programming is a widely used technique to define functions that work regularly over a class of datatypes. Examples include deriving serialization of data, equality or even functoriality. The state-of-the-art of generic programming still lacks handling GADTs, multiple type variables, and some other features. This paper exploits modern GHC extensions, including TypeInType, to handle arbitrary number of type variables, constraints, and existentials. We also provide an Agda model of our construction that does not require Russel{\textquoteright}s paradox, proving the construction is consistent.",

keywords = "Generic programming, Haskell",

author = "Alejandro Serrano and \{Cacciari Miraldo\}, V.",

year = "2018",

month = sep,

day = "17",

doi = "10.1145/3242744.3242745",

language = "English",

isbn = "978-1-4503-5835-4 ",

pages = "41--54",

booktitle = "Proceedings of the 11th ACM SIGPLAN International Symposium on Haskell",

publisher = "Association for Computing Machinery",

}

TY - GEN

T1 - Generic programming of all kinds

AU - Serrano, Alejandro

AU - Cacciari Miraldo, V.

PY - 2018/9/17

Y1 - 2018/9/17

N2 - Datatype-generic programming is a widely used technique to define functions that work regularly over a class of datatypes. Examples include deriving serialization of data, equality or even functoriality. The state-of-the-art of generic programming still lacks handling GADTs, multiple type variables, and some other features. This paper exploits modern GHC extensions, including TypeInType, to handle arbitrary number of type variables, constraints, and existentials. We also provide an Agda model of our construction that does not require Russel’s paradox, proving the construction is consistent.

AB - Datatype-generic programming is a widely used technique to define functions that work regularly over a class of datatypes. Examples include deriving serialization of data, equality or even functoriality. The state-of-the-art of generic programming still lacks handling GADTs, multiple type variables, and some other features. This paper exploits modern GHC extensions, including TypeInType, to handle arbitrary number of type variables, constraints, and existentials. We also provide an Agda model of our construction that does not require Russel’s paradox, proving the construction is consistent.

KW - Generic programming

KW - Haskell

UR - https://www.scopus.com/pages/publications/85056717819

U2 - 10.1145/3242744.3242745

DO - 10.1145/3242744.3242745

M3 - Conference contribution

AN - SCOPUS:85056717819

SN - 978-1-4503-5835-4

SP - 41

EP - 54

BT - Proceedings of the 11th ACM SIGPLAN International Symposium on Haskell

PB - Association for Computing Machinery

ER -

Generic programming of all kinds

Abstract

Keywords

Access to Document

Other files and links

Fingerprint

Cite this