Programming with algebraic effects

One of the concepts that programming language theory deals with are computational effects such as input/output, state, exceptions and nondeterminism. They can be represented in various ways. A novel approach is used by the programming language eff where they are modeled using algebraic theories. Effects are first-class objects in eff which gives us new ways of solving various problems. In the first part of this thesis the basic language is presented, followed by a number of examples demonstrating effects and handlers, and the various possibilities offered by this new approach. Eff is in many ways similar to OCaml and other languages in the ML family. One example is the support for patterns, which are used to match and decompose values. Pattern matching is used in case analysis, which is a control structure that uses a list of patterns to determine a branch of program execution according to the input value. The branch corresponding to the first pattern matching that value is selected; the analysis is said to be exhaustive if every possible value is matched by at least one pattern. If a given input value does not match any pattern, a runtime error occurs. The practical goal of this thesis was to implement an algorithm to check case analyses for exhaustiveness. The idea is to warn programmers about possible inexhaustive matchings and also produce an example of an unmatched value. The algorithm and its implementation are described in the second part of the thesis. Finally, the limitations and some possible improvements of our work are stated