Mehner, Stefan Georg: Tools for Reasoning about Effectful Declarative Programs. - Bonn, 2015. - Dissertation, Rheinische Friedrich-Wilhelms-Universität Bonn.

Online-Ausgabe in bonndoc: https://nbn-resolving.org/urn:nbn:de:hbz:5n-41789

Online-Ausgabe in bonndoc: https://nbn-resolving.org/urn:nbn:de:hbz:5n-41789

@phdthesis{handle:20.500.11811/6552,

urn: https://nbn-resolving.org/urn:nbn:de:hbz:5n-41789,

author = {{Stefan Georg Mehner}},

title = {Tools for Reasoning about Effectful Declarative Programs},

school = {Rheinische Friedrich-Wilhelms-Universität Bonn},

year = 2015,

month = oct,

note = {In the pure functional language Haskell, nearly all side-effects that a function can produce have to be noted in its type. This includes input/output, propagation of a state, and nondeterminism. If no side-effects are noted, such a function acts like a mathematical function, i.e., mapping arguments to unique results. In that case, expressions in a program can be reasoned about like mathematical expressions. In addition to this socalled equational reasoning, the type system also enables type based reasoning. One example are free theorems - equations between expressions that are true only due to the types of the expressions involved. Some such statements serve as formal justification for optimization strategies in compilers.

The thesis at hand investigates two generalizations of such methods for programs not free of side-effects, i.e., effectful programs. First, effectful traversals of data structures are being studied. The most important contribution in this part is that a data structure can be lawfully traversed if, and only if, it is isomorphic to a polynomial functor. This result links the widespread interface of traversing to a clear intuition regarding the structure and behavior of the data type. Furthermore, tools are presented facilitating convenient proofs about effectful traversals.

Second, free theorems for the functional-logic language Curry are derived. Due to the close relationship between both languages, Curry can be understood as Haskell with built-in nondeterminism, i.e., a built-in side-effect. Equational and type based reasoning can both be adapted to Curry to a certain degree. In particular, short cut fusion - a very fertile runtime optimization - is enabled for Curry.},

url = {http://hdl.handle.net/20.500.11811/6552}

}

urn: https://nbn-resolving.org/urn:nbn:de:hbz:5n-41789,

author = {{Stefan Georg Mehner}},

title = {Tools for Reasoning about Effectful Declarative Programs},

school = {Rheinische Friedrich-Wilhelms-Universität Bonn},

year = 2015,

month = oct,

note = {In the pure functional language Haskell, nearly all side-effects that a function can produce have to be noted in its type. This includes input/output, propagation of a state, and nondeterminism. If no side-effects are noted, such a function acts like a mathematical function, i.e., mapping arguments to unique results. In that case, expressions in a program can be reasoned about like mathematical expressions. In addition to this socalled equational reasoning, the type system also enables type based reasoning. One example are free theorems - equations between expressions that are true only due to the types of the expressions involved. Some such statements serve as formal justification for optimization strategies in compilers.

The thesis at hand investigates two generalizations of such methods for programs not free of side-effects, i.e., effectful programs. First, effectful traversals of data structures are being studied. The most important contribution in this part is that a data structure can be lawfully traversed if, and only if, it is isomorphic to a polynomial functor. This result links the widespread interface of traversing to a clear intuition regarding the structure and behavior of the data type. Furthermore, tools are presented facilitating convenient proofs about effectful traversals.

Second, free theorems for the functional-logic language Curry are derived. Due to the close relationship between both languages, Curry can be understood as Haskell with built-in nondeterminism, i.e., a built-in side-effect. Equational and type based reasoning can both be adapted to Curry to a certain degree. In particular, short cut fusion - a very fertile runtime optimization - is enabled for Curry.},

url = {http://hdl.handle.net/20.500.11811/6552}

}