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...
Main Authors: | , , , |
---|---|
Format: | Conference Object |
Language: | unknown |
Published: |
2010
|
Subjects: | |
Online Access: | https://repository.upenn.edu/handle/20.500.14332/6698 https://hdl.handle.net/20.500.14332/6698 |
id |
ftunivpenn:oai:repository.upenn.edu:20.500.14332/6698 |
---|---|
record_format |
openpolar |
spelling |
ftunivpenn:oai:repository.upenn.edu:20.500.14332/6698 2024-02-04T10:00:02+01:00 Dependent types and Program Equivalence Jia, Limin Zhao, Jianzhou Sjoberg, Vilhelm Weirich, Stephanie 2010-01-17 application/pdf https://repository.upenn.edu/handle/20.500.14332/6698 https://hdl.handle.net/20.500.14332/6698 unknown https://repository.upenn.edu/handle/20.500.14332/6698 632 Departmental Papers (CIS) published Computer Sciences Presentation 2010 ftunivpenn https://doi.org/20.500.14332/6698 2024-01-06T23:24:33Z 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, Omega, 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 equi valence, we parameterize our type system with an abstract relation that is not n ecessarily decidable. We then design a novel set of typing rules that require on ly weak properties of this abstract relation in the proof of the preservation an d progress lemmas. This design provides flexibility: we compare valid instantiat ions of term equivalence which range from beta-equivalence, to contextual equiva lence, to some exotic equivalences. © ACM, 2010. This is the author's version of the work. It is posted here by permission of ACM for your personal use. Not for redistribution. The definitive version was published in 37th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages , {(2010)} ... Conference Object DML University of Pennsylvania: ScholaryCommons@Penn Haskell ENVELOPE(-64.279,-64.279,-66.749,-66.749) |
institution |
Open Polar |
collection |
University of Pennsylvania: ScholaryCommons@Penn |
op_collection_id |
ftunivpenn |
language |
unknown |
topic |
Computer Sciences |
spellingShingle |
Computer Sciences Jia, Limin Zhao, Jianzhou Sjoberg, Vilhelm Weirich, Stephanie Dependent types and Program Equivalence |
topic_facet |
Computer Sciences |
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, Omega, 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 equi valence, we parameterize our type system with an abstract relation that is not n ecessarily decidable. We then design a novel set of typing rules that require on ly weak properties of this abstract relation in the proof of the preservation an d progress lemmas. This design provides flexibility: we compare valid instantiat ions of term equivalence which range from beta-equivalence, to contextual equiva lence, to some exotic equivalences. © ACM, 2010. This is the author's version of the work. It is posted here by permission of ACM for your personal use. Not for redistribution. The definitive version was published in 37th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages , {(2010)} ... |
format |
Conference Object |
author |
Jia, Limin Zhao, Jianzhou Sjoberg, Vilhelm Weirich, Stephanie |
author_facet |
Jia, Limin Zhao, Jianzhou Sjoberg, 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 |
publishDate |
2010 |
url |
https://repository.upenn.edu/handle/20.500.14332/6698 https://hdl.handle.net/20.500.14332/6698 |
long_lat |
ENVELOPE(-64.279,-64.279,-66.749,-66.749) |
geographic |
Haskell |
geographic_facet |
Haskell |
genre |
DML |
genre_facet |
DML |
op_source |
632 Departmental Papers (CIS) published |
op_relation |
https://repository.upenn.edu/handle/20.500.14332/6698 |
op_doi |
https://doi.org/20.500.14332/6698 |
_version_ |
1789965127936638976 |