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