Wednesday, April 17, 2013

Applicatives do not need `pure`

A few days ago I said:

Usually, applicatives are assigned a third power, which is the power to take a plain object and bring it into the functor in the simplest way possible, eg 2 becomes [ 2 ]. This power is essential to writing generic, recursive programs with applicatives.

I take it back. I now believe that nothing interesting you can do with an applicative functor requires `pure`.

Assumption: if the only practical difference between two programs is that one applies pure at the very end, it is no more interesting than the other.

For example, pure 3 is not interesting, because it doesn't tell you anything that 3 doesn't, and (+) <$> (pure x) <*> (pure y) is not interesting because it is equivalent to pure (x + y).

I had been thinking of ways to represent events in FRP without bringing in memory issues that usually come with FRP. This meant I was spending a lot of time looking at different algebraic structures, and trying to peel off the assumptions that weren't needed. At one point I had a structure like the following:

     UnpureApplicatives.agda 

  1  module UnpureApplicatives where
  2  
  3  open import Level
  4  
  5  -- Here is a definition of applicatives that does not include
  6  -- a `pure` axiom.
  7  
  8  record UnpureApplicative {l} (F : Set l → Set l) : Set (suc l ⊔ suc zero) where
  9    field
 10      -- The basic map axiom.
 11      _ap\_ : ∀ {A B} (f : A → B) (x : F A) → F B
 12  
 13      -- The combine axiom.
 14      _/ap\_ : ∀ {A B} (f : F (A → B)) (x : F A) → F B

which has map and ap (as all applicatives do) but lacks pure, and provides no way of defining pure.

But we can still define something that is just as good as sequence:

     Test1.agda 

  1  open import Level
  2  open import UnpureApplicatives
  3  
  4  module Test1 {l} (F : _) (applicative : UnpureApplicative {l} F) where
  5      open import Data.List using (List; []; _∷_)
  6      open import Data.Sum using (_⊎_; inj₁; inj₂)
  7  
  8      open UnpureApplicative applicative
  9  
 10      -- We can derive this from the other two.
 11      -- Agda auto was actually able to solve this one.
 12      _/ap_ : ∀ {B} {A : Set l} (f : F (A → B)) (x : A) → F B
 13      _/ap_ f x = (λ z → z x) ap\ f
 14  
 15      -- This is how sequence now looks.
 16      -- It's ugly, but it gets the job done.
 17      sequence : ∀ {A} → List (F A) → List A ⊎ F (List A)
 18      sequence [] = inj₁ []
 19      sequence (x ∷ list) with sequence list
 20      ...                     | inj₁ plain = inj₂ ((_∷_ ap\ x) /ap plain)
 21      ...                     | inj₂ appy = inj₂ ((_∷_ ap\ x) /ap\ appy)

and the lack of pure is not "interesting" here because it may be applied at the end, by pattern matching on .

So what we've really done is use this "unpure" applicative to build a regular "pure" applicative:

     BuildFromUnpure.agda 

  1  open import UnpureApplicatives
  2  
  3  module BuildFromUnpure {l} (F : Set l → Set l) (Unpure : UnpureApplicative F) where
  4    open import Data.Sum using (_⊎_; inj₁; inj₂)
  5    open UnpureApplicative Unpure using (_ap\_; _/ap\_)
  6  
  7    F' : Set l → Set l
  8    F' A = A ⊎ F A
  9  
 10    pure : ∀ {A} → A → F' A
 11    pure = inj₁
 12  
 13    _/ap'\_ : ∀ {A B} (f : F' (A → B)) (x : F' A) → F' B
 14    inj₁ f /ap'\ inj₁ x = inj₁ (f x)
 15    inj₁ f /ap'\ inj₂ x = inj₂ (f ap\ x)
 16    inj₂ f /ap'\ inj₁ x = inj₂ ((λ f → f x) ap\ f)
 17    inj₂ f /ap'\ inj₂ x = inj₂ (f /ap\ x)

And I think it is clear that these two definitions are equally interesting, and, if a definition for pure were supplied originally, it could always be applied at the end, and so would add nothing.

Also, you could take an unpure applicative, make it a regular applicative, then drop the pure, and have something equivalent to the original unpure applicative.

No comments:

Post a Comment