Conversion by Evaluation

Abstract. We show how testing convertibility of two types in dependently typed systems can advantageously be implemented instead untyped normalization by evaluation, thereby reusing existing compilers and runtime environments for stock functional languages, without peeking under the hood, for a fast yet cheap system in terms of implementation effort. Our focus is on performance of untyped normalization by evaluation. We demonstrate that with the aid of a standard optimization for higher order programs (namely uncurrying), the reuse of native datatypes and pattern matching facilities of the underlying evaluator, we may obtain a normalizer with little to no performance overhead compared to a regular evaluator.

• Type: Conference
• Year: 2010
• Where: PADL
• Authors: Mathieu Boespflug
• Keywords: PADL 2010, Pattern Matching Facilities, Programming Languages, Regular Evaluator, Untyped Normalization