Dependent Types and Program Equivalence
The definition of type equivalence is one of the most important design issues for any typed language. In dependentlytyped 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...
Main Authors: | , , , |
---|---|
Other Authors: | |
Format: | Text |
Language: | English |
Published: |
2009
|
Subjects: | |
Online Access: | http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.163.6638 http://www.andrew.cmu.edu/user/liminjia/research/papers/lambdaEq.pdf |
id |
ftciteseerx:oai:CiteSeerX.psu:10.1.1.163.6638 |
---|---|
record_format |
openpolar |
spelling |
ftciteseerx:oai:CiteSeerX.psu:10.1.1.163.6638 2023-05-15T16:02:04+02:00 Dependent Types and Program Equivalence Limin Jia Jianzhou Zhao Vilhelm Sjöberg Stephanie Weirich The Pennsylvania State University CiteSeerX Archives 2009 application/pdf http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.163.6638 http://www.andrew.cmu.edu/user/liminjia/research/papers/lambdaEq.pdf en eng http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.163.6638 http://www.andrew.cmu.edu/user/liminjia/research/papers/lambdaEq.pdf Metadata may be used without restrictions as long as the oai identifier remains attached to it. http://www.andrew.cmu.edu/user/liminjia/research/papers/lambdaEq.pdf text 2009 ftciteseerx 2016-01-07T15:47:49Z The definition of type equivalence is one of the most important design issues for any typed language. In dependentlytyped 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—and, in this context, type safety implies partial correctness. 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. Text DML Unknown Haskell ENVELOPE(-64.279,-64.279,-66.749,-66.749) |
institution |
Open Polar |
collection |
Unknown |
op_collection_id |
ftciteseerx |
language |
English |
description |
The definition of type equivalence is one of the most important design issues for any typed language. In dependentlytyped 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—and, in this context, type safety implies partial correctness. 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. |
author2 |
The Pennsylvania State University CiteSeerX Archives |
format |
Text |
author |
Limin Jia Jianzhou Zhao Vilhelm Sjöberg Stephanie Weirich |
spellingShingle |
Limin Jia Jianzhou Zhao Vilhelm Sjöberg Stephanie Weirich Dependent Types and Program Equivalence |
author_facet |
Limin Jia Jianzhou Zhao Vilhelm Sjöberg Stephanie Weirich |
author_sort |
Limin Jia |
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 |
2009 |
url |
http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.163.6638 http://www.andrew.cmu.edu/user/liminjia/research/papers/lambdaEq.pdf |
long_lat |
ENVELOPE(-64.279,-64.279,-66.749,-66.749) |
geographic |
Haskell |
geographic_facet |
Haskell |
genre |
DML |
genre_facet |
DML |
op_source |
http://www.andrew.cmu.edu/user/liminjia/research/papers/lambdaEq.pdf |
op_relation |
http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.163.6638 http://www.andrew.cmu.edu/user/liminjia/research/papers/lambdaEq.pdf |
op_rights |
Metadata may be used without restrictions as long as the oai identifier remains attached to it. |
_version_ |
1766397688574640128 |