CHAD for expressive total languages

Fernando Lucatelli Nunes; Matthijs Vákár

doi:10.1017/S096012952300018X

CHAD for expressive total languages

Fernando Lucatelli Nunes
, Matthijs Vákár

Sub Software Technology

Research output: Contribution to journal › Article › Academic › peer-review

Abstract

We show how to apply forward and reverse mode Combinatory Homomorphic Automatic Differentiation (CHAD) (Vákár (2021). ESOP, 607–634; Vákár and Smeding (2022). ACM Transactions on Programming Languages and Systems 44 (3) 20:1–20:49.) to total functional programming languages with expressive type systems featuring the combination of

• tuple types;

• sum types;

• inductive types;

• coinductive types;

• function types.

We achieve this by analyzing the categorical semantics of such types in Σ-types (Grothendieck constructions) of suitable categories. Using a novel categorical logical relations technique for such expressive type systems, we give a correctness proof of CHAD in this setting by showing that it computes the usual mathematical derivative of the function that the original program implements. The result is a principled, purely functional and provably correct method for performing forward- and reverse-mode automatic differentiation (AD) on total functional programming languages with expressive type systems.

Original language	English
Article number	PII S096012952300018X
Pages (from-to)	311–426
Number of pages	116
Journal	Mathematical Structures in Computer Science
Volume	33
Issue number	4-5
DOIs	https://doi.org/10.1017/S096012952300018X
Publication status	Published - Apr 2023

Bibliographical note

Funding Information:
This project has received funding from the European Union’s Horizon 2020 research and innovation program under the Marie Skłodowska-Curie grant agreement No. 895827 and from the Nederlandse Organisatie voor Wetenschappelijk Onderzoek under NWO Veni grant number VI.Veni.202.124. This research was also supported through the program “Oberwolfach Leibniz Fellows” by the Mathematisches Forschungsinstitut Oberwolfach in 2022 and partially supported by the CMUC, Centre for Mathematics of the University of Coimbra – UIDB/00324/2020, funded by the Portuguese Government through FCT/MCTES.

Publisher Copyright:
© The Author(s), 2023. Published by Cambridge University Press.

Keywords

(Co)monadicity
Artin gluing
Automatic differentiation
Cartesian closed categories
Coalgebras
Coinductive types
Comma categories
Creation of initial algebras
Denotational semantics
Dependently typed languages
Exponentiability
Extensive categories
Extensive indexed categories
Fibered categories
Free cocompletion under coproducts
Grothendieck construction
Inductive types
Initial algebra semantics
Linear types
Logical relations
Polynomial functors
Program transformations
Programming languages
Scientific computing
Software correctness
Type systems
Variant types

Access to Document

10.1017/S096012952300018XLicence: CC BY

chad-for-expressive-total-languagesFinal published version, 1.99 MBLicence: CC BY

Cite this

@article{7a7cf3af9fd04b1199184e605cf5991d,

title = "CHAD for expressive total languages",

abstract = "We show how to apply forward and reverse mode Combinatory Homomorphic Automatic Differentiation (CHAD) (V{\'a}k{\'a}r (2021). ESOP, 607–634; V{\'a}k{\'a}r and Smeding (2022). ACM Transactions on Programming Languages and Systems 44 (3) 20:1–20:49.) to total functional programming languages with expressive type systems featuring the combination of • tuple types; • sum types; • inductive types; • coinductive types; • function types. We achieve this by analyzing the categorical semantics of such types in Σ-types (Grothendieck constructions) of suitable categories. Using a novel categorical logical relations technique for such expressive type systems, we give a correctness proof of CHAD in this setting by showing that it computes the usual mathematical derivative of the function that the original program implements. The result is a principled, purely functional and provably correct method for performing forward- and reverse-mode automatic differentiation (AD) on total functional programming languages with expressive type systems.",

keywords = "(Co)monadicity, Artin gluing, Automatic differentiation, Cartesian closed categories, Coalgebras, Coinductive types, Comma categories, Creation of initial algebras, Denotational semantics, Dependently typed languages, Exponentiability, Extensive categories, Extensive indexed categories, Fibered categories, Free cocompletion under coproducts, Grothendieck construction, Inductive types, Initial algebra semantics, Linear types, Logical relations, Polynomial functors, Program transformations, Programming languages, Scientific computing, Software correctness, Type systems, Variant types",

author = "Nunes, \{Fernando Lucatelli\} and Matthijs V{\'a}k{\'a}r",

note = "Funding Information: This project has received funding from the European Union{\textquoteright}s Horizon 2020 research and innovation program under the Marie Sk{\l}odowska-Curie grant agreement No. 895827 and from the Nederlandse Organisatie voor Wetenschappelijk Onderzoek under NWO Veni grant number VI.Veni.202.124. This research was also supported through the program “Oberwolfach Leibniz Fellows” by the Mathematisches Forschungsinstitut Oberwolfach in 2022 and partially supported by the CMUC, Centre for Mathematics of the University of Coimbra – UIDB/00324/2020, funded by the Portuguese Government through FCT/MCTES. Publisher Copyright: {\textcopyright} The Author(s), 2023. Published by Cambridge University Press.",

year = "2023",

month = apr,

doi = "10.1017/S096012952300018X",

language = "English",

volume = "33",

pages = "311–426",

journal = "Mathematical Structures in Computer Science",

issn = "0960-1295",

publisher = "Cambridge University Press",

number = "4-5",

}

TY - JOUR

T1 - CHAD for expressive total languages

AU - Nunes, Fernando Lucatelli

AU - Vákár, Matthijs

N1 - Funding Information: This project has received funding from the European Union’s Horizon 2020 research and innovation program under the Marie Skłodowska-Curie grant agreement No. 895827 and from the Nederlandse Organisatie voor Wetenschappelijk Onderzoek under NWO Veni grant number VI.Veni.202.124. This research was also supported through the program “Oberwolfach Leibniz Fellows” by the Mathematisches Forschungsinstitut Oberwolfach in 2022 and partially supported by the CMUC, Centre for Mathematics of the University of Coimbra – UIDB/00324/2020, funded by the Portuguese Government through FCT/MCTES. Publisher Copyright: © The Author(s), 2023. Published by Cambridge University Press.

PY - 2023/4

Y1 - 2023/4

N2 - We show how to apply forward and reverse mode Combinatory Homomorphic Automatic Differentiation (CHAD) (Vákár (2021). ESOP, 607–634; Vákár and Smeding (2022). ACM Transactions on Programming Languages and Systems 44 (3) 20:1–20:49.) to total functional programming languages with expressive type systems featuring the combination of • tuple types; • sum types; • inductive types; • coinductive types; • function types. We achieve this by analyzing the categorical semantics of such types in Σ-types (Grothendieck constructions) of suitable categories. Using a novel categorical logical relations technique for such expressive type systems, we give a correctness proof of CHAD in this setting by showing that it computes the usual mathematical derivative of the function that the original program implements. The result is a principled, purely functional and provably correct method for performing forward- and reverse-mode automatic differentiation (AD) on total functional programming languages with expressive type systems.

AB - We show how to apply forward and reverse mode Combinatory Homomorphic Automatic Differentiation (CHAD) (Vákár (2021). ESOP, 607–634; Vákár and Smeding (2022). ACM Transactions on Programming Languages and Systems 44 (3) 20:1–20:49.) to total functional programming languages with expressive type systems featuring the combination of • tuple types; • sum types; • inductive types; • coinductive types; • function types. We achieve this by analyzing the categorical semantics of such types in Σ-types (Grothendieck constructions) of suitable categories. Using a novel categorical logical relations technique for such expressive type systems, we give a correctness proof of CHAD in this setting by showing that it computes the usual mathematical derivative of the function that the original program implements. The result is a principled, purely functional and provably correct method for performing forward- and reverse-mode automatic differentiation (AD) on total functional programming languages with expressive type systems.

KW - (Co)monadicity

KW - Artin gluing

KW - Automatic differentiation

KW - Cartesian closed categories

KW - Coalgebras

KW - Coinductive types

KW - Comma categories

KW - Creation of initial algebras

KW - Denotational semantics

KW - Dependently typed languages

KW - Exponentiability

KW - Extensive categories

KW - Extensive indexed categories

KW - Fibered categories

KW - Free cocompletion under coproducts

KW - Grothendieck construction

KW - Inductive types

KW - Initial algebra semantics

KW - Linear types

KW - Logical relations

KW - Polynomial functors

KW - Program transformations

KW - Programming languages

KW - Scientific computing

KW - Software correctness

KW - Type systems

KW - Variant types

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

U2 - 10.1017/S096012952300018X

DO - 10.1017/S096012952300018X

M3 - Article

SN - 0960-1295

VL - 33

SP - 311

EP - 426

JO - Mathematical Structures in Computer Science

JF - Mathematical Structures in Computer Science

IS - 4-5

M1 - PII S096012952300018X

ER -

CHAD for expressive total languages

Abstract

Bibliographical note

Keywords

Access to Document

Other files and links

Fingerprint

Cite this