on master help sign in
Merge branch 'master' of github.com:edwinb/Idris-dev
commit0458d81ef29a70e07213cc6e9330989c63a0e782 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSun 13 Jan 2013, 14:14 (14 years ago) parent17e40d2875eecc
1 file changed+16
lib/Prelude/Maybe.idr+16
lib/Prelude/Maybe.idr+16
@@ -2,6 +2,9 @@ module Prelude.Maybe
22
33import Builtins
44
5+%access public
6+%default total
7+
58data Maybe a
69 = Nothing
710 | Just a
@@ -41,3 +44,16 @@ toMaybe False j = Nothing
4144maybe_bind : Maybe a -> (a -> Maybe b) -> Maybe b
4245maybe_bind Nothing k = Nothing
4346maybe_bind (Just x) k = k x
47+
48+-- | Lift a semigroup into 'Maybe' forming a 'Monoid' according to
49+-- <http://en.wikipedia.org/wiki/Monoid>: \"Any semigroup S may be
50+-- turned into a monoid simply by adjoining an element e not in S
51+-- and defining i+i = i and i+s = s = s+i for all s ∈ S.\"
52+
53+instance (Semigroup a) => Semigroup (Maybe a) where
54+ Nothing <+> m = m
55+ m <+> Nothing = m
56+ Just m1 <+> Just m2 = Just (m1 <+> m2)
57+
58+instance (Monoid a) => Monoid (Maybe a) where
59+ neutral = Nothing