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

Typ
Examensarbete för masterexamen
Master Thesis
Program
Computer science – algorithms, languages and logic (MPALG), MSc
Publicerad
2015
Författare
Johansson, Marcus
Lloyd, Jesper
Modellbyggare
Tidskriftstitel
ISSN
Volymtitel
Utgivare
Sammanfattning
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.
Beskrivning
Ämne/nyckelord
Data- och informationsvetenskap , Computer and Information Science
Citation
Arkitekt (konstruktör)
Geografisk plats
Byggnad (typ)
Byggår
Modelltyp
Skala
Teknik / material
Index