open import 1Lab.Equiv
open import 1Lab.Type

open import Data.Sum.Base

open import Meta.Idiom
open import Meta.Alt

module Meta.Invariant where


# Meta: Invariantπ

An Invariant functor is, informally, one that has both a covariant and a contravariant dependency on its argument type. For a motivating example, think of Dec.

record Invariant (M : Effect) : TypeΟ where
private module M = Effect M
field
invmap
: β {β} {ββ²} {A : Type β} {B : Type ββ²}
β (A β B) β (B β A) β M.β A β M.β B

open Invariant β¦ ... β¦ public

_<β>_
: β {β β'} {M : Effect} β¦ _ : Invariant M β¦ {A : Type β} {B : Type β'}
β A β B β M .Effect.β A β M .Effect.β B
_<β>_ f = invmap (Equiv.to f) (Equiv.from f)


We also provide versions of Idiom and Alt that only require an invariant functor instead of a covariant one. A functor is Monoidal if it commutes with products, and Alternative if it turns sums into products.

record Monoidal (M : Effect) : TypeΟ where
private module M = Effect M
field
β¦ Invariant-monoidal β¦ : Invariant M
munit : M.β β€
_<,>_
: β {β} {ββ²} {A : Type β} {B : Type ββ²}
β M.β A β M.β B β M.β (A Γ B)

infixl 4 _<,>_

record Alternative (M : Effect) : TypeΟ where
private module M = Effect M
field
β¦ Invariant-alternative β¦ : Invariant M
empty : M.β β₯
_<+>_
: β {β} {ββ²} {A : Type β} {B : Type ββ²}
β M.β A β M.β B β M.β (A β B)

infixl 3 _<+>_

open Monoidal β¦ ... β¦ public
open Alternative β¦ ... β¦ public


We provide blanket instances mapping covariant classes to their invariant counterparts.

instance
Invariant-Map : β {M : Effect} β β¦ Map M β¦ β Invariant M
Invariant-Map .Invariant.invmap f _ = f <$>_ {-# OVERLAPPABLE Invariant-Map #-} Monoidal-Idiom : β {M : Effect} β β¦ Idiom M β¦ β Monoidal M Monoidal-Idiom .Monoidal.munit = pure tt Monoidal-Idiom .Monoidal._<,>_ ma mb = _,_ <$> ma <*> mb
{-# OVERLAPPABLE Monoidal-Idiom #-}

Alternative-Alt : β {M : Effect} β β¦ Map M β¦ β β¦ Alt M β¦ β Alternative M
Alternative-Alt .Alternative.empty = fail
Alternative-Alt .Alternative._<+>_ ma mb = inl <$> ma <|> inr <$> mb
{-# INCOHERENT Alternative-Alt #-}