0 | ||| A module defining the `DEq` interface
  1 | module Data.DEq
  2 |
  3 | import Data.Maybe
  4 |
  5 | -------------------------------------------------------------------------------
  6 | -- (=?)
  7 | -------------------------------------------------------------------------------
  8 | export infix 1 =?
  9 | public export
 10 | (=?) : t -> t -> Type
 11 | a =? b = Maybe (a = b)
 12 |
 13 | ||| Takes a function and an optional proof of the equality between two values
 14 | ||| and returns a proof of the equality between the results of that function
 15 | ||| applied to these values
 16 | |||
 17 | ||| @ f   the function
 18 | ||| @ x y the values
 19 | ||| @ prf the potential proof of `x = y`
 20 | export
 21 | mcong : (0 f : a -> b) -> {0 x, y : a} -> (prf : x =? y) -> f x =? f y
 22 | -- A "kosher" definition of `mcong would be this:
 23 | -- ```
 24 | -- mcong f Nothing     = Nothing
 25 | -- mcong f (Just Refl) = Just Refl
 26 | -- ```
 27 | -- but, for performance resons, I will skip the pattern matching and use
 28 | -- `believe_me` since the values are indistinguishible runtime-wise.
 29 | --
 30 | -- This should be dafinable with the `cong` function
 31 | -- (`mcong f prf = map (cong f) prf`)
 32 | -- but I cannot figure out why it doesn't type check.
 33 | mcong f prf = believe_me prf
 34 |
 35 | ||| Like `mcong` but the function is implicit
 36 | export
 37 | mcong' : {0 f : a -> b} -> {0 x, y : a} -> (prf : x =? y) -> f x =? f y
 38 | mcong' {f} prf = mcong f prf
 39 |
 40 | ||| When the condition holds, return the (optional) equality proof
 41 | ||| @ meq  the (optional) equality proof
 42 | ||| @ cond the condition
 43 | export
 44 | when : (cond : Bool) -> (meq : a =? b) -> a =? b
 45 | when False _  = Nothing
 46 | when True meq = meq
 47 |
 48 | ||| Returns the (optional) equality, but only when the condition holds
 49 | ||| @ meq  the (optional) equality proof
 50 | ||| @ cond the condition
 51 | export
 52 | butOnlyWhen : (meq : a =? b) -> (cond : Bool) -> a =? b
 53 | butOnlyWhen = flip when
 54 |
 55 | export
 56 | and
 57 |    : {0 a, b   : t}
 58 |   -> {0 aa, bb : tt}
 59 |   -> {0 f      : t -> tt -> ttt}
 60 |   -> (lhs      : a      =? b)
 61 |   -> (rhs      : aa     =? bb)
 62 |   ->             f a aa =? f b bb
 63 | and _ Nothing = Nothing
 64 | and Nothing _ = Nothing
 65 | and (Just Refl) (Just Refl) = Just Refl
 66 |
 67 | -------------------------------------------------------------------------------
 68 | -- PEq, DEq interfaces
 69 | -------------------------------------------------------------------------------
 70 | ||| Similar to `Eq` but the comparison operator returns a proof that the
 71 | ||| operands are equal (in the case where they are)
 72 | |||
 73 | ||| The "P" in `PEq` stands for "proof"
 74 | ||| Note, this is not the same as `EqP` from the "some" package from Hackage
 75 | public export
 76 | interface PEq a where
 77 |   ||| Returns a proof that the operands are equal when they are,
 78 |   ||| otherwise, returns `Nothing`
 79 |   peq : (x, y : a) -> x =? y
 80 |
 81 | ||| Constructors of types that allow for deciding the equality between values
 82 | ||| of such types, even in the case when their types are constructed from
 83 | ||| different parameters
 84 | |||
 85 | ||| Modeled after the `GEq` typeclass from Haskells "some" package
 86 | |||
 87 | ||| @ f the type constructor
 88 | ||| @ t the parameter type
 89 | public export
 90 | interface DEq (0 f : t -> Type) where
 91 |   ||| If the operands are equal, returns a proof, that their type parameters
 92 |   ||| are equal
 93 |   deq : f a -> f b -> (a =? b)
 94 |
 95 | ||| Compare the operands and ignore the equality proof
 96 | export
 97 | deq' : (impl : DEq f) => f a -> f b -> Bool
 98 | deq' fa fb = isJust (deq fa fb @{impl})
 99 |
100 | ||| Decide the inequality of the operands
101 | export
102 | ngeq' : (impl : DEq f) => f a -> f b -> Bool
103 | ngeq' fa fb = not (deq' fa fb @{impl})
104 |
105 | -------------------------------------------------------------------------------
106 | -- PEq implementations
107 | -------------------------------------------------------------------------------
108 | ||| Use only when absolutely sure that `x == y` returns `True` only when `x`
109 | ||| and `y` are identical.
110 | export
111 | implementation [unsafeViaEq] Eq a => PEq a where
112 |   x `peq` y = Just (believe_me $ the (x = x) Refl) `butOnlyWhen` x == y
113 |
114 | export
115 | implementation PEq Bool where
116 |   peq x y = peq x y @{unsafeViaEq}
117 |
118 | export
119 | implementation PEq Nat where
120 |   peq x y = peq x y @{unsafeViaEq}
121 |
122 |   -- A "kosher" definition:
123 |   -- peq : (n1, n2 : Nat) -> Maybe (n1 = n2)
124 |   -- peq Z Z = Just Refl
125 |   -- peq (S n) (S n') = mcong S (peq n n')
126 |   -- peq _ _ = Nothing
127 |
128 | export
129 | implementation PEq Int where
130 |   peq x y = peq x y @{unsafeViaEq}
131 |
132 | export
133 | implementation PEq Integer where
134 |   peq x y = peq x y @{unsafeViaEq}
135 |
136 | export
137 | implementation PEq Char where
138 |   peq x y = peq x y @{unsafeViaEq}
139 |
140 | export
141 | implementation PEq String where
142 |   peq x y = peq x y @{unsafeViaEq}
143 |
144 | export
145 | implementation PEq a => PEq (List a) where
146 |   peq Nil Nil = Just Refl
147 |   peq (x :: xs) (y :: ys) = (peq x y `and` peq xs ys) {f = (::)}
148 |   peq _ _ = Nothing
149 |
150 | export
151 | implementation PEq a => PEq b => PEq (a, b) where
152 |   peq (a1, b1) (a2, b2) = (peq a1 a2 `and` peq b1 b2) {f = (,)}
153 |