git.iko.soy/Idris-dev
on master help sign in
Merge pull request #1107 from ziman/data-erased

Add Data.Erased to libs/base

commit86b2ef4ece9094bdbb65bc5b3e69a5231beb9604 authorEdwin Brady <edwin.brady@gmail.com> dateFri 25 Apr 2014, 09:53 (13 years ago) parent198d067dd6b95a
2 files changed+30−1
compare with master
unifiedsplit
libs/base/Data/Erased.idr+29 libs/base/base.ipkg+1−1
libs/base/Data/Erased.idrnew file+29
@@ -0,0 +1,29 @@
1+module Data.Erased
2+
3+%access public
4+%default total
5+
6+||| The erasure monad.
7+|||
8+||| Used when explicit modelling of erasure in the type system is needed.
9+data Erased : Type -> Type where
10+
11+ ||| Construct an erased value from any value.
12+ Erase : .(x : a) -> Erased a
13+
14+instance Functor Erased where
15+ map f (Erase x) = Erase (f x)
16+
17+instance Applicative Erased where
18+ pure = Erase
19+ (<$>) (Erase f) (Erase x) = Erase (f x)
20+
21+instance Monad Erased where
22+ (>>=) (Erase x) f = f x
23+
24+||| Project the erased value out of the monad.
25+|||
26+||| This is usable only in types and other erased contexts,
27+||| where it won't cause erasure violations.
28+unerase : Erased a -> a
29+unerase (Erase x) = x
libs/base/base.ipkg+1−1
@@ -22,7 +22,7 @@ modules = System,
2222 Data.SortedMap, Data.SortedSet, Data.BoundedList,
2323 Data.Vect, Data.HVect, Data.Vect.Quantifiers,
2424 Data.Floats, Data.Complex, Data.Heap, Data.Fun,
25− Data.Rel, Data.Buffer,
25+ Data.Rel, Data.Buffer, Data.Erased,
2626
2727 Control.Isomorphism, Control.Isomorphism.Primitives,
2828 Control.Monad.Identity,