Semantics and Type Checking of Dependently−Typed Lazy Functional Programs

Abstract

We present a denotational semantics, type checking algorithm and soundness result for a language with dependent function and record types, dependent case expressions, a fixpoint combinator and a type of all types. The design of our algorithm is guided by key ideas from related work on the semantics of dependent types in domain theory, normalisation of typed lambda terms with sums, and subtyping of recursive types. We address a subtlety that arises with respect to the soundness of checking case expressions if the underlying language is based on a non-strict evaluation order. Subtyping of recursive types is extended to take into account functions occurring in types. The expressiveness of our language comes at the cost of undecidable type checking; we discuss the limitations of our algorithm, which arise mainly from the interaction of case expressions and fixpoints