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 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 tot...

• Type: Conference
• Year: 2010
• Where: POPL
• Authors: Jianzhou Zhao, Limin Jia, Stephanie Weirich, Vilhelm Sjöberg
• Keywords: Decidable Type Checking, POPL 2010, Programming Languages, Term Equivalence Relation, Type Equivalence