0 | ||| A module defining the `Some` type
 1 | module Data.Some
 2 |
 3 | import public Data.DEq
 4 | import public Data.DOrd
 5 | import public Data.DShow
 6 |
 7 | ||| Wraps a dependent type, so that its parameter is hidden.
 8 | ||| Values of dependent types, wrapped this way, have the same type
 9 | ||| @ f the type constructor of types of the wrapped values.
10 | public export
11 | data Some : (f : t -> Type) -> Type where
12 |   ||| Hide the type parameter of the type of a value
13 |   ||| @ a the parameter of the type of the wrapped value
14 |   ||| @ x the wrapped value
15 |   MkSome : {0 a : t} -> (x : f a) -> Some f
16 |
17 | export
18 | implementation (impl : DEq f) => Eq (Some f) where
19 |   MkSome x == MkSome y = deq' x y @{impl}
20 |
21 | export
22 | implementation (impl : DOrd f) => Ord (Some f) where
23 |   compare (MkSome x) (MkSome y) = case dcompare x y @{impl} of
24 |     DLT => LT
25 |     DGT => GT
26 |     DEQ => EQ
27 |
28 | export
29 | implementation (impl : DShow f) => Show (Some f) where
30 |   showPrec prec (MkSome fx) = showCon prec "MkSome" (dshowArg fx @{impl})
31 |
32 | ||| Apply a dependency-removing function to the value wrapped in `Some` and
33 | ||| drop the wrapper
34 | export
35 | withSome : Some f -> ({0 x : a} -> f x -> b) -> b
36 | withSome (MkSome thing) some = some thing
37 |
38 | ||| Monadic 'withSome'.
39 | export
40 | withSomeM : Monad m => m (Some f) -> ({0 x : a} -> f x -> m b) -> m b
41 | withSomeM m k = m >>= (\s => withSome s k)
42 |
43 | |||| `'flip' 'withSome'`
44 | export
45 | foldSome : ({0 a : t} -> tag a -> b) -> Some tag -> b
46 | foldSome some (MkSome thing) = some thing
47 |
48 | ||| Apply a function to the wrapped value
49 | export
50 | map : ({0 a : t} -> f a -> g a) -> Some f -> Some g
51 | map f (MkSome x) = MkSome (f x)
52 |
53 | ||| Traverse over argument.
54 | export
55 | traverseSome : Functor m => ({0 a : t} -> f a -> m (g a)) -> Some f -> m (Some g)
56 | traverseSome f (MkSome x) = map MkSome (f x)
57 |
58 | export
59 | implementation Applicative m => Semigroup (Some m) where
60 |   MkSome mx <+> MkSome my = MkSome (mx *> my)
61 |
62 | export
63 | implementation Applicative m => Monoid (Some m) where
64 |   neutral = MkSome (pure ())
65 |