Erased.idr

module Data.Erased

%access public
%default total

||| The erasure monad.
|||
||| Used when explicit modelling of erasure in the type system is needed.
data Erased : Type -> Type where

    ||| Construct an erased value from any value.
    Erase : .(x : a) -> Erased a

instance Functor Erased where
  map f (Erase x) = Erase (f x)

instance Applicative Erased where
  pure = Erase
  (<$>) (Erase f) (Erase x) = Erase (f x)

instance Monad Erased where
  (>>=) (Erase x) f = f x

||| Project the erased value out of the monad.
|||
||| This is usable only in types and other erased contexts,
||| where it won't cause erasure violations.
unerase : Erased a -> a
unerase (Erase x) = x