[Agda] Applicative with arbitrary morphisms : how ?

[Daniel Peebles]

The Haskell definition of Applicative seems to rely on the existence of
exponential objects. If you encode Applicative by its liftA2 form (or liftA2
(,)) you just need products, and you get something like a lax monoidal
functor.

On Fri, Feb 18, 2011 at 5:32 PM, Permjacov Evgeniy <permeakra at gmail.com>wrote:

> let's assume following definitions (record members and parametrs with
> laws that must hold are dropped for simplicity)
>
> record categoryOps {oℓ aℓ : Level}
>  (obj : Set oℓ)
>  (_⇒_ : obj → obj → Set aℓ) : Set (oℓ ⊔ aℓ) where
>  field
>  id   : {o : obj} → o ⇒ o
>  _∘_  : {x y z : obj} → x ⇒ y → y ⇒ z → x ⇒ z
>
> record functorOps {oℓ₁ aℓ₁ oℓ₂ aℓ₂ : Level}
>  (obj₁ : Set oℓ₁)
>  (_⇒₁_ : obj₁ → obj₁ → Set aℓ₁)
>  (cat₁ : categoryOps obj₁ _⇒₁_)
>  (obj₂ : Set oℓ₂)
>  (_⇒₂_ : obj₂ → obj₂ → Set aℓ₂)
>  (cat₂ : categoryOps obj₂ _⇒₂_)
>  : Set (oℓ₁ ⊔ aℓ₁ ⊔ oℓ₂ ⊔ aℓ₂) where
>  field
>  liftO : obj₁ → obj₂
>  liftA : {x y : obj₁} → x ⇒₁ y → liftO x ⇒₂ liftO y
>
>
> monad can be codified with easy as it is simply an endofunctor with two
> special types of arrows
>
> record monadOps {oℓ aℓ : Level}
>  (obj : Set oℓ)
>  (_⇒_ : obj → obj → Set aℓ)
>  (cat : categoryOps obj _⇒_)
>  (fun : functorOps obj _⇒_ cat obj _⇒_ cat)
>  : Set (oℓ ⊔ aℓ) where
>  open functorOps fun
>  field
>  liftV : {o : obj} → o ⇒ liftO o
>  join  : {o : obj} → liftO (liftO o) ⇒ liftO o
>
> comonads can be codified in similiar way. However, 'applcative' cannot.
> The haskell base uses  function with type
>
> Applicative f => f (a -> b) -> f a -> f b
>
> When I tried to encode this function as f (a =>b) -> f (a) => f (b), I
> got typecheck error and it is understandable. A somehow worked (sorry,
> no code, I'm rewriting it from scratch) is encoding Combinative, that
> will be triple of endofunctor f, two endobifunctors 'ext' and 'int' and
> group of morphisms \all {a b} -> ext (f a) (f b) => f (int a b) . This
> should typecheck, however, such interface looks extremly heavyweight
> from perspective of size of declarations. So, what extension of
> functorOps may codify Applicative in sane way ?
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20110218/11659d80/attachment.html