Applicative functor

Last updated

In functional programming, an applicative functor, or an applicative for short, is an intermediate structure between functors and monads. In Category Theory they are called Closed Monoidal Functors [1] .Applicative functors allow for functorial computations to be sequenced (unlike plain functors), but don't allow using results from prior computations in the definition of subsequent ones (unlike monads). Applicative functors are the programming equivalent of lax monoidal functors with tensorial strength in category theory.

Contents

Applicative functors were introduced in 2008 by Conor McBride and Ross Paterson in their paper Applicative programming with effects. [2]

Applicative functors first appeared as a library feature in Haskell, but have since spread to other languages as well, including Idris, Agda, OCaml, Scala and F#. Glasgow Haskell, Idris, and F# offer language features designed to ease programming with applicative functors. In Haskell, applicative functors are implemented in the Applicative type class.

While in languages like Haskell monads are applicative functors, it is not always so in general settings of Category Theory - examples of monads that are not strong can be found on Math Overflow' [3] .

Definition

In Haskell, an applicative is a parameterized type that we think of as being a container for data of the parameter type plus two methods pure and <*>. The pure method for an applicative of parameterized type f has type

pure::a->fa

and can be thought of as bringing values into the applicative. The <*> method for an applicative of type f has type

(<*>)::f(a->b)->fa->fb

and can be thought of as the equivalent of function application inside the applicative. [4]

Alternatively, instead of providing <*>, one may provide a function called liftA2. These two functions may be defined in terms of each other; therefore only one is needed for a minimally complete definition. [5]

Applicatives are also required to satisfy four equational laws: [5]

Every applicative is a functor. To be explicit, given the methods pure and <*>, fmap can be implemented as [5] 

fmapgx=pureg<*>x

The commonly-used notation g<$>x is equivalent to pureg<*>x.

Examples

In Haskell, the Maybe type can be made an instance of the type class Applicative using the following definition: [4] 

instanceApplicativeMaybewhere-- pure :: a -> Maybe apurea=Justa-- (<*>) :: Maybe (a -> b) -> Maybe a -> Maybe bNothing<*>_=Nothing_<*>Nothing=Nothing(Justg)<*>(Justx)=Just(gx)

As stated in the Definition section, pure turns an a into a Maybea, and <*> applies a Maybe function to a Maybe value. Using the Maybe applicative for type a allows one to operate on values of type a with the error being handled automatically by the applicative machinery. For example, to add m::MaybeInt and n::MaybeInt, one needs only write

(+)<$>m<*>n

For the non-error case, adding m=Justi and n=Justj gives Just(i+j). If either of m or n is Nothing, then the result will be Nothing also. This example also demonstrates how applicatives allow a sort of generalized function application.

See also

Related Research Articles

In mathematics and computer science, currying is the technique of translating the evaluation of a function that takes multiple arguments into evaluating a sequence of functions, each with a single argument. For example, currying a function that takes three arguments creates a nested unary function , so that the code

In mathematics, specifically category theory, a functor is a mapping between categories. Functors were first considered in algebraic topology, where algebraic objects are associated to topological spaces, and maps between these algebraic objects are associated to continuous maps between spaces. Nowadays, functors are used throughout modern mathematics to relate various categories. Thus, functors are important in all areas within mathematics to which category theory is applied.

In combinatorial mathematics, the theory of combinatorial species is an abstract, systematic method for deriving the generating functions of discrete structures, which allows one to not merely count these structures but give bijective proofs involving them. Examples of combinatorial species are graphs, permutations, trees, and so on; each of these has an associated generating function which counts how many structures there are of a certain size. One goal of species theory is to be able to analyse complicated structures by describing them in terms of transformations and combinations of simpler structures. These operations correspond to equivalent manipulations of generating functions, so producing such functions for complicated structures is much easier than with other methods. The theory was introduced, carefully elaborated and applied by Canadian researchers around André Joyal.

In category theory, a category is Cartesian closed if, roughly speaking, any morphism defined on a product of two objects can be naturally identified with a morphism defined on one of the factors. These categories are particularly important in mathematical logic and the theory of programming, in that their internal language is the simply typed lambda calculus. They are generalized by closed monoidal categories, whose internal language, linear type systems, are suitable for both quantum and classical computation.

In mathematics, the idea of a free object is one of the basic concepts of abstract algebra. Informally, a free object over a set A can be thought of as being a "generic" algebraic structure over A: the only equations that hold between elements of the free object are those that follow from the defining axioms of the algebraic structure. Examples include free groups, tensor algebras, or free lattices.

In category theory, a branch of mathematics, a monad is a monoid in the category of endofunctors of some fixed category. An endofunctor is a functor mapping a category to itself, and a monad is an endofunctor together with two natural transformations required to fulfill certain coherence conditions. Monads are used in the theory of pairs of adjoint functors, and they generalize closure operators on partially ordered sets to arbitrary categories. Monads are also useful in the theory of datatypes, the denotational semantics of imperative programming languages, and in functional programming languages, allowing languages with non-mutable states to do things such as simulate for-loops; see Monad.

In functional programming, a monad is a structure that combines program fragments (functions) and wraps their return values in a type with additional computation. In addition to defining a wrapping monadic type, monads define two operators: one to wrap a value in the monad type, and another to compose together functions that output values of the monad type. General-purpose languages use monads to reduce boilerplate code needed for common operations. Functional languages use monads to turn complicated sequences of functions into succinct pipelines that abstract away control flow, and side-effects.

In computer science, arrows or bolts are a type class used in programming to describe computations in a pure and declarative fashion. First proposed by computer scientist John Hughes as a generalization of monads, arrows provide a referentially transparent way of expressing relationships between logical steps in a computation. Unlike monads, arrows don't limit steps to having one and only one input. As a result, they have found use in functional reactive programming, point-free programming, and parsers among other applications.

This is a glossary of properties and concepts in category theory in mathematics.

In mathematics, specifically in category theory, hom-sets give rise to important functors to the category of sets. These functors are called hom-functors and have numerous applications in category theory and other branches of mathematics.

In computer science, a type class is a type system construct that supports ad hoc polymorphism. This is achieved by adding constraints to type variables in parametrically polymorphic types. Such a constraint typically involves a type class T and a type variable a, and means that a can only be instantiated to a type whose members support the overloaded operations associated with T.

In category theory, the concept of catamorphism denotes the unique homomorphism from an initial algebra into some other algebra.

In many programming languages, map is a higher-order function that applies a given function to each element of a collection, e.g. a list or set, returning the results in a collection of the same type. It is often called apply-to-all when considered in functional form.

In computer programming, an anamorphism is a function that generates a sequence by repeated application of the function to its previous result. You begin with some value A and apply a function f to it to get B. Then you apply f to B to get C, and so on until some terminating condition is reached. The anamorphism is the function that generates the list of A, B, C, etc. You can think of the anamorphism as unfolding the initial value into a sequence.

In mathematics and computer science, apply is a function that applies a function to arguments. It is central to programming languages derived from lambda calculus, such as LISP and Scheme, and also in functional languages. It has a role in the study of the denotational semantics of computer programs, because it is a continuous function on complete partial orders. Apply is also a continuous function in homotopy theory, and, indeed underpins the entire theory: it allows a homotopy deformation to be viewed as a continuous path in the space of functions. Likewise, valid mutations (refactorings) of computer programs can be seen as those that are "continuous" in the Scott topology.

Substructural type systems are a family of type systems analogous to substructural logics where one or more of the structural rules are absent or only allowed under controlled circumstances. Such systems are useful for constraining access to system resources such as files, locks, and memory by keeping track of changes of state that occur and preventing invalid states.

In programming languages and type theory, an option type or maybe type is a polymorphic type that represents encapsulation of an optional value; e.g., it is used as the return type of functions which may or may not return a meaningful value when they are applied. It consists of a constructor which either is empty, or which encapsulates the original data type A.

This article describes the features in the programming language Haskell.

Idris is a purely-functional programming language with dependent types, optional lazy evaluation, and features such as a totality checker. Idris may be used as a proof assistant, but is designed to be a general-purpose programming language similar to Haskell.

<span class="mw-page-title-main">Functor (functional programming)</span> Design pattern in pure functional programming

In functional programming, a functor is a design pattern inspired by the definition from category theory that allows one to apply a function to values inside a generic type without changing the structure of the generic type. In Haskell this idea can be captured in a type class:

References

  1. ↑ {{url=https://math.stackexchange.com/questions/4254772/definition-of-closed-monoidal-functor}}
  2. ↑ McBride, Conor; Paterson, Ross (2008-01-01). "Applicative programming with effects". Journal of Functional Programming. 18 (1): 1–13. CiteSeerX   10.1.1.114.1555 . doi:10.1017/S0956796807006326. ISSN   1469-7653.
  3. ↑ {{url=https://mathoverflow.net/questions/85391/any-example-of-a-non-strong-monad}}
  4. 1 2 Hutton, Graham (2016). Programming in Haskell (2 ed.). pp. 157–163.
  5. 1 2 3 "Control.Applicative".
This page is based on this Wikipedia article
Text is available under the CC BY-SA 4.0 license; additional terms may apply.
Images, videos and audio are available under their respective licenses.