0 | module Data.Linear.Copies
 1 |
 2 | import Data.Linear.Bifunctor
 3 | import Data.Linear.Notation
 4 | import Data.Nat
 5 |
 6 | %default total
 7 |
 8 | export infix 1 `Copies`
 9 |
10 | ||| Carries multiple linear copies of the same value. Usage: m `Copies` x
11 | ||| reads as "m copies of value x". This data structure is necessary to implement
12 | ||| algorithms that rely on linearity but also interact with Nat indicies, like
13 | ||| Vect and Fin.
14 | ||| This data structure can be found in the paper "How to Take the Inverse of a Type" by
15 | ||| Daniel Marshall and Dominic Orchard where it's described as an exponent operator
16 | public export
17 | data Copies : Nat -> (0 x : a) -> Type where
18 |   Nil : Copies Z x
19 |   (::) : (1 x : a) -> (1 copies : Copies n x) -> Copies (S n) x
20 |
21 | ||| Split copies into two
22 | export
23 | splitAt : (1 m : Nat) -> Copies (m + n) x -@ LPair (Copies m x) (Copies n x)
24 | splitAt Z xs = ([] # xs)
25 | splitAt (S m) (x :: xs) = let (ys # zs) = splitAt m xs in (x :: ys # zs)
26 |
27 | ||| Combine multiple copies into one
28 | export
29 | (++) : Copies m x -@ Copies n x -@ Copies (m + n) x
30 | [] ++ ys = ys
31 | (x :: xs) ++ ys = x :: (xs ++ ys)
32 |
33 | ||| Copies of pairs are like pairs of copies
34 | export
35 | unzip : Copies m (Builtin.(#) x y) -@ LPair (Copies m x) (Copies m y)
36 | unzip [] = [] # []
37 | unzip ((x # y) :: xys) = let (xs # ys) = unzip xys in (x :: xs # y :: ys)
38 |
39 | -- Copies is a bit of an applicative
40 | export
41 | pure : {1 n : Nat} -> (x : a) -> Copies n x
42 | pure {n = Z} x = []
43 | pure {n = S n} x = x :: pure x
44 |
45 | ||| Applies m copies of a linear function to m arguments, resulting in m copies
46 | ||| of the result.
47 | export
48 | (<*>) : Copies {a = a -@ b} m f -@ Copies m x -@ Copies m (f x)
49 | [] <*> [] = []
50 | (f :: fs) <*> (x :: xs) = f x :: (fs <*> xs)
51 |
52 | ||| Apply f to `m` copies of `x`, resulting in `m` copies of `f x`.
53 | |||
54 | ||| Note that this is not quite `pure f <*> xs` because we don't actually
55 | ||| need to know `m` to be able to define `(<$>)` as we can proceed by
56 | ||| induction on xs.
57 | export
58 | (<$>) : (f : a -@ b) -> Copies m x -@ Copies m (f x)
59 | f <$> [] = []
60 | f <$> (x :: xs) = f x :: (f <$> xs)
61 |
62 | ||| Combine copies of two values into a pair of copies
63 | export
64 | zip : Copies m x -@ Copies m y -@ Copies m (Builtin.(#) x y)
65 | zip as bs = (#) <$> as <*> bs
66 |
67 | ||| If we have a single copy, we can extract its value
68 | export
69 | extract : {0 x : a} -> 1 `Copies` x -@ a
70 | extract [x] = x
71 |
72 | ||| Extract 2 copies into a linear pair
73 | export
74 | pair : {0 x : a} -> 2 `Copies` x -@ LPair a a
75 | pair y = bimap extract extract (splitAt 1 y)
76 |