A Haskell Implementation for a Dependent Type Theory with Definitions

Abstract

We present in this paper a simple dependently typed language. This language could be viewed as a pure -calculus extended with dependent types and definitions. The focus of this project is on the study of a definition mechanism where the definitions of constants could be handled efficiently during the type checking process. We later enrich the language with a module system to study how the definition mechanism should be adjusted for the introduction of the concept namespace on variables. The outcome of our work is a REPL(read-evaluate-print-loop) program through which a source file of our language could be loaded and type checked. The program also provides auxiliary functions for users to experiment with and observe the effect of the definition mechanism. The syntax of our language is specified by the BNF converter and the program is implemented in Haskell. We hold the expectation that our work could contribute to the development of proof assistant systems based on the dependent type theory.