git.iko.soy/Idris-dev
on master help sign in
Add Data.Erased to libs/base.
commit3aa1833c4bafbf1ba1d4c2371b09642bfe42cd31 authorMatus Tejiscak <ziman@functor.sk> dateThu 17 Apr 2014, 13:37 (13 years ago) parent7ed177a
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,