Extended Abstract: Towards a Performance Comparison of Syntax and Type-Directed NbE
Fuente:
arXiv
Salvato in:
| Autori principali: | , |
|---|---|
| Natura: | Preprint |
| Pubblicazione: |
2025
|
| Soggetti: | |
| Accesso online: | |
| Tags: |
Aggiungi Tag
Nessun Tag, puoi essere il primo ad aggiungerne!!
|
| _version_ | 1866909791860817920 |
|---|---|
| author | Gould, Chester J. F. Bowman, William J. |
| author_facet | Gould, Chester J. F. Bowman, William J. |
| contents | A key part of any dependent type-checker is the method for checking whether two types are equal. A common claim is that syntax-directed equality is more performant, although type-directed equality is more expressive. However, this claim is difficult to make precise, since implementations choose only one or the other approach, making a direct comparison impossible. We present some work-in-progress developing a realistic platform for direct, apples-to-apples, comparison of the two approaches, quantifying how much slower type-directed equality checking is, and analyzing why and how it can be improved. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2509_13489 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Extended Abstract: Towards a Performance Comparison of Syntax and Type-Directed NbE Gould, Chester J. F. Bowman, William J. Programming Languages A key part of any dependent type-checker is the method for checking whether two types are equal. A common claim is that syntax-directed equality is more performant, although type-directed equality is more expressive. However, this claim is difficult to make precise, since implementations choose only one or the other approach, making a direct comparison impossible. We present some work-in-progress developing a realistic platform for direct, apples-to-apples, comparison of the two approaches, quantifying how much slower type-directed equality checking is, and analyzing why and how it can be improved. |
| title | Extended Abstract: Towards a Performance Comparison of Syntax and Type-Directed NbE |
| topic | Programming Languages |
| url | https://arxiv.org/abs/2509.13489 |