Efficient Functional Programming using Linear Types: The Array Fragment
Ladda ner
Typ
Examensarbete för masterexamen
Master Thesis
Master Thesis
Program
Computer science – algorithms, languages and logic (MPALG), MSc
Publicerad
2015
Författare
Juan, Víctor López
Modellbyggare
Tidskriftstitel
ISSN
Volymtitel
Utgivare
Sammanfattning
Functional languages excel at describing complex programs by composition of small building blocks. Yet, it can be difficult to predict the performance properties of such compositions. Namely, whether parts of the computation are shared or duplicated is typically left to the compiler to decide heuristically. Linear types serve as a tool to specify the desired behaviour (sharing or duplication). This means that the programmer is able to predict the performance of composition solely from the types of the composed functions. Girard’s linear logic (LL) can be extended with vector types and a synchronization primitive, making a linear language with array manipulation capabilities. In this master thesis, we improve on the n-ary extension of LL by introducing a self-dual, sequential array operator with an aggregation function. We provide a functional interpretation of the resulting calculus, which forms the basis for a low-level code generator. We then illustrate the effectiveness of the extended language by writing a number of examples in compositional style, and show that they predictably compile to efficient code. Examples include kernels of classical algorithms (1-dimensional stencil, QuickHull).
Beskrivning
Ämne/nyckelord
Informations- och kommunikationsteknik , Data- och informationsvetenskap , Information & Communication Technology , Computer and Information Science