30 | import Data.List.Elem
35 | data Literal : Shape -> Type -> Type where
36 | Scalar : a -> Literal [] a
37 | Nil : Literal (0 :: ds) a
38 | (::) : Literal ds a -> Literal (d :: ds) a -> Literal (S d :: ds) a
41 | fromInteger : Num a => Integer -> Literal [] a
42 | fromInteger = Scalar . fromInteger
45 | fromDouble : Double -> Literal [] Double
50 | True, False : Literal [] Bool
52 | False = Scalar False
55 | Functor (Literal shape) where
56 | map f (Scalar x) = Scalar (f x)
58 | map f (x :: xs) = map f x :: map f xs
60 | functorIdentity : (xs : Literal shape a) -> map Prelude.id xs = xs
61 | functorIdentity (Scalar _) = Refl
62 | functorIdentity [] = Refl
63 | functorIdentity (x :: xs) = cong2 (::) (functorIdentity x) (functorIdentity xs)
65 | functorComposition :
66 | (xs : Literal shape a) -> (f : a -> b) -> (g : b -> c) -> map (g . f) xs = map g (map f xs)
67 | functorComposition (Scalar _) _ _ = Refl
68 | functorComposition [] _ _ = Refl
69 | functorComposition (x :: xs) f g =
70 | cong2 (::) (functorComposition x f g) (functorComposition xs f g)
73 | {shape : _} -> Applicative (Literal shape) where
74 | pure x = case shape of
77 | (S d :: ds) => pure x :: assert_total (pure x)
79 | (Scalar f) <*> (Scalar x) = Scalar (f x)
81 | (f :: fs) <*> (x :: xs) = (f <*> x) :: (fs <*> xs)
83 | applicativeIdentity : (xs : Literal shape a) -> pure Prelude.id <*> xs = xs
84 | applicativeIdentity (Scalar _) = Refl
85 | applicativeIdentity [] = Refl
86 | applicativeIdentity (x :: xs) = cong2 (::) (applicativeIdentity x) (applicativeIdentity xs)
88 | applicativeHomomorphism :
89 | (shape : Shape) -> (f : a -> b) -> (x : a) -> pure f <*> pure x = pure {f = Literal shape} (f x)
90 | applicativeHomomorphism [] _ _ = Refl
91 | applicativeHomomorphism (d :: ds) f x = forCons d ds f x
98 | pure f <*> pure x = pure {f = Literal (d :: ds)} (f x)
99 | forCons 0 _ _ _ = Refl
100 | forCons (S d) ds f x = cong2 (::) (applicativeHomomorphism ds f x) (forCons d ds f x)
102 | applicativeInterchange :
103 | (fs : Literal shape (a -> b)) -> (x : a) -> fs <*> pure x = pure ($
x) <*> fs
104 | applicativeInterchange (Scalar _) _ = Refl
105 | applicativeInterchange [] _ = Refl
106 | applicativeInterchange (f :: fs) x =
107 | cong2 (::) (applicativeInterchange f x) (applicativeInterchange fs x)
109 | applicativeComposition :
110 | (xs : Literal shape a) ->
111 | (fs : Literal shape (a -> b)) ->
112 | (gs : Literal shape (b -> c)) ->
113 | pure (.) <*> gs <*> fs <*> xs = gs <*> (fs <*> xs)
114 | applicativeComposition (Scalar _) (Scalar _) (Scalar _) = Refl
115 | applicativeComposition [] [] [] = Refl
116 | applicativeComposition (x :: xs) (f :: fs) (g :: gs) =
117 | cong2 (::) (applicativeComposition x f g) (applicativeComposition xs fs gs)
120 | Foldable (Literal shape) where
121 | foldr f acc (Scalar x) = f x acc
122 | foldr _ acc [] = acc
123 | foldr f acc (x :: xs) = foldr f (foldr f acc xs) x
126 | Traversable (Literal shape) where
127 | traverse f (Scalar x) = [| Scalar (f x) |]
128 | traverse f [] = pure []
129 | traverse f (x :: xs) = [| traverse f x :: traverse f xs |]
132 | Zippable (Literal shape) where
133 | zipWith f (Scalar x) (Scalar y) = Scalar (f x y)
134 | zipWith _ [] [] = []
135 | zipWith f (x :: xs) (y :: ys) = zipWith f x y :: zipWith f xs ys
137 | zipWith3 f (Scalar x) (Scalar y) (Scalar z) = Scalar (f x y z)
138 | zipWith3 _ [] [] [] = []
139 | zipWith3 f (x :: xs) (y :: ys) (z :: zs) = zipWith3 f x y z :: zipWith3 f xs ys zs
141 | unzipWith f (Scalar x) = let (x, y) = f x in (Scalar x, Scalar y)
142 | unzipWith _ [] = ([], [])
143 | unzipWith f (x :: xs) =
144 | let (x, y) = unzipWith f x
145 | (xs, ys) = unzipWith f xs
146 | in (x :: xs, y :: ys)
148 | unzipWith3 f (Scalar x) = let (x, y, z) = f x in (Scalar x, Scalar y, Scalar z)
149 | unzipWith3 _ [] = ([], [], [])
150 | unzipWith3 f (x :: xs) =
151 | let (x, y, z) = unzipWith3 f x
152 | (xs, ys, zs) = unzipWith3 f xs
153 | in (x :: xs, y :: ys, z :: zs)
157 | all : Literal shape Bool -> Bool
158 | all xs = foldr (\x, y => x && y) True xs
161 | Num a => Num (Literal [] a) where
162 | x + y = [| x + y |]
163 | x * y = [| x * y |]
164 | fromInteger = Scalar . fromInteger
167 | negate : Neg a => Literal shape a -> Literal shape a
168 | negate = map negate
171 | Eq a => Eq (Literal shape a) where
172 | x == y = all (zipWith (==) x y)
174 | toVect : Literal (d :: ds) a -> Vect d (Literal ds a)
176 | toVect (x :: y) = x :: toVect y
180 | {shape : _} -> Show a => Show (Literal shape a) where
181 | show = showWithIndent "" where
182 | showWithIndent : {shape : _} -> String -> Literal shape a -> String
183 | showWithIndent _ (Scalar x) = show x
184 | showWithIndent _ [] = "[]"
185 | showWithIndent {shape = [S _]} _ x = show (toList x)
186 | showWithIndent {shape = (S d :: dd :: ddd)} indent (x :: xs) =
187 | let indent = " " ++ indent
188 | first = showWithIndent indent x
189 | rest = foldMap (\e => ",\n" ++ indent ++ showWithIndent indent e) (toVect xs)
190 | in "[" ++ first ++ rest ++ "]"
193 | {shape : _} -> Cast (Array shape a) (Literal shape a) where
194 | cast x with (shape)
195 | cast x | [] = Scalar x
196 | cast _ | (0 :: _) = []
197 | cast (x :: xs) | (S d :: ds) = cast x :: cast xs
200 | [toArray] Cast (Literal shape a) (Array shape a) where
201 | cast (Scalar x) = x
203 | cast (x :: y) = cast @{toArray} x :: cast @{toArray} y
210 | data All : (0 p : a -> Type) -> Literal shape a -> Type where
211 | Scalar : forall x . p x -> All p (Scalar x)
213 | (::) : All p x -> All p xs -> All p (x :: xs)
221 | data All2 : (p : a -> b -> Type) -> Literal shape a -> Literal shape b -> Type where
222 | Scalar : forall a, b . p a b -> All2 p (Scalar a) (Scalar b)
224 | (::) : All2 p a b -> All2 p as bs -> All2 p (a :: as) (b :: bs)