| Aiding Dependent Type Checking with Rewrite Rules (2007) | |||||||||||||||
Abstract | |||||||||||||||
| Dependent type checking in Cayenne often fails when the programmer has relied on non-trivial properties of functions that are used in types. For instance, associativity of addition on natural numbers does not follow immediately from the function denition, but it may be required during the type checking process. We propose to tackle this problem by allowing the programmer to annotate programs with rewrite rules whenever such additional properties are required. We discuss two motivating examples and report on a feasibility study where we integrated a rewriting system into a type checking algorithm for a language with dependent types and general recursion. 1 Motivating examples All our examples involve lists of a given length, called vectors. The function Vec takes the type of elements and the length of the vector and returns a type. An empty vector is represented by a type with the single constructor nil, and a non-empty vector of length n+1 is a pair consisting of the type of elements and a vector of length n. Borrowing notation from Cayenne [2], we could write | |||||||||||||||
Publication details | |||||||||||||||
| |||||||||||||||