Implementation of Pattern Matching Calculus Using Type-Indexed Expressions

Abstract

<p> The pattern matching calculus introduced by Kahl provides a fine-grained mechanism of modelling non-strict pattern matching in modern functional programming languages. By changing the rule of interpreting the empty expression that results from matching failures, the pattern matching calculus can be transformed into another calculus that abstracts a "more successful" evaluation. Kahl also showed that the two calculi have both a confluent reduction system and a same normalising strategy, which constitute the operational semantics of the pattern matching calculi.</p> <p> As a new technique based on Haskell's language extensions of type-saft cast, arbitrary-rank polymorphism and generalised algebraic data types, type-indexed expressions introduced by Kahl demonstrate a uniform way of defining all expressions as type-indexed to guarantee type safety.</p> <p> In this thesis, we implemented the type-indexed syntax and operational semantics of the pattern matching calculi using type-indexed expressions. Our type-indexed syntax mirrors the definition of the pattern matching calculi. We implemented the operational semantics of the two calculi perfectly and provided reduction and normalisation examples that show that the pattern matching calculus can be a useful basis of modelling non-strict pattern matching.</p> <p> We formalised and implemented the bimonadic semantics of the pattern matching calculi using categorical concepts and type-indexed expressions respectively. The bimonadic semantics employs two monads to reflect two kinds of computational effects, which correspond to the two major syntactic categories of the pattern matching calculi, i.e. expressons and matchings. Thus, the resulting implementation provides the detotational model of non-strict pattern matching with more accuracy.</p> <p> Finally, from a practical programming viewpoint, our implementation is a good demonstration of how to program in the pure type-indexed setting by taking fully advantage of Haskell's language extensions of type-safe cast, arbitrary-rank polymorphism and generalised algebraic data types.</p>