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.Diff
 5 |
 6 | import Data.Linear
 7 | import Data.Linear.Inverse
 8 | import Data.Linear.LEither
 9 |
10 | %default total
11 |
12 | public export
13 | Quadruple : Type -> Type
14 | Quadruple a = LPair a (LPair a (LPair a a))
15 |
16 | -- Differentiating a⁴ wrt a gives us 4a³
17 | data QuadContexts : Type -> Type where
18 |   Mk1 : (1    y, z, w : a) -> QuadContexts a
19 |   Mk2 : (1 x,    z, w : a) -> QuadContexts a
20 |   Mk3 : (1 x, y,    w : a) -> QuadContexts a
21 |   Mk4 : (1 x, y, z    : a) -> QuadContexts a
22 |
23 | -- Differentiating a⁴ wrt a² gives us 4a³ * (2a)⁻¹
24 | data QuadTwoContexts : Type -> Type where
25 |   Mk : QuadContexts a -@ Inverse (LEither a a) -@ QuadTwoContexts a
26 |
27 | -- Consume the element next to the hole such that the 2-hole
28 | -- does not separate the remaining values of the original tuple
29 | fromContext : LPair a a -@ QuadTwoContexts a -@ Quadruple a
30 | fromContext (h1 # h2) (Mk (Mk1 y z w) inv)
31 |   = (Right y `divide` inv) `seq` (h1 # h2 # z # w)
32 | fromContext (h1 # h2) (Mk (Mk2 x z w) inv)
33 |   = (Left x `divide` inv) `seq` (h1 # h2 # z # w)
34 | fromContext (h1 # h2) (Mk (Mk3 x y w) inv)
35 |   = (Right w `divide` inv) `seq` (x # y # h1 # h2)
36 | fromContext (h1 # h2) (Mk (Mk4 x y z) inv)
37 |   = (Left z `divide` inv) `seq` (x # y # h1 # h2)
38 |
39 | -- The current hole in QuadTwoContexts is understood to be the
40 | -- 2nd one placeholder for the fillers.
41 | -- Always consume the element to the left of it to fit the 2-hole
42 | -- (if none then throw the left hole away)
43 | fromContext' : LPair a a -@ QuadTwoContexts a -@ Quadruple a
44 | fromContext' (h1 # h2) (Mk (Mk1 y z w) inv)
45 |   -- first hole outside of the tuple
46 |   = (Left h1 `divide` inv) `seq` (h2 # y # z # w)
47 | fromContext' (h1 # h2) (Mk (Mk2 x z w) inv)
48 |   -- 2-hole at the start of the tuple
49 |   = (Left x `divide` inv) `seq` (h1 # h2 # z # w)
50 | fromContext' (h1 # h2) (Mk (Mk3 x y w) inv)
51 |   -- 2-hole in the middle of the tuple
52 |   = (Left y `divide` inv) `seq` (x # h1 # h2 # w)
53 | fromContext' (h1 # h2) (Mk (Mk4 x y z) inv)
54 |   -- 2-hole at the end of the tuple
55 |   = (Left z `divide` inv) `seq` (x # y # h1 # h2)
56 |