Why type of pure is a -> f a, not (a -> b) -> f (a -> b) on Applicative?-CodePudding

Pure is used to transform normal function into function in Applicative container. With this, any multi-parameter operations become can be used on Applicative. In this context, pure is not desired to be a -> f a type, it is just desired to be (a -> b) -> f (a -> b) type. But type of pure is a -> f a. Why should normal values can be transformed into Applicative? Is there more purpose for use pure more than transforming functions?

CodePudding user response：

You can define pure :: a -> f a in terms of lift :: (a -> b) -> f (a -> b) and <*>:

pure x = lift (const x) <*> lift (const ())

So it's equivalent either way, and usually simpler to write pure.

CodePudding user response：

I don't find the Applicative interface of applying lifted functions (namely, (<*>)) a good intuition. Functions are more complicated to conceptualize for various reasons.

I prefer thinking of Applicative as lifting an n-ary function

liftA0 :: Applicative f => (a)                -> (f a)
liftA  :: Functor     f => (a -> b)           -> (f a -> f b)
liftA2 :: Applicative f => (a -> b -> c)      -> (f a -> f b -> f c)
liftA3 :: Applicative f => (a -> b -> c -> d) -> (f a -> f b -> f c -> f d)

where liftA0 = pure and liftA already exists as fmap defined in terms of Applicative.

The thing is that 0-ary and 1-ary liftings

liftA0 @f @a    :: Applicative f => a -> f a
liftA  @f @a @b :: Applicative f => (a -> b) -> (f a -> f b)

can both take an a -> b function if we instantiate liftA0 = pure at a function type:

liftA0 @f @(a->b) :: Applicative f => (a -> b) -> f (a->b)
liftA  @f @a @b   :: Applicative f => (a -> b) -> (f a -> f b)

So pure @f @(a->b) already has that type.

And pure has plenty of purposes, theoretical which turn out to be practical in Haskell, it is the unit if Applicative is viewed as a Monoid in the category of natural transformations, with (Notions of Computation as Monoids) with Day

type Mempty :: Type -> Type
type Mempty = Identity

type Mappend :: (Type -> Type) -> (Type -> Type) -> (Type -> Type)
type Mappend = Day

mempty :: Applicative f => Mempty ~> f
mempty (Identity a) = pure a

mappend :: Mappend f f ~> f
mappend (LiftA2 (·) as bs) = liftA2 (·) as bs

I just released a library that works with Applicative functions, that are polymorphic functions that respect the applicative structure. It defines a type class for such structures

type  Idiom :: k -> (Type -> Type) -> (Type -> Type) -> Constraint
class (Applicative f, Applicative g) => Idiom tag f g where
  idiom :: f ~> g

where pure is the initial applicative morphism.

-- https://chrisdone.com/posts/haskell-constraint-trick/
instance (Identity ~ id, Applicative f) => Idiom Initial id f where
  idiom :: Identity ~> f
  idiom (Identity a) = pure a

pure as an unit is then use often, as a driving force in Traversable one of the success stories of Haskell

instance Traversable [] where
  traverse :: Applicative f => (a -> f b) -> ([a] -> f [b])
  traverse f []     = pure []
  traverse f (x:xs) = ...

we require pure because our only argument that produces an Applicative-action is f x but with an empty list we don't have an x :: a to feed it. Thus, we need 0-ary lifting.

CodePudding user response：

Yes, there is more purpose for pure than transforming functions. It is very common for do blocks to end with a call to pure. It's also handy for giving fallback values by combining its use with <|>.

Also, it meshes well with the underlying category theory; but I don't really consider that a motivating reason. Rather it's first useful and then discovered to coincide with a previously-known category theory concept. (Actually, historically I think it went "define something useful; realize it's the concept of monad; discover the related concept of applicative functors; realize they're useful. So it is in fact a mix of "useful first" and "theory first". But I would never defend its existence because it's there in theory -- only get excited that the theory was insightful.)