0 | ||| This module is based on the content of the functional pearl
  1 | ||| How to Take the Inverse of a Type
  2 | ||| by Daniel Marshall and Dominic Orchard
  3 |
  4 | module Data.Linear.Inverse
  5 |
  6 | import Data.INTEGER
  7 |
  8 | import Data.Linear
  9 | import Data.Linear.LEither
 10 | import Data.Linear.LMaybe
 11 | import Data.Linear.LVect
 12 |
 13 | import Data.Nat
 14 |
 15 | import Syntax.PreorderReasoning
 16 |
 17 | %default total
 18 |
 19 | ||| Inverse is a shorthand for 'multiplicative skew inverse'
 20 | export
 21 | Inverse : Type -> Type
 22 | Inverse a = a -@ ()
 23 |
 24 | export
 25 | mkInverse : (a -@ ()) -@ Inverse a
 26 | mkInverse f = f
 27 |
 28 | ||| And this is the morphism witnessing the multiplicative skew inverse
 29 | export
 30 | divide : a -@ Inverse a -@ ()
 31 | divide x u = u x
 32 |
 33 | export
 34 | doubleNegation : a -@ Inverse (Inverse a)
 35 | doubleNegation = divide
 36 |
 37 | ||| We only use the inverse of a if the LMaybe is actually Just.m
 38 | export
 39 | maybeNeg : LMaybe a -@ Inverse a -@ LMaybe (Inverse a)
 40 | maybeNeg Nothing u = Just u
 41 | maybeNeg (Just n) u = divide n u `seq` Nothing
 42 |
 43 | public export
 44 | lid : a -@ a
 45 | lid x = x
 46 |
 47 | public export
 48 | lcompose : (b -@ c) -@ (a -@ b) -@ (a -@ c)
 49 | lcompose g f = \ 1 x => g (f x)
 50 |
 51 | public export
 52 | comap : (b -@ a) -@ Inverse a -@ Inverse b
 53 | comap f u = lcompose u f
 54 |
 55 | export
 56 | comapId : (u : Inverse a) -> Inverse.comap Inverse.lid u === Inverse.lid u
 57 | comapId u = Refl
 58 |
 59 | export
 60 | comapComp : (u : Inverse a) ->
 61 |   Inverse.comap (lcompose g f) u
 62 |   === lcompose (Inverse.comap f) (Inverse.comap g) u
 63 | comapComp u = Refl
 64 |
 65 | export
 66 | munit : () -@ Inverse ()
 67 | munit u = u `seq` lid
 68 |
 69 | export
 70 | mmult : Inverse a -@ Inverse b -@ Inverse (LPair a b)
 71 | mmult ua ub (a # b) = divide a ua `seq` divide b ub
 72 |
 73 | public export
 74 | Pow : Type -> INTEGER -> Type
 75 | Pow a Z = ()
 76 | Pow a (PS n) = LVect (S n) a
 77 | Pow a (NS n) = LVect (S n) (Inverse a)
 78 |
 79 | public export
 80 | zip : {n : INTEGER} -> Pow a n -@ Pow b n -@ Pow (LPair a b) n
 81 | zip {n = Z} as bs = as `seq` bs
 82 | zip {n = (PS k)} as bs = zip as bs
 83 | zip {n = (NS k)} as bs = mmult <$> as <*> bs
 84 |
 85 | export
 86 | powPositiveL : (m, n : Nat) -> Pow a (cast $ m + n) -@
 87 |                LPair (Pow a (cast m)) (Pow a (cast n))
 88 | powPositiveL Z n as = (() # as)
 89 | powPositiveL 1 Z [a] = ([a] # ())
 90 | powPositiveL 1 (S n) (a :: as) = ([a] # as)
 91 | powPositiveL (S m@(S _)) n (a :: as)
 92 |   = let (xs # ys) = powPositiveL m n as in (a :: xs # ys)
 93 |
 94 | export
 95 | powPositiveR : (m, n : Nat) -> Pow a (cast m) -@ Pow a (cast n) -@
 96 |            Pow a (cast $ m + n)
 97 | powPositiveR 0 n xs ys = xs `seq` ys
 98 | powPositiveR 1 0 xs ys = ys `seq` xs
 99 | powPositiveR 1 (S n) [a] ys = a :: ys
100 | powPositiveR (S m@(S _)) n (x :: xs) ys = x :: powPositiveR m n xs ys
101 |
102 | export
103 | powNegateL : (m : Nat) -> Pow a (- cast m) -> Pow (Inverse a) (cast m)
104 | powNegateL Z as = as
105 | powNegateL (S m) as = as
106 |
107 | export
108 | powNegateR : (m : Nat) -> Pow (Inverse a) (cast m) -> Pow a (- cast m)
109 | powNegateR Z as = as
110 | powNegateR (S m) as = as
111 |
112 | export
113 | powNegativeL : (m, n : Nat) -> Pow a (- cast (m + n)) -@
114 |             LPair (Pow a (- cast m)) (Pow a (- cast n))
115 | powNegativeL Z n as = (() # as)
116 | powNegativeL 1 Z [a] = ([a] # ())
117 | powNegativeL 1 (S n) (a :: as) = ([a] # as)
118 | powNegativeL (S m@(S _)) n (a :: as)
119 |   = let (xs # ys) = powNegativeL m n as in (a :: xs # ys)
120 |
121 | export
122 | powNegativeR : (m, n : Nat) -> Pow a (- cast m) -@ Pow a (- cast n) -@
123 |            Pow a (- cast (m + n))
124 | powNegativeR 0 n xs ys = xs `seq` ys
125 | powNegativeR 1 0 xs ys = ys `seq` xs
126 | powNegativeR 1 (S n) [a] ys = a :: ys
127 | powNegativeR (S m@(S _)) n (x :: xs) ys = x :: powNegativeR m n xs ys
128 |
129 | export
130 | powAnnihilate : (m : Nat) -> Pow a (cast m) -@ Pow a (- cast m) -@ ()
131 | powAnnihilate 0         pos neg = pos `seq` neg
132 | powAnnihilate 1         [x] [u] = u x
133 | powAnnihilate (S (S k)) (x :: pos) (u :: neg)
134 |   = u x `seq` powAnnihilate (S k) pos neg
135 |
136 | powMinusAux : (m, n : Nat) -> CmpNat m n ->
137 |   Pow a (cast m) -@ Pow a (- cast n) -@ Pow a (cast m - cast n)
138 | powMinusAux m (m + S n) (CmpLT n) pos neg
139 |   = let (neg1 # neg2) = powNegativeL m (S n) neg in
140 |     powAnnihilate m pos neg1 `seq` replace {p = Pow a} eq neg2
141 |
142 |   where
143 |
144 |   eq : NS n === cast m - cast (m + S n)
145 |   eq = sym $ Calc $
146 |      |~ cast m - cast (m + S n)
147 |      ~~ cast m - (cast m + cast (S n))
148 |         ...( cong (cast m -) (castPlus m (S n)) )
149 |      ~~ cast m + (- cast m - cast (S n))
150 |         ...( cong (cast m +) (negatePlus (cast m) (cast (S n))) )
151 |      ~~ (cast m - cast m) - cast (S n)
152 |         ...( plusAssociative (cast m) (- cast m) (- cast (S n)) )
153 |      ~~ - cast (S n)
154 |         ...( cong (+ - cast (S n)) (plusInverse (cast m)) )
155 |
156 | powMinusAux m m CmpEQ pos neg
157 |   = rewrite plusInverse (cast m) in
158 |     powAnnihilate (cast m) pos neg
159 | powMinusAux (_ + S m) n (CmpGT m) pos neg
160 |   = let (pos1 # pos2) = powPositiveL n (S m) pos in
161 |     powAnnihilate n pos1 neg `seq` replace {p = Pow a} eq pos2
162 |
163 |   where
164 |
165 |   eq : PS m === cast (n + S m) - cast n
166 |   eq = sym $ Calc $
167 |     |~ cast (n + S m) - cast n
168 |     ~~ cast n + cast (S m) - cast n
169 |       ...( cong (+ - cast n) (castPlus n (S m)) )
170 |     ~~ cast n + (cast (S m) - cast n)
171 |       ...( sym (plusAssociative (cast n) (cast (S m)) (- cast n)) )
172 |     ~~ cast n + (- cast n + cast (S m))
173 |       ...( cong (cast n +) (plusCommutative (cast (S m)) (- cast n)) )
174 |     ~~ (cast n - cast n) + cast (S m)
175 |       ...( plusAssociative (cast n) (- cast n) (cast (S m)) )
176 |     ~~ cast (S m)
177 |       ...( cong (+ cast (S m)) (plusInverse (cast n)) )
178 |
179 | export
180 | powMinus : (m, n : Nat) ->
181 |   Pow a (cast m) -@ Pow a (- cast n) -@ Pow a (cast m - cast n)
182 | powMinus m n = powMinusAux m n (cmp m n)
183 |