Code Extraction from a Dependently Typed Language to a Stack Based Language

Title

Code Extraction from a Dependently Typed Language to a Stack Based Language

 Author

Milliken, Louis (TU Delft Electrical Engineering, Mathematics and Computer Science; TU Delft Programming Languages)

Contributor

Cockx, J.G.H. (mentor)
Escot, L.F.B. (mentor)
Spaan, M.T.J. (graduation committee)

Degree granting institution

Delft University of Technology

 Programme

Computer Science and Engineering

 Project

CSE3000 Research Project

 Date

2022-06-27

 Abstract

Dependently typed languages such as Agda can provide users certain guarantees about the correct- ness of the code that they write, however, this comes at the cost of excess code that is not used at run time. Agda code is currently compiled to another language before it is run, there are not many target languages in popular use, so it is unclear if there are other potential target languages that could do a better job. The purpose of this paper is to investigate the efficacy of Forth as a target language for Extraction from Agda, in the hopes that Forth may prove to have the potential to be a better target language than the currently used target languages, Haskell and Javascript. Forth is a stack-based, imperative language, meaning that values are pushed and popped from a stack through the use of ’words’ instead of passing and returning values with functions, as is the case in most languages. Agda is a dependently typed, purely functional language. A dependent type is a type whose definition depends on another value, which allows for types with very specific information, such as a ’Vec n’ representing an array of length ’n’. These dependent types are used to write code with more certainty about its correctness and behaviour. Overall, Forth can be used as a target language to compile Agda code, however many of the advantages of Forth are squandered by executing code written and structured with Agda in mind, making it a rather ineffective target language when compared to other solutions such as Haskell.

 Subject

Agda
Forth
Dependent Types
code Extraction

 To reference this document use:

http://resolver.tudelft.nl/uuid:abc0814c-357f-48d1-b839-890251923952

 Part of collection

Student theses

 Document type

bachelor thesis

 Rights

© 2022 Louis Milliken
Files
PDF Code_Extraction_from_a_De ... nguage.pdf 592.26 KB
Close viewer