09-higherOrderClasses.agda

{-# OPTIONS --universe-polymorphism #-}

module 09-higherOrderClasses where

open import Category.Applicative
open import Category.Monad
open import Category.Monad.Indexed
open import Function

lift : ∀ {a b c} {A : Set a} {C : Set c} {B : A → Set b} →
       ({{x : A}} → B x) → (f : C → A) → {{x : C}} → B (f x)
lift m f {{x}} = m {{f x}}

monadToApplicative : ∀ {l} {M : Set l → Set l} → RawMonad M → RawApplicative M
monadToApplicative = RawIMonad.rawIApplicative

liftAToM : ∀ {l} {V : Set l} {M : Set l → Set l} → ({{appM : RawApplicative M}} → M V) → 
           {{monadM : RawMonad M}} → M V
liftAToM app {{x}} = lift (λ {{appM}} → app {{appM}}) monadToApplicative {{x}}