git.iko.soy/Idris-dev
on master help sign in
Merge pull request #1107 from ziman/data-erased
86b2ef4Edwin Brady
libs/base/Data/Erased.idrnew file+29
compare with master
unifiedsplit
@@ -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,
22 Data.SortedMap, Data.SortedSet, Data.BoundedList,
22 Data.SortedMap, Data.SortedSet, Data.BoundedList,
23 Data.Vect, Data.HVect, Data.Vect.Quantifiers,
23 Data.Vect, Data.HVect, Data.Vect.Quantifiers,
24 Data.Floats, Data.Complex, Data.Heap, Data.Fun,
24 Data.Floats, Data.Complex, Data.Heap, Data.Fun,
25− Data.Rel, Data.Buffer,
25+ Data.Rel, Data.Buffer, Data.Erased,
26
26
27 Control.Isomorphism, Control.Isomorphism.Primitives,
27 Control.Isomorphism, Control.Isomorphism.Primitives,
28 Control.Monad.Identity,
28 Control.Monad.Identity,