------------------------------------------------------------------------
-- The Agda standard library
--
-- Wrapper for the erased modality
--
-- This allows us to store erased proofs in a record and use projections
-- to manipulate them without having to turn on the unsafe option
-- --irrelevant-projections.
------------------------------------------------------------------------

{-# OPTIONS --without-K --safe #-}

module Data.Erased where

open import Level using (Level)

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

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

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

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

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

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

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

infixl  _>>=_
_>>=_ : Erased A → (.A → Erased B) → Erased B
[ a ] >>= f = f a

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

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