DRAFT—Do not distribute 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 |
Subjects: | |
Online Access: | http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.409.5359 http://www.andrew.cmu.edu/user/liminjia/research/papers/lambda-eek.pdf |
id |
ftciteseerx:oai:CiteSeerX.psu:10.1.1.409.5359 |
---|---|
record_format |
openpolar |
spelling |
ftciteseerx:oai:CiteSeerX.psu:10.1.1.409.5359 2023-05-15T16:02:06+02:00 DRAFT—Do not distribute Dependent Types and Program Equivalence Limin Jia Jianzhou Zhao Vilhelm Sjöberg Stephanie Weirich The Pennsylvania State University CiteSeerX Archives application/pdf http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.409.5359 http://www.andrew.cmu.edu/user/liminjia/research/papers/lambda-eek.pdf en eng http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.409.5359 http://www.andrew.cmu.edu/user/liminjia/research/papers/lambda-eek.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/lambda-eek.pdf text ftciteseerx 2016-01-08T03:13:14Z 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. [Copyright notice will appear here once ’preprint ’ option is removed.] 1. 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. [Copyright notice will appear here once ’preprint ’ option is removed.] 1. |
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 DRAFT—Do not distribute Dependent Types and Program Equivalence |
author_facet |
Limin Jia Jianzhou Zhao Vilhelm Sjöberg Stephanie Weirich |
author_sort |
Limin Jia |
title |
DRAFT—Do not distribute Dependent Types and Program Equivalence |
title_short |
DRAFT—Do not distribute Dependent Types and Program Equivalence |
title_full |
DRAFT—Do not distribute Dependent Types and Program Equivalence |
title_fullStr |
DRAFT—Do not distribute Dependent Types and Program Equivalence |
title_full_unstemmed |
DRAFT—Do not distribute Dependent Types and Program Equivalence |
title_sort |
draft—do not distribute dependent types and program equivalence |
url |
http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.409.5359 http://www.andrew.cmu.edu/user/liminjia/research/papers/lambda-eek.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/lambda-eek.pdf |
op_relation |
http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.409.5359 http://www.andrew.cmu.edu/user/liminjia/research/papers/lambda-eek.pdf |
op_rights |
Metadata may be used without restrictions as long as the oai identifier remains attached to it. |
_version_ |
1766397714201837568 |