Dependent types and program equivalence
The definition of type equivalence is one of the most important design issues for any typed language. In dependently typed languages, because terms appear in types, this definition must rely on a definition of term equivalence. In that case, decidability of type checking requires decidability for th...
Published in: | ACM SIGPLAN Notices |
---|---|
Main Authors: | , , , |
Format: | Article in Journal/Newspaper |
Language: | English |
Published: |
Association for Computing Machinery (ACM)
2010
|
Subjects: | |
Online Access: | http://dx.doi.org/10.1145/1707801.1706333 https://dl.acm.org/doi/pdf/10.1145/1707801.1706333 |
id |
cracm:10.1145/1707801.1706333 |
---|---|
record_format |
openpolar |
spelling |
cracm:10.1145/1707801.1706333 2024-06-02T08:05:49+00:00 Dependent types and program equivalence Jia, Limin Zhao, Jianzhou Sjöberg, Vilhelm Weirich, Stephanie 2010 http://dx.doi.org/10.1145/1707801.1706333 https://dl.acm.org/doi/pdf/10.1145/1707801.1706333 en eng Association for Computing Machinery (ACM) ACM SIGPLAN Notices volume 45, issue 1, page 275-286 ISSN 0362-1340 1558-1160 journal-article 2010 cracm https://doi.org/10.1145/1707801.1706333 2024-05-07T12:57:11Z The definition of type equivalence is one of the most important design issues for any typed language. In dependently typed languages, because terms appear in types, this definition must rely on a definition of term equivalence. In that case, decidability of type checking requires decidability for the term equivalence relation. Almost all dependently-typed languages require this relation to be decidable. Some, such as Coq, Epigram or Agda, do so by employing analyses to force all programs to terminate. Conversely, others, such as DML, ATS, Ωmega, or Haskell, allow nonterminating computation, but do not allow those terms to appear in types. Instead, they identify a terminating index language and use singleton types to connect indices to computation. In both cases, decidable type checking comes at a cost, in terms of complexity and expressiveness. Conversely, the benefits to be gained by decidable type checking are modest. Termination analyses allow dependently typed programs to verify total correctness properties. However, decidable type checking is not a prerequisite for type safety. Furthermore, decidability does not imply tractability. A decidable approximation of program equivalence may not be useful in practice. Therefore, we take a different approach: instead of a fixed notion for term equivalence, we parameterize our type system with an abstract relation that is not necessarily decidable. We then design a novel set of typing rules that require only weak properties of this abstract relation in the proof of the preservation and progress lemmas. This design provides flexibility: we compare valid instantiations of term equivalence which range from beta-equivalence, to contextual equivalence, to some exotic equivalences. Article in Journal/Newspaper DML ACM Publications (Association for Computing Machinery) Haskell ENVELOPE(-64.279,-64.279,-66.749,-66.749) ACM SIGPLAN Notices 45 1 275 286 |
institution |
Open Polar |
collection |
ACM Publications (Association for Computing Machinery) |
op_collection_id |
cracm |
language |
English |
description |
The definition of type equivalence is one of the most important design issues for any typed language. In dependently typed languages, because terms appear in types, this definition must rely on a definition of term equivalence. In that case, decidability of type checking requires decidability for the term equivalence relation. Almost all dependently-typed languages require this relation to be decidable. Some, such as Coq, Epigram or Agda, do so by employing analyses to force all programs to terminate. Conversely, others, such as DML, ATS, Ωmega, or Haskell, allow nonterminating computation, but do not allow those terms to appear in types. Instead, they identify a terminating index language and use singleton types to connect indices to computation. In both cases, decidable type checking comes at a cost, in terms of complexity and expressiveness. Conversely, the benefits to be gained by decidable type checking are modest. Termination analyses allow dependently typed programs to verify total correctness properties. However, decidable type checking is not a prerequisite for type safety. Furthermore, decidability does not imply tractability. A decidable approximation of program equivalence may not be useful in practice. Therefore, we take a different approach: instead of a fixed notion for term equivalence, we parameterize our type system with an abstract relation that is not necessarily decidable. We then design a novel set of typing rules that require only weak properties of this abstract relation in the proof of the preservation and progress lemmas. This design provides flexibility: we compare valid instantiations of term equivalence which range from beta-equivalence, to contextual equivalence, to some exotic equivalences. |
format |
Article in Journal/Newspaper |
author |
Jia, Limin Zhao, Jianzhou Sjöberg, Vilhelm Weirich, Stephanie |
spellingShingle |
Jia, Limin Zhao, Jianzhou Sjöberg, Vilhelm Weirich, Stephanie Dependent types and program equivalence |
author_facet |
Jia, Limin Zhao, Jianzhou Sjöberg, Vilhelm Weirich, Stephanie |
author_sort |
Jia, Limin |
title |
Dependent types and program equivalence |
title_short |
Dependent types and program equivalence |
title_full |
Dependent types and program equivalence |
title_fullStr |
Dependent types and program equivalence |
title_full_unstemmed |
Dependent types and program equivalence |
title_sort |
dependent types and program equivalence |
publisher |
Association for Computing Machinery (ACM) |
publishDate |
2010 |
url |
http://dx.doi.org/10.1145/1707801.1706333 https://dl.acm.org/doi/pdf/10.1145/1707801.1706333 |
long_lat |
ENVELOPE(-64.279,-64.279,-66.749,-66.749) |
geographic |
Haskell |
geographic_facet |
Haskell |
genre |
DML |
genre_facet |
DML |
op_source |
ACM SIGPLAN Notices volume 45, issue 1, page 275-286 ISSN 0362-1340 1558-1160 |
op_doi |
https://doi.org/10.1145/1707801.1706333 |
container_title |
ACM SIGPLAN Notices |
container_volume |
45 |
container_issue |
1 |
container_start_page |
275 |
op_container_end_page |
286 |
_version_ |
1800750699231838208 |