git.iko.soy/Idris-dev
on master help sign in
mtimes, stimes, and Monoid for Iso
f35d483howtonotwin
libs/base/Control/Isomorphism.idr+6
compare with master
unifiedsplit
@@ -37,6 +37,12 @@ Category Iso where
37 id = isoRefl
37 id = isoRefl
38 (.) = flip isoTrans
38 (.) = flip isoTrans
39
39
40+Semigroup (Iso a a) where
41+ (<+>) = isoTrans
42+
43+Monoid (Iso a a) where
44+ neutral = isoRefl
45+
40||| Isomorphism is symmetric
46||| Isomorphism is symmetric
41isoSym : Iso a b -> Iso b a
47isoSym : Iso a b -> Iso b a
42isoSym (MkIso to from toFrom fromTo) = MkIso from to fromTo toFrom
48isoSym (MkIso to from toFrom fromTo) = MkIso from to fromTo toFrom
libs/contrib/Control/Algebra.idr+14
@@ -126,6 +126,20 @@ pow' : RingWithUnity a => a -> Nat -> a
126pow' _ Z = unity
126pow' _ Z = unity
127pow' x (S n) = x <.> pow' x n
127pow' x (S n) = x <.> pow' x n
128
128
129+-- TODO: This can be more efficient:
130+-- stimes 5 x = x <+> (x <+> (x <+> (x <+> x)))
131+-- = x <+> ((x <+> x) <+> (x <+> x))
132+-- = let y = x <+> x in x <+> (y <+> y)
133+-- 4 <+>s into 3 <+>
134+||| Combine `n` copies of a value with `<+>`
135+stimes : Semigroup a => (n : Nat) -> {auto prf : IsSucc n} -> a -> a
136+stimes (S Z) x = x
137+stimes (S (S k)) x = x <+> stimes (S k) x
138+
139+||| Like `stimes`, but accepting `Z` as argument.
140+mtimes : Monoid a => (n : Nat) -> a -> a
141+mtimes Z x = neutral
142+mtimes (S k) x = stimes (S k) x
129
143
130-- XXX todo:
144-- XXX todo:
131-- Structures where "abs" make sense.
145-- Structures where "abs" make sense.