git.iko.soy/Idris-dev
on master help sign in
Add Functor, Applicative and Monad instances for (Vect n)
8a53e68Melvar Chen
lib/Prelude.idr+8
compare with master
unifiedsplit
@@ -216,6 +216,11 @@ instance Applicative List where
216
216
217 fs <$> vs = concatMap (\f => map f vs) fs
217 fs <$> vs = concatMap (\f => map f vs) fs
218
218
219+instance Applicative (Vect k) where
220+ pure = replicate _
221+
222+ fs <$> vs = zipWith ($) fs vs
223+
219---- Alternative instances
224---- Alternative instances
220
225
221instance Alternative Maybe where
226instance Alternative Maybe where
@@ -245,6 +250,9 @@ instance Monad (Either e) where
245instance Monad List where
250instance Monad List where
246 m >>= f = concatMap f m
251 m >>= f = concatMap f m
247
252
253+instance Monad (Vect n) where
254+ m >>= f = diag (map f m)
255+
248---- some mathematical operations
256---- some mathematical operations
249
257
250%include C "math.h"
258%include C "math.h"
lib/Prelude/Vect.idr+9−5
@@ -104,9 +104,9 @@ unzip ((l, r)::xs) with (unzip xs)
104-- Maps
104-- Maps
105--------------------------------------------------------------------------------
105--------------------------------------------------------------------------------
106
106
107−map : (a -> b) -> Vect n a -> Vect n b
107+instance Functor (Vect n) where
108−map f [] = []
108+ map f [] = []
109−map f (x::xs) = f x :: map f xs
109+ map f (x::xs) = f x :: map f xs
110
110
111-- XXX: causes Idris to enter an infinite loop when type checking in the REPL
111-- XXX: causes Idris to enter an infinite loop when type checking in the REPL
112--mapMaybe : (a -> Maybe b) -> Vect n a -> (p ** Vect b p)
112--mapMaybe : (a -> Maybe b) -> Vect n a -> (p ** Vect b p)
@@ -145,10 +145,10 @@ total or : Vect m Bool -> Bool
145or = foldr (||) False
145or = foldr (||) False
146
146
147total any : (a -> Bool) -> Vect m a -> Bool
147total any : (a -> Bool) -> Vect m a -> Bool
148−any p = Vect.or . Vect.map p
148+any p = Vect.or . map p
149
149
150total all : (a -> Bool) -> Vect m a -> Bool
150total all : (a -> Bool) -> Vect m a -> Bool
151−all p = Vect.and . Vect.map p
151+all p = Vect.and . map p
152
152
153--------------------------------------------------------------------------------
153--------------------------------------------------------------------------------
154-- Transformations
154-- Transformations
@@ -317,6 +317,10 @@ catMaybes (Nothing::xs) = catMaybes xs
317catMaybes ((Just j)::xs) with (catMaybes xs)
317catMaybes ((Just j)::xs) with (catMaybes xs)
318 | (_ ** tail) = (_ ** j::tail)
318 | (_ ** tail) = (_ ** j::tail)
319
319
320+diag : Vect n (Vect n a) -> Vect n a
321+diag [] = []
322+diag ((x::xs)::xss) = x :: diag (map tail xss)
323+
320range : Vect n (Fin n)
324range : Vect n (Fin n)
321range =
325range =
322 reverse range_
326 reverse range_