Add Traversable and instance for List
commit545550fdb386527301d0efe0e46eb2b852a0410b
authorMelvar Chen <Melvar.Chen@googlemail.com>
dateSun 4 Aug 2013, 02:28 (13 years ago)
parentac1c15b
lib/Prelude.idr+6
@@ -254,6 +254,12 @@ instance Monad List where
254254instance Monad (Vect n) where
255255 m >>= f = diag (map f m)
256256
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+
257263---- some mathematical operations
258264
259265%include C "math.h"
lib/Prelude/Applicative.idr−7
@@ -29,10 +29,3 @@ guard a = if a then pure () else empty
2929
3030when : Applicative f => Bool -> f () -> f ()
3131when 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 ())
99sequence_ : (Foldable t, Applicative f) => t (f a) -> f ()
1010sequence_ = foldr ($>) (pure ())
1111
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