Eliminating the problems of hidden-lambda insertion - Restricting implicit arguments for increased predictability of type checking in a functional programming language with depending types

Abstract

Agda is a dependently typed functional programming language developed with the aim of making programming with dependent types practical. One highly useful feature of Agda, implicit arguments, allows a user to omit arguments which can be inferred by their relation to other arguments. This thesis aims to document a set of problems with the way implicit arguments are currently handled by Agda’s type checker, and provide a way to resolve them. Three programs are presented as defining examples of the problems, along with derivations pinpointing the source of the problems within the checking process. We conclude that although the problems cannot be resolved by modifying the heuristic central to this problematic type checking process, it is sufficient to impose a simple limitation on where implicit arguments may be declared, bound and given. The limitation somewhat restricts how things can be expressed, but we show that general expressiveness is not negatively affected. A small dependently typed calculus called λΞΦ (Xiphi) is defined, and implemented in Haskell. The implementation supports the feasibility of the solution while also indicating shortcomings, which are discussed.