@@ -42,6 +42,12 @@ toMaybe False j = Nothing
42justInjective : {x : t} -> {y : t} -> (Just x = Just y) -> x = y
42justInjective : {x : t} -> {y : t} -> (Just x = Just y) -> x = y
43justInjective refl = refl
43justInjective refl = refl
45+lowerMaybe : Monoid a => Maybe a -> a
46+lowerMaybe Nothing = neutral
47+lowerMaybe (Just x) = x
49+raiseToMaybe : (Monoid a, Eq a) => a -> Maybe a
50+raiseToMaybe x = if x == neutral then Nothing else Just x
46--------------------------------------------------------------------------------
52--------------------------------------------------------------------------------
47-- Class instances
53-- Class instances
@@ -58,22 +64,20 @@ instance (Eq a) => Eq (Maybe a) where
58 (Just a) == (Just b) = a == b
64 (Just a) == (Just b) = a == b
60-- | Lift a semigroup into 'Maybe' forming a 'Monoid' according to
66-- | Lift a semigroup into 'Maybe' forming a 'Monoid' according to
61−-- <http://en.wikipedia.org/wiki/Monoid>: \"Any semigroup S may be
67+-- <http://en.wikipedia.org/wiki/Monoid>: "Any semigroup S may be
62−-- turned into a monoid simply by adjoining an element e not in S
68+-- turned into a monoid simply by adjoining an element i not in S
63−-- and defining i+i = i and i+s = s = s+i for all s ∈ S.\"
69+-- and defining i+i = i and i+s = s = s+i for all s ∈ S."
65instance (Semigroup a) => Semigroup (Maybe a) where
71instance (Semigroup a) => Semigroup (Maybe a) where
66 Nothing <+> m = m
72 Nothing <+> m = m
67 m <+> Nothing = m
73 m <+> Nothing = m
68 (Just m1) <+> (Just m2) = Just (m1 <+> m2)
74 (Just m1) <+> (Just m2) = Just (m1 <+> m2)
70−instance (Monoid a) => Monoid (Maybe a) where
76+instance (Semigroup a) => Monoid (Maybe a) where
71 neutral = Nothing
77 neutral = Nothing
74instance (Monoid a, Eq a) => Cast a (Maybe a) where
79instance (Monoid a, Eq a) => Cast a (Maybe a) where
75− cast x = if x == neutral then Nothing else Just x
80+ cast = raiseToMaybe
77instance (Monoid a) => Cast (Maybe a) a where
82instance (Monoid a) => Cast (Maybe a) a where
78− cast Nothing = neutral
83+ cast = lowerMaybe