0 | module Control.Lens.Equality
 1 |
 2 | import Control.Lens.Optic
 3 |
 4 | %default total
 5 |
 6 |
 7 | ------------------------------------------------------------------------------
 8 | -- Type definitions
 9 | ------------------------------------------------------------------------------
10 |
11 |
12 | -- This type is trivial and thus really isn't necessary;
13 | -- it's only defined and used in order to assist Idris with optic coersion.
14 | public export
15 | record IsEquality {0 k,k' : _} (p : k -> k' -> Type) where
16 |   constructor MkIsEquality
17 |
18 |
19 | ||| An `Equality s t a b` is a witness that `(s = a, t = b)` that can be used
20 | ||| as an optic.
21 | |||
22 | ||| The canonical `Equality` is `id : Equality a b a b`.
23 | |||
24 | ||| An `Equality` can be coerced to any other optic.
25 | public export
26 | 0 Equality : k -> k' -> k -> k' -> Type
27 | Equality s t a b = forall p. IsEquality p => p a b -> p s t
28 |
29 | ||| An `Equality' s a` is a witness that `s = a` that can be used as an optic.
30 | ||| This is the `Simple` version of `Equality`.
31 | public export
32 | 0 Equality' : (s,a : k) -> Type
33 | Equality' = Simple Equality
34 |
35 |
36 | ------------------------------------------------------------------------------
37 | -- Utilities for Equality
38 | ------------------------------------------------------------------------------
39 |
40 |
41 | ||| Extract the two `Equal` values from an `Equality`.
42 | public export
43 | runEq : Equality s t a b -> (s = a, t = b)
44 | runEq l = (l {p = \x,_ => x = a} Refl,
45 |            l {p = \_,y => y = b} Refl)
46 |
47 | ||| Extract an `Equal` value from an `Equality`.
48 | public export
49 | runEq' : Equality s t a b -> s = a
50 | runEq' l = l {p = \x,_ => x = a} Refl
51 |
52 |
53 | ||| `Equality` is a congruence.
54 | public export
55 | congEq : forall f,g. Equality s t a b -> Equality (f s) (g t) (f a) (g b)
56 | congEq l {p} = l {p = \x,y => p (f x) (g y)}
57 |
58 | ||| Symmetry of an `Equality` optic.
59 | public export
60 | symEq : Equality s t a b -> Equality b a t s
61 | symEq l = case runEq l of (Refl, Refl) => id
62 |
63 | public export
64 | substEq : forall p. Equality s t a b -> p a b a b -> p s t a b
65 | substEq {p} l = l {p = \x,y => p x y a b}
66 |
67 |
68 | ||| The trivial `Simple Equality`.
69 | ||| Composing this optic with any other can force it to be a `Simple` optic.
70 | public export
71 | simple : Equality' a a
72 | simple = id
73 |