A functional specification of effects
This dissertation is about effects and type theory. Functional programming languages such as Haskell illustrate how to encapsulate side effects using monads. Haskell compilers provide a handful of primitive effectful functions. Programmers can construct larger computations using the monadic return...
| Main Author: | |
|---|---|
| Format: | Thesis (University of Nottingham only) |
| Language: | English |
| Published: |
2009
|
| Subjects: | |
| Online Access: | https://eprints.nottingham.ac.uk/10779/ |
| _version_ | 1848791127576018944 |
|---|---|
| author | Swierstra, Wouter |
| author_facet | Swierstra, Wouter |
| author_sort | Swierstra, Wouter |
| building | Nottingham Research Data Repository |
| collection | Online Access |
| description | This dissertation is about effects and type theory.
Functional programming languages such as Haskell illustrate how to encapsulate side effects using monads. Haskell compilers provide a handful of primitive effectful functions. Programmers can construct larger computations using the monadic return and bind operations.
These primitive effectful functions, however, have no associated definition. At best, their semantics are specified separately on paper. This can make it difficult to test, debug, verify, or even predict the behaviour of effectful computations.
This dissertation provides pure, functional specifications in Haskell of several different effects. Using these specifications, programmers can test and debug effectful programs. This is particularly useful in tandem with automatic testing tools such as QuickCheck.
The specifications in Haskell are not total. This makes them unsuitable for the formal verification of effectful functions. This dissertation overcomes this limitation, by presenting total functional specifications in Agda, a programming language with dependent types.
There have been alternative approaches to incorporating effects in a dependently typed programming language. Most notably, recent work on Hoare Type Theory proposes to extend type theory with axioms that postulate the existence of primitive effectful functions. This dissertation shows how the functional specifications implement these axioms, unifying the two approaches.
The results presented in this dissertation may be used to write and verify effectful programs in the framework of type theory. |
| first_indexed | 2025-11-14T18:23:34Z |
| format | Thesis (University of Nottingham only) |
| id | nottingham-10779 |
| institution | University of Nottingham Malaysia Campus |
| institution_category | Local University |
| language | English |
| last_indexed | 2025-11-14T18:23:34Z |
| publishDate | 2009 |
| recordtype | eprints |
| repository_type | Digital Repository |
| spelling | nottingham-107792025-02-28T11:09:31Z https://eprints.nottingham.ac.uk/10779/ A functional specification of effects Swierstra, Wouter This dissertation is about effects and type theory. Functional programming languages such as Haskell illustrate how to encapsulate side effects using monads. Haskell compilers provide a handful of primitive effectful functions. Programmers can construct larger computations using the monadic return and bind operations. These primitive effectful functions, however, have no associated definition. At best, their semantics are specified separately on paper. This can make it difficult to test, debug, verify, or even predict the behaviour of effectful computations. This dissertation provides pure, functional specifications in Haskell of several different effects. Using these specifications, programmers can test and debug effectful programs. This is particularly useful in tandem with automatic testing tools such as QuickCheck. The specifications in Haskell are not total. This makes them unsuitable for the formal verification of effectful functions. This dissertation overcomes this limitation, by presenting total functional specifications in Agda, a programming language with dependent types. There have been alternative approaches to incorporating effects in a dependently typed programming language. Most notably, recent work on Hoare Type Theory proposes to extend type theory with axioms that postulate the existence of primitive effectful functions. This dissertation shows how the functional specifications implement these axioms, unifying the two approaches. The results presented in this dissertation may be used to write and verify effectful programs in the framework of type theory. 2009-07-23 Thesis (University of Nottingham only) NonPeerReviewed application/pdf en arr https://eprints.nottingham.ac.uk/10779/1/Thesis.pdf Swierstra, Wouter (2009) A functional specification of effects. PhD thesis, University of Nottingham. functional programming effects haskell type theory |
| spellingShingle | functional programming effects haskell type theory Swierstra, Wouter A functional specification of effects |
| title | A functional specification of effects |
| title_full | A functional specification of effects |
| title_fullStr | A functional specification of effects |
| title_full_unstemmed | A functional specification of effects |
| title_short | A functional specification of effects |
| title_sort | functional specification of effects |
| topic | functional programming effects haskell type theory |
| url | https://eprints.nottingham.ac.uk/10779/ |