open import 1Lab.Type

module Meta.Idiom where

Meta: IdiomπŸ”—

The Idiom class, probably better known as Applicative (from languages like Haskell and the Agda standard library), captures the β€œeffects with parallel composition”, where an β€œeffect” is simply a mapping from types to types, with an arbitrary adjustment of universe levels:

record Effect : Typeω where
  constructor eff
  field
    {adj} : Level β†’ Level
    β‚€     : βˆ€ {β„“} β†’ Type β„“ β†’ Type (adj β„“)

The adjustment of universe levels lets us consider, for example, a β€œpower set” effect, where the adjustment is given by lsuc. In most cases, Agda can infer the adjustment, so we can use the eff constructor.

record Map (M : Effect) : Typeω where
  private module M = Effect M
  field
    map : βˆ€ {β„“} {β„“'} {A : Type β„“} {B : Type β„“'} β†’ (A β†’ B) β†’ M.β‚€ A β†’ M.β‚€ B

record Idiom (M : Effect) : Typeω where
  private module M = Effect M
  field
    ⦃ Map-idiom ⦄ : Map M
    pure  : βˆ€ {β„“} {A : Type β„“} β†’ A β†’ M.β‚€ A
    _<*>_ : βˆ€ {β„“} {β„“'} {A : Type β„“} {B : Type β„“'} β†’ M.β‚€ (A β†’ B) β†’ M.β‚€ A β†’ M.β‚€ B

  infixl 4 _<*>_

open Idiom ⦃ ... ⦄ public
open Map   ⦃ ... ⦄ public

infixl 4 _<$>_ _<&>_

_<$>_ : βˆ€ {β„“ β„“'} {M : Effect} ⦃ _ : Map M ⦄ {A : Type β„“} {B : Type β„“'}
      β†’ (A β†’ B) β†’ M .Effect.β‚€ A β†’ M .Effect.β‚€ B
f <$> x = map f x

_<$_ : βˆ€ {β„“ β„“'} {M : Effect} ⦃ _ : Map M ⦄ {A : Type β„“} {B : Type β„“'}
      β†’ B β†’ M .Effect.β‚€ A β†’ M .Effect.β‚€ B
c <$ x = map (Ξ» _ β†’ c) x

_<&>_ : βˆ€ {β„“ β„“'} {M : Effect} ⦃ _ : Map M ⦄ {A : Type β„“} {B : Type β„“'}
      β†’ M .Effect.β‚€ A β†’ (A β†’ B) β†’ M .Effect.β‚€ B
x <&> f = map f x

module _
  {M N : Effect} (let module M = Effect M; module N = Effect N) ⦃ _ : Map M ⦄ ⦃ _ : Map N ⦄
  {β„“} {β„“'} {A : Type β„“} {B : Type β„“'}
  where

  _<<$>>_ : (A β†’ B) β†’ M.β‚€ (N.β‚€ A) β†’ M.β‚€ (N.β‚€ B)
  f <<$>> a = (f <$>_) <$> a

  _<<&>>_ : M.β‚€ (N.β‚€ A) β†’ (A β†’ B) β†’ M.β‚€ (N.β‚€ B)
  x <<&>> f = f <<$>> x

when : βˆ€ {M : Effect} (let module M = Effect M) ⦃ app : Idiom M ⦄
     β†’ Bool β†’ M.β‚€ ⊀ β†’ M.β‚€ ⊀
when true  t = t
when false _ = pure tt

unless : βˆ€ {M : Effect} (let module M = Effect M) ⦃ app : Idiom M ⦄
       β†’ Bool β†’ M.β‚€ ⊀ β†’ M.β‚€ ⊀
unless false t = t
unless true  _ = pure tt