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 #-}