### Abstract

Applicative functors augment computations with effects by lifting function application to types which model the effects. 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. 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 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 exploits a number of additional properties (e.g., commutativity of effects) provided the properties have been declared for the concrete applicative functor at hand upon registration.

We declare several types from the Isabelle library as applicative functors and illustrate the use of the methods with two examples: the lifting of the arithmetic type class hierarchy to streams and the verification of a relabelling function on binary trees. We also formalise and verify the normalisation algorithm used by the first proof method.

### License

BSD License

### History

June 10, 2016
  implemented automatic derivation of lifted combinator reductions; support arbitrary lifted relations using relators; improved compatibility with locale interpretation (revision ec336f354f37)
March 3, 2016
  added formalisation of lifting with combinators

### Topics

- Computer science/Functional programming

### Session Applicative_Lifting

- Applicative
- Applicative_Environment
- Applicative_Option
- Applicative_Sum
- Applicative_Set
- Applicative_List
- Applicative_DNEList
- Applicative_Monoid
- Applicative_Filter
- Applicative_State
- Applicative_Stream
- Applicative_Open_State
- Applicative_PMF
- Applicative_Probability_List
- Applicative_Star
- Applicative_Vector
- Applicative_Functor
- Applicative_Environment_Algebra
- Stream_Algebra
- Tree_Relabelling
- Applicative_Examples
- Joinable
- Beta_Eta
- Combinators
- Idiomatic_Terms
- Abstract_AF
- Applicative_Test

### Used by

- CryptHOL
- The Stern-Brocot Tree
- Free Groups
- Locally Nameless Sigma Calculus

## Cite

×

Applicative_Lifting-AFP

    @article{Applicative_Lifting-AFP,
      author  = {Andreas Lochbihler and Joshua Schneider},
      title   = {Applicative Lifting},
      journal = {Archive of Formal Proofs},
      month   = {December},
      year    = {2015},
      note    = {\url{https://isa-afp.org/entries/Applicative_Lifting.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 18, 2020 : Isabelle2020
- Jun 11, 2019 : Isabelle2019
- Aug 16, 2018 : Isabelle2018
- Oct 10, 2017 : Isabelle2017
- Dec 17, 2016 : Isabelle2016-1
- Feb 22, 2016 : Isabelle2016
- Dec 22, 2015 : Isabelle2015