Applicative Lifting

Applicative functors augment computations with effects by lifting function application to types which model the effects [5]. As the structure of the computation cannot depend on the effects, applicative expressions can be analysed statically. This allows us to lift universally quantified equations to the effectful types, as observed by Hinze [3]. Thus, equational reasoning over effectful computations can be reduced to pure types. This entry provides a package for registering applicative functors and two proof methods for lifting of equations over applicative functors. The first method applicative-nf normalises applicative expressions according to the laws of applicative functors. This way, equations whose two sides contain the same list of variables can be lifted to every applicative functor. To lift larger classes of equations, the second method applicativelifting exploits a number of additional properties (e.g., commutativity of effects) provided the properties have been dec...

• Type: Journal
• Year: 2015
• Where: AFP
• Authors: Andreas Lochbihler, Joshua Schneider
• Keywords: AFP 2015, Formal Methods