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: | Text |
Language: | unknown |
Published: |
ScholarlyCommons
2010
|
Subjects: | |
Online Access: | https://repository.upenn.edu/cis_papers/632 https://repository.upenn.edu/cgi/viewcontent.cgi?article=1668&context=cis_papers |
id |
ftunivpenn:oai:repository.upenn.edu:cis_papers-1668 |
---|---|
record_format |
openpolar |
spelling |
ftunivpenn:oai:repository.upenn.edu:cis_papers-1668 2023-05-15T16:02:04+02:00 Dependent types and Program Equivalence Jia, Limin Zhao, Jianzhou Sjoberg, Vilhelm Weirich, Stephanie 2010-01-17T08:00:00Z application/pdf https://repository.upenn.edu/cis_papers/632 https://repository.upenn.edu/cgi/viewcontent.cgi?article=1668&context=cis_papers unknown ScholarlyCommons https://repository.upenn.edu/cis_papers/632 https://repository.upenn.edu/cgi/viewcontent.cgi?article=1668&context=cis_papers Departmental Papers (CIS) Computer Sciences text 2010 ftunivpenn 2021-01-05T06:54:23Z 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. Text 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. |
format |
Text |
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 |
publisher |
ScholarlyCommons |
publishDate |
2010 |
url |
https://repository.upenn.edu/cis_papers/632 https://repository.upenn.edu/cgi/viewcontent.cgi?article=1668&context=cis_papers |
long_lat |
ENVELOPE(-64.279,-64.279,-66.749,-66.749) |
geographic |
Haskell |
geographic_facet |
Haskell |
genre |
DML |
genre_facet |
DML |
op_source |
Departmental Papers (CIS) |
op_relation |
https://repository.upenn.edu/cis_papers/632 https://repository.upenn.edu/cgi/viewcontent.cgi?article=1668&context=cis_papers |
_version_ |
1766397687993729024 |