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

Examensarbete för masterexamen

Please use this identifier to cite or link to this item: https://hdl.handle.net/20.500.12380/215291
Download file(s):
File Description SizeFormat 
215291.pdfFulltext1.16 MBAdobe PDFView/Open
Type: Examensarbete för masterexamen
Master Thesis
Title: Eliminating the problems of hidden-lambda insertion - Restricting implicit arguments for increased predictability of type checking in a functional programming language with depending types
Authors: Johansson, Marcus
Lloyd, Jesper
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.
Keywords: Data- och informationsvetenskap;Computer and Information Science
Issue Date: 2015
Publisher: Chalmers tekniska högskola / Institutionen för data- och informationsteknik (Chalmers)
Chalmers University of Technology / Department of Computer Science and Engineering (Chalmers)
URI: https://hdl.handle.net/20.500.12380/215291
Collection:Examensarbeten för masterexamen // Master Theses



Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.