Programming and static analysis with graded monads

Programmers writing purely functional code have long represented impure, side-effecting computation using monads. Recent research in program semantics has focussed on graded monads, a useful generalisation of monads which allow the programmer to establish useful properties of a computation purely from their type of a computation. They have been used to represent a variety of properties traditionally inferred by frameworks such as type-and-effect systems -- for example, success of partial computation and taint checking. However, their use has been limited to defining the formal semantics of type-and-effect systems and to embedding effect systems into pure functional languages (such as Haskell). Graded monads have not previously been seen as an interesting programming construct on their own. This thesis explores the capability of graded monads to represent a variety of program analyses in a unified fashion, as well as the extent to which programmers are able to define their own interesting program analyses. This thesis first defines the class of analysis-graded monads, a class of graded monads whose intended use is to represent what is commonly thought of as `program analysis’ or `effect system’. A contribution of this thesis is a zoo of examples of analysis-graded monads, as well as their representation in Haskell. Analysis-graded monads are considered from both the programming side and as a tool for defining a denotational semantics (using category theory). The thesis considers the matters of type inference in language with support for graded monadic types, effectively framing program analysis as a question of type (and grade) inference. A practical implementation comes in the form of a Haskell package (analysis-monad). The remaining contributions of the thesis address the use of analysis-graded monads in more sophisticated settings and large programs. Firstly, I consider computations and associated analyses that can be seen as being parameterised by a set of distinct components (such as individual exception names forming an analysis similar to Java checked exceptions), and propose the concept of graded monad builders as a way of generating such analysis given a set of such component names. Secondly, I look at the question of combining more than one analysis, which effectively means combining the role of several analysis-graded monads. This research on programming with graded monads and their use in program analysis informs conclusions about the way program analysis for effectful computation can be seen as an instance of typing.

Name dc:type.qualificationname

Doctor of Philosophy (PhD)

Level dc:type.qualificationlevel

Doctoral

Grantor dc:publisher.institution

University of Cambridge

Year dc:date.issued

2022

Author dc:creator

• Ivaskovic, Andrej

Advisor dc:contributor.advisor

• Mycroft, Alan

• graded monads
• program analysis
• monads
• type systems

Licence

• https://creativecommons.org/licenses/by/4.0/

Language dc:language

eng

Author Identifier

0000-0002-1347-4884

OAI identifier oai:identifier

oai:www.repository.cam.ac.uk:1810/346522