open import 1Lab.Type

open import Data.List.Base

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
    _<$>_ : βˆ€ {β„“} {β„“β€²} {A : Type β„“} {B : Type β„“β€²} β†’ (A β†’ B) β†’ M.β‚€ A β†’ M.β‚€ B

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

  _<&>_ : βˆ€ {β„“} {β„“β€²} {A : Type β„“} {B : Type β„“β€²} β†’ M.β‚€ A β†’ (A β†’ B) β†’ M.β‚€ B
  x <&> f = f <$> x

instance
  Map-List : Map (eff List)
  Map-List .Map._<$>_ = map

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 Map ⦃ ... ⦄ public
open Idiom ⦃ ... ⦄ public