------------------------------------------------------------------------
-- The Agda standard library
--
-- Wrapper for the proof irrelevance modality
--
-- This allows us to store proof irrelevant witnesses in a record and
-- use projections to manipulate them without having to turn on the
-- unsafe option --irrelevant-projections.
-- Cf. Data.Refinement for a use case
------------------------------------------------------------------------

{-# OPTIONS --cubical-compatible --safe #-}

module Data.Irrelevant where

open import Level using (Level)
open import Relation.Nullary.Recomputable.Core using (Recomputable)

private
  variable
    a b c : Level
    A : Set a
    B : Set b
    C : Set c

------------------------------------------------------------------------
-- Type

record Irrelevant (A : Set a) : Set a where
  constructor [_]
  field .irrelevant : A
open Irrelevant public

------------------------------------------------------------------------
-- Relationship with the . modality: wrapped/unwrapped abstraction

λ∙⁻ : (.A → B) → Irrelevant A → B
λ∙⁻ f [ a ] = f a
{-# INLINE λ∙⁻ #-}

λ∙⁺ : (Irrelevant A → B) → .A → B
λ∙⁺ f a = f [ a ]
{-# INLINE λ∙⁺ #-}

-- Irrelevant types are Recomputable

recompute : Recomputable (Irrelevant A)
irrelevant (recompute [ a ]) = a

------------------------------------------------------------------------
-- Algebraic structure: Functor, Appplicative and Monad

map : (A → B) → Irrelevant A → Irrelevant B
map f [ a ] = [ f a ]

pure : A → Irrelevant A
pure x = [ x ]

infixl  _<*>_
_<*>_ : Irrelevant (A → B) → Irrelevant A → Irrelevant B
[ f ] <*> [ a ] = [ f a ]

infixl  _>>=_
_>>=_ : Irrelevant A → (A → Irrelevant B) → Irrelevant B
[ a ] >>= f = recompute (f a)

------------------------------------------------------------------------
-- Other functions

zipWith : (A → B → C) → Irrelevant A → Irrelevant B → Irrelevant C
zipWith f a b = ⦇ f a b ⦈