545550f · Idris-dev · git.iko.soy

lib/Prelude.idr+6

@@ -254,6 +254,12 @@ instance Monad List where

254instance Monad (Vect n) where

255 m >>= f = diag (map f m)

256

257+---- Traversable instances

258+

259+instance Traversable List where

260+ traverse f [] = pure List.Nil

261+ traverse f (x::xs) = [| List.(::) (f x) (traverse f xs) |]

262+

257---- some mathematical operations

263---- some mathematical operations

258

264

259%include C "math.h"

265%include C "math.h"

lib/Prelude/Applicative.idr−7

@@ -29,10 +29,3 @@ guard a = if a then pure () else empty

29

30when : Applicative f => Bool -> f () -> f ()

31when a f = if a then f else pure ()

32−

33−sequence : Applicative f => List (f a) -> f (List a)

34−sequence [] = pure []

35−sequence (x :: xs) = map (::) x <$> sequence xs

36−

37−traverse : Applicative f => (a -> f b) -> List a -> f (List b)

38−traverse f xs = sequence (map f xs)

lib/Prelude/Traversable.idr+5

@@ -9,3 +9,8 @@ traverse_ f = foldr (($>) . f) (pure ())

9sequence_ : (Foldable t, Applicative f) => t (f a) -> f ()

10sequence_ = foldr ($>) (pure ())

11

12+class (Functor t, Foldable t) => Traversable (t : Type -> Type) where

13+ traverse : Applicative f => (a -> f b) -> t a -> f (t b)

14+

15+sequence : (Traversable t, Applicative f) => t (f a) -> f (t a)

16+sequence = traverse id