idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-11-24 06:52:19 +03:00
Code Issues Projects Releases Wiki Activity

[ new ] Applicative and Monad for Pair (#1188)

Browse Source
This commit is contained in:
Stefan Höck 2021-03-15 14:42:04 +01:00 committed by GitHub
parent f4a790ded4
commit 1784593abb
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
2 changed files with 12 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

11
libs/prelude/Prelude/Types.idr
View File

@ -107,6 +107,17 @@ public export
Functor (Pair a) where Functor (Pair a) where
map = mapSnd map = mapSnd
%inline
public export
Monoid a => Applicative (Pair a) where
pure = (neutral,)
(a1,f) <*> (a2,v) = (a1 <+> a2, f v)
%inline
public export
Monoid a => Monad (Pair a) where
(a1,a) >>= f = let (a2,b) = f a in (a1 <+> a2, b)
----------- -----------
-- MAYBE -- -- MAYBE --
----------- -----------

1
tests/idris2/docs001/expected
View File

@ -76,6 +76,7 @@ join : m (m a) -> m a
Implementations: Implementations:
Monad IO Monad IO
Monoid a => Monad (Pair a)
Monad Maybe Monad Maybe
Monad (Either e) Monad (Either e)
Monad List Monad List