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