0 | ||| This module defines `Wrap0`, a wrapper type containing a value
 1 | ||| that is present at compile-time, but erased during run-time. This
 2 | ||| wrapper is used to define categories with erased objects, such as
 3 | ||| the category of types `Typ`.
 4 | module Data.Wrap0
 5 |
 6 | %default total
 7 |
 8 | ||| A wrapper for a value that is erased at runtime.
 9 | public export
10 | record Wrap0 (a : Type) where
11 |   constructor W0
12 |   0 runW0 : a
13 |
14 | ||| Lift a function to act on `Wrap0` values. Since the values it
15 | ||| operates on are erased, the function does not have to exist at
16 | ||| runtime.
17 | public export
18 | liftW : (0 f : a -> b) -> Wrap0 a -> Wrap0 b
19 | liftW f x = W0 (f x.runW0)
20 |
21 | ||| Lift a binary operation to act on `Wrap0` values. Since the values
22 | ||| it operates on are erased, the function does not have to exist at
23 | ||| runtime.
24 | public export
25 | liftW2 : (0 f : a -> b -> c) -> Wrap0 a -> Wrap0 b -> Wrap0 c
26 | liftW2 f x y = W0 (f x.runW0 y.runW0)
27 |
28 |
29 | -- I doubt these interface implementations will be of much use, but
30 | -- they might as well be defined.
31 |
32 | public export
33 | Functor Wrap0 where
34 |   map f x = W0 (f x.runW0)
35 |
36 | public export
37 | Applicative Wrap0 where
38 |   pure x = W0 x
39 |   f <*> x = W0 (f.runW0 x.runW0)
40 |
41 | public export
42 | Monad Wrap0 where
43 |   join x = W0 x.runW0.runW0
44 |   x >>= f = W0 (f x.runW0).runW0
45 |
46 |
47 | ||| A type that is erased at runtime.
48 | public export
49 | Type0 : Type
50 | Type0 = Wrap0 Type
51 |