5e1ef78 · Idris-dev · git.iko.soy

CHANGELOG+6

compare with master

unifiedsplit

@@ -8,6 +8,12 @@ New in 0.9.17:

8* Quasiquotation supports the generation of Language.Reflection.Raw terms

9 in addition to Language.Reflection.TT. Types are used for disambiguation,

10 defaulting to TT at the REPL.

11+* Library operators have been renamed for consistency with Haskell. In

12+ particular, Applicative.(<$>) is now Applicative.(<*>) and (<$>) is

13+ now an alias for Functor.map. Correspondingly, ($>) and (<$) have

14+ been renamed to (<*) and (*>). The cascading effects of this rename

15+ are that Algebra.(<*>) has been renamed to Algebra.(<.>) and

16+ Matrix.(<.>) is now Matrix.(<:>).

11

17

12New in 0.9.16:

18New in 0.9.16:

13--------------

19--------------

contribs/lib/SQLite3/Sqlite3.idr+1−1

@@ -48,7 +48,7 @@ instance Functor DB where

48

49instance Applicative DB where

50 pure = MkDB . return . Right

51− (MkDB f) <$> (MkDB x) = MkDB (do f' <- f

51+ (MkDB f) <*> (MkDB x) = MkDB (do f' <- f

52 case f' of

53 Left err => return (Left err)

54 Right op => x >>= (return . map op))

contribs/lib/SimpleParser/SimpleParser.idr+1−1

@@ -30,7 +30,7 @@ instance Functor Parser where

30

31instance Applicative Parser where

32 pure v = P (\inp => Right (v, inp))

33− a <$> b = P (\inp => do (f, rest) <- parse a inp

33+ a <*> b = P (\inp => do (f, rest) <- parse a inp

34 (x, rest') <- parse b rest

35 pure ((f x), rest'))

36

libs/base/Control/Arrow.idr+1−1

@@ -95,7 +95,7 @@ instance Arrow a => Functor (ArrowMonad a) where

95

96instance Arrow a => Applicative (ArrowMonad a) where

97 pure x = MkArrowMonad $ arrow $ \_ => x

98− (MkArrowMonad f) <$> (MkArrowMonad x) = MkArrowMonad $ f &&& x >>> arrow (uncurry id)

98+ (MkArrowMonad f) <*> (MkArrowMonad x) = MkArrowMonad $ f &&& x >>> arrow (uncurry id)

99

100instance ArrowApply a => Monad (ArrowMonad a) where

101 (MkArrowMonad m) >>= f =

libs/base/Control/IOExcept.idr+2−2

@@ -10,8 +10,8 @@ instance Functor (IOExcept e) where

10

11instance Applicative (IOExcept e) where

12 pure x = ioM (pure (pure x))

13− (ioM f) <$> (ioM a) = ioM (do f' <- f; a' <- a

13+ (ioM f) <*> (ioM a) = ioM (do f' <- f; a' <- a

14− return (f' <$> a'))

14+ return (f' <*> a'))

15

16instance Monad (IOExcept e) where

17 (ioM x) >>= k = ioM (do x' <- x;

libs/base/Control/Monad/Identity.idr+1−1

@@ -9,7 +9,7 @@ instance Functor Identity where

9instance Applicative Identity where

10 pure x = Id x

11

12− (Id f) <$> (Id g) = Id (f g)

12+ (Id f) <*> (Id g) = Id (f g)

13

14instance Monad Identity where

15 (Id x) >>= k = k x

libs/base/Control/Monad/RWS.idr+1−1

@@ -21,7 +21,7 @@ instance Monad m => Functor (RWST r w s m) where

21

22instance (Monoid w, Monad m) => Applicative (RWST r w s m) where

23 pure a = MkRWST $ \_,s => return (a, s, neutral)

24− (MkRWST f) <$> (MkRWST v) = MkRWST $ \r,s => do (a, s', w) <- v r s

24+ (MkRWST f) <*> (MkRWST v) = MkRWST $ \r,s => do (a, s', w) <- v r s

25 (fn, ss, w') <- f r s

26 return (fn a, ss, w <+> w)

27

libs/base/Control/Monad/Reader.idr+1−1

@@ -27,7 +27,7 @@ instance Functor f => Functor (ReaderT r f) where

27

28instance Applicative m => Applicative (ReaderT r m) where

29 pure = liftReaderT . pure

30− (RD f) <$> (RD v) = RD $ \r => f r <$> v r

30+ (RD f) <*> (RD v) = RD $ \r => f r <*> v r

31

32instance Alternative m => Alternative (ReaderT r m) where

33 empty = liftReaderT empty

libs/base/Control/Monad/State.idr+1−1

@@ -25,7 +25,7 @@ instance Functor f => Functor (StateT s f) where

25instance Monad f => Applicative (StateT s f) where

26 pure x = ST (\st => pure (x, st))

27

28− (ST f) <$> (ST a) = ST (\st => do (g, r) <- f st

28+ (ST f) <*> (ST a) = ST (\st => do (g, r) <- f st

29 (b, t) <- a r

30 return (g b, t))

31

libs/base/Control/Monad/Writer.idr+1−1

@@ -25,7 +25,7 @@ instance Functor f => Functor (WriterT w f) where

25

26instance (Monoid w, Applicative m) => Applicative (WriterT w m) where

27 pure a = WR $ pure (a, neutral)

28− (WR f) <$> (WR v) = WR $ liftA2 merge f v where

28+ (WR f) <*> (WR v) = WR $ liftA2 merge f v where

29 merge (fn, w) (a, w') = (fn a, w <+> w')

30

31instance (Monoid w, Alternative m) => Alternative (WriterT w m) where

libs/base/Data/Erased.idr+1−1

@@ -16,7 +16,7 @@ instance Functor Erased where

16

17instance Applicative Erased where

18 pure = Erase

19− (<$>) (Erase f) (Erase x) = Erase (f x)

19+ (<*>) (Erase f) (Erase x) = Erase (f x)

20

21instance Monad Erased where

22 (>>=) (Erase x) f = f x

libs/base/Data/Matrix.idr+29−29

@@ -7,13 +7,13 @@ import Data.Vect

7

8%default total

9

10−infixr 2 <.> -- vector inner product

10+infixr 2 <:> -- vector inner product

11infixr 2 >< -- vector outer product

12infixr 2 <<>> -- matrix commutator

13infixr 2 >><< -- matrix anticommutator

14infixl 3 <\> -- row times a matrix

15infixr 4 </> -- matrix times a column

16−infixr 5 <> -- matrix multiplication

16+infixr 5 <> -- matrix multiplication

17infixr 7 \&\ -- vector tensor product

18infixr 7 <&> -- matrix tensor product

19

@@ -26,14 +26,14 @@ instance Semigroup a => Semigroup (Vect n a) where

26

27instance Monoid a => Monoid (Vect n a) where

28 neutral {n} = replicate n neutral

29−

29+

30instance Group a => Group (Vect n a) where

31 inverse = map inverse

32

33instance AbelianGroup a => AbelianGroup (Vect n a) where {}

34

35instance Ring a => Ring (Vect n a) where

36− (<*>) v w = zipWith (<*>) v w

36+ (<.>) v w = zipWith (<.>) v w

37

38instance RingWithUnity a => RingWithUnity (Vect n a) where

39 unity {n} = replicate n unity

@@ -42,7 +42,7 @@ instance Field a => Field (Vect n a) where

42 inverseM = map inverseM

43

44instance RingWithUnity a => Module a (Vect n a) where

45− (<#>) r v = map (r <*>) v

45+ (<#>) r v = map (r <.>) v

46

47instance RingWithUnity a => Module a (Vect n (Vect l a)) where

48 (<#>) r m = map (r <#>) m

@@ -53,12 +53,12 @@ instance RingWithUnity a => Module a (Vect n (Vect l a)) where

53-----------------------------------------------------------------------

54

55||| Inner product of ring vectors

56−(<.>) : Ring a => Vect n a -> Vect n a -> a

56+(<:>) : Ring a => Vect n a -> Vect n a -> a

57−(<.>) w v = foldr (<+>) neutral (zipWith (<*>) w v)

57+(<:>) w v = foldr (<+>) neutral (zipWith (<.>) w v)

58

59||| Tensor multiply (⊗) ring vectors

60(\&\) : Ring a => Vect n a -> Vect m a -> Vect (n * m) a

61−(\&\) {n} {m} v w = zipWith (<*>) (oextend m v) (orep n w) where

61+(\&\) {n} {m} v w = zipWith (<.>) (oextend m v) (orep n w) where

62 orep : (n : Nat) -> Vect m a -> Vect (n * m) a

63 orep n v = concat $ replicate n v

64 oextend : (n : Nat) -> Vect k a -> Vect (k * n) a

@@ -90,15 +90,15 @@ indices f1 f2 m = index f2 (index f1 m)

90

91||| Matrix times a column vector

92(</>) : Ring a => Matrix n m a -> Vect m a -> Vect n a

93−(</>) m v = map (v <.>) m

93+(</>) m v = map (v <:>) m

94

95||| Matrix times a row vector

96(<\>) : Ring a => Vect n a -> Matrix n m a -> Vect m a

97−(<\>) r m = map (r <.>) $ transpose m

97+(<\>) r m = map (r <:>) $ transpose m

98

99||| Matrix multiplication

100−(<>) : Ring a => Matrix n k a ->

100+(<>) : Ring a => Matrix n k a ->

101− Matrix k m a ->

101+ Matrix k m a ->

102 Matrix n m a

103(<>) m1 m2 = map (<\> m2) m1

104

@@ -110,11 +110,11 @@ indices f1 f2 m = index f2 (index f1 m)

110 stepTwo : Matrix h1 w1 a -> Matrix h2 w2 a -> Matrix (h1 * h2) w2 a

111 stepTwo {h1} m1 m2 = concat $ (Vect.replicate h1) m2

112

113−||| Cast a vector from a standard Vect to a proper n x 1 matrix

113+||| Cast a vector from a standard Vect to a proper n x 1 matrix

114col : Vect n a -> Matrix n 1 a

115col v = map (\x => [x]) v

116

117−||| Cast a row from a standard Vect to a proper 1 x n matrix

117+||| Cast a row from a standard Vect to a proper 1 x n matrix

118row : Vect n a -> Matrix 1 n a

119row r = [r]

120

@@ -157,11 +157,11 @@ instance Monoid Integer where

157

158instance Group Integer where

159 inverse = (* -1)

160−

160+

161instance AbelianGroup Integer

162

163−instance Ring Integer where

163+instance Ring Integer where

164− (<*>) = (*)

164+ (<.>) = (*)

165

166instance RingWithUnity Integer where

167 unity = 1

@@ -175,11 +175,11 @@ instance Monoid Int where

175

176instance Group Int where

177 inverse = (* -1)

178−

178+

179instance AbelianGroup Int

180

181−instance Ring Int where

181+instance Ring Int where

182− (<*>) = (*)

182+ (<.>) = (*)

183

184instance RingWithUnity Int where

185 unity = 1

@@ -193,11 +193,11 @@ instance Monoid Float where

193

194instance Group Float where

195 inverse = (* -1)

196−

196+

197instance AbelianGroup Float

198

199−instance Ring Float where

199+instance Ring Float where

200− (<*>) = (*)

200+ (<.>) = (*)

201

202instance RingWithUnity Float where

203 unity = 1

@@ -211,7 +211,7 @@ instance Semigroup Nat where

211

212instance Monoid Nat where

213 neutral = 0

214−

214+

215instance VerifiedSemigroup Nat where

216 semigroupOpIsAssociative = plusAssociative

217

@@ -228,12 +228,12 @@ instance Monoid ZZ where

228

229instance Group ZZ where

230 inverse = (* -1)

231−

231+

232instance AbelianGroup ZZ

233

234−instance Ring ZZ where

234+instance Ring ZZ where

235− (<*>) = (*)

235+ (<.>) = (*)

236−

236+

237instance RingWithUnity ZZ where

238 unity = 1

239

@@ -250,7 +250,7 @@ instance Group a => Group (Complex a) where

250instance Ring a => AbelianGroup (Complex a) where {}

251

252instance Ring a => Ring (Complex a) where

253− (<*>) (a :+ b) (c :+ d) = (a <*> c <-> b <*> d) :+ (a <*> d <+> b <*> c)

253+ (<.>) (a :+ b) (c :+ d) = (a <.> c <-> b <.> d) :+ (a <.> d <+> b <.> c)

254

255instance RingWithUnity a => RingWithUnity (Complex a) where

256 unity = (unity :+ neutral)

libs/base/Data/Morphisms.idr+1−1

@@ -25,7 +25,7 @@ instance Functor (Morphism r) where

25

26instance Applicative (Morphism r) where

27 pure a = Mor $ const a

28− (Mor f) <$> (Mor a) = Mor $ \r => f r $ a r

28+ (Mor f) <*> (Mor a) = Mor $ \r => f r $ a r

29

30instance Monad (Morphism r) where

31 (Mor h) >>= f = Mor $ \r => applyMor (f $ h r) r

libs/base/Data/VectType.idr+1−1

@@ -529,7 +529,7 @@ transpose (x :: xs) = zipWith (::) x (transpose xs)

529instance Applicative (Vect k) where

530 pure = replicate _

531

532− fs <$> vs = zipWith apply fs vs

532+ fs <*> vs = zipWith apply fs vs

533

534instance Monad (Vect n) where

535 m >>= f = diag (map f m)

libs/base/Network/Cgi.idr+1−1

@@ -36,7 +36,7 @@ instance Functor CGI where

36instance Applicative CGI where

37 pure v = MkCGI (\s => return (v, s))

38

39− (MkCGI a) <$> (MkCGI b) = MkCGI (\s => do (f, i) <- a s

39+ (MkCGI a) <*> (MkCGI b) = MkCGI (\s => do (f, i) <- a s

40 (c, j) <- b i

41 return (f c, j))

42

libs/base/Providers.idr+3−3

@@ -17,9 +17,9 @@ instance Functor Provider where

17 map f (Error err) = Error err

18

19instance Applicative Provider where

20− (Provide f) <$> (Provide x) = Provide (f x)

20+ (Provide f) <*> (Provide x) = Provide (f x)

21− (Provide f) <$> (Error err) = Error err

21+ (Provide f) <*> (Error err) = Error err

22− (Error err) <$> _ = Error err

22+ (Error err) <*> _ = Error err

23 pure = Provide

24

25instance Monad Provider where

libs/base/System/Concurrency/Process.idr+1−1

@@ -19,7 +19,7 @@ instance Functor (Process msg) where

19

20instance Applicative (Process msg) where

21 pure = Lift . return

22− (Lift f) <$> (Lift a) = Lift (f <$> a)

22+ (Lift f) <*> (Lift a) = Lift (f <*> a)

23

24instance Monad (Process msg) where

25 (Lift io) >>= k = Lift (do x <- io

libs/effects/Effect/Memory.idr+12−12

@@ -24,11 +24,11 @@ data RawMemory : Effect where

24 (size : Nat) ->

25 So (offset + size <= i) ->

26 RawMemory (Vect size Bits8)

27− (MemoryChunk n i) (\v => MemoryChunk n i)

27+ (MemoryChunk n i) (\v => MemoryChunk n i)

28 Poke : (offset : Nat) ->

29 (Vect size Bits8) ->

30 So (offset <= i && offset + size <= n) ->

31− RawMemory () (MemoryChunk n i) (\v => MemoryChunk n (max i (offset + size)))

31+ RawMemory () (MemoryChunk n i) (\v => MemoryChunk n (max i (offset + size)))

32 Move : (src : MemoryChunk src_size src_init) ->

33 (dst_offset : Nat) ->

34 (src_offset : Nat) ->

@@ -36,8 +36,8 @@ data RawMemory : Effect where

36 So (dst_offset <= dst_init && dst_offset + size <= dst_size) ->

37 So (src_offset + size <= src_init) ->

38 RawMemory () (MemoryChunk dst_size dst_init)

39− (\v => MemoryChunk dst_size (max dst_init (dst_offset + size)))

39+ (\v => MemoryChunk dst_size (max dst_init (dst_offset + size)))

40− GetRawPtr : RawMemory (MemoryChunk n i) (MemoryChunk n i) (\v => MemoryChunk n i)

40+ GetRawPtr : RawMemory (MemoryChunk n i) (MemoryChunk n i) (\v => MemoryChunk n i)

41

42private

43do_malloc : Nat -> IOExcept String Ptr

@@ -84,9 +84,9 @@ instance Handler RawMemory (IOExcept String) where

84 = do ptr <- do_malloc n

85 k () (CH ptr)

86 handle {-{res = MemoryChunk _ offset}-} (CH ptr) (Initialize {i} c size _) k

87− = ioe_lift (do_memset ptr i c size) $> k () (CH ptr)

87+ = ioe_lift (do_memset ptr i c size) *> k () (CH ptr)

88 handle (CH ptr) (Free) k

89− = ioe_lift (do_free ptr) $> k () ()

89+ = ioe_lift (do_free ptr) *> k () ()

90 handle (CH ptr) (Peek offset size _) k

91 = do res <- ioe_lift (do_peek ptr offset size)

92 k res (CH ptr)

@@ -102,7 +102,7 @@ instance Handler RawMemory (IOExcept String) where

102RAW_MEMORY : Type -> EFFECT

103RAW_MEMORY t = MkEff t RawMemory

104

105−allocate : (n : Nat) ->

105+allocate : (n : Nat) ->

106 Eff () [RAW_MEMORY ()] (\v => [RAW_MEMORY (MemoryChunk n 0)])

107allocate size = call $ Allocate size

108

@@ -111,7 +111,7 @@ initialize : {i : Nat} ->

111 Bits8 ->

112 (size : Nat) ->

113 So (i + size <= n) ->

114− Eff () [RAW_MEMORY (MemoryChunk n i)]

114+ Eff () [RAW_MEMORY (MemoryChunk n i)]

115 (\v => [RAW_MEMORY (MemoryChunk n (i + size))])

116initialize c size prf = call $ Initialize c size prf

117

@@ -122,7 +122,7 @@ peek : {i : Nat} ->

122 (offset : Nat) ->

123 (size : Nat) ->

124 So (offset + size <= i) ->

125− { [RAW_MEMORY (MemoryChunk n i)] } Eff (Vect size Bits8)

125+ { [RAW_MEMORY (MemoryChunk n i)] } Eff (Vect size Bits8)

126peek offset size prf = call $ Peek offset size prf

127

128poke : {n : Nat} ->

@@ -130,12 +130,12 @@ poke : {n : Nat} ->

130 (offset : Nat) ->

131 Vect size Bits8 ->

132 So (offset <= i && offset + size <= n) ->

133− Eff () [RAW_MEMORY (MemoryChunk n i)]

133+ Eff () [RAW_MEMORY (MemoryChunk n i)]

134 (\v => [RAW_MEMORY (MemoryChunk n (max i (offset + size)))])

135poke offset content prf = call $ Poke offset content prf

136

137private

138−getRawPtr : { [RAW_MEMORY (MemoryChunk n i)] } Eff (MemoryChunk n i)

138+getRawPtr : { [RAW_MEMORY (MemoryChunk n i)] } Eff (MemoryChunk n i)

139getRawPtr = call $ GetRawPtr

140

141private

@@ -173,5 +173,5 @@ move : {dst_size : Nat} ->

173move dst_offset src_offset size dst_bounds src_bounds

174 = do src_ptr <- Src :- getRawPtr

175 Dst :- move' src_ptr dst_offset src_offset size dst_bounds src_bounds

176− return ()

176+ return ()

177

libs/effects/Effect/Monad.idr+1−1

@@ -11,7 +11,7 @@ using (xs : List EFFECT, m : Type -> Type)

11

12 instance Applicative (\a => EffM m a xs (\v => xs)) where

13 pure = value

14− (<$>) f a = do f' <- f

14+ (<*>) f a = do f' <- f

15 a' <- a

16 value (f' a')

17

libs/effects/Effects.idr+3−3

@@ -174,7 +174,7 @@ return x = value x

174

175-- ------------------------------------------------------ [ for idiom brackets ]

176

177−infixl 2 <$>

177+infixl 2 <*>

178

179pure : a -> Eff a xs (\v => xs)

180pure = value

@@ -182,9 +182,9 @@ pure = value

182pureM : (val : a) -> Eff a (xs val) xs

183pureM = value

184

185−(<$>) : Eff (a -> b) xs (\v => xs) ->

185+(<*>) : Eff (a -> b) xs (\v => xs) ->

186 Eff a xs (\v => xs) -> Eff b xs (\v => xs)

187−(<$>) prog v = do fn <- prog

187+(<*>) prog v = do fn <- prog

188 arg <- v

189 return (fn arg)

190

libs/oldeffects/Effect/Monad.idr+1−1

@@ -11,7 +11,7 @@ using (xs : List EFFECT, m : Type -> Type)

11

12 instance Applicative (\a => EffM m a xs (\v => xs)) where

13 pure = value

14− (<$>) f a = do f' <- f

14+ (<*>) f a = do f' <- f

15 a' <- a

16 value (f' a')

17

libs/oldeffects/Effects.idr+3−3

@@ -185,16 +185,16 @@ return x = value x

185

186-- ------------------------------------------------------ [ for idiom brackets ]

187

188−infixl 2 <$>

188+infixl 2 <*>

189

190pure : a -> Eff m a xs (\v => xs)

191pure = value

192

193syntax pureM [val] = with_val val (pure ())

194

195−(<$>) : Eff m (a -> b) xs (\v => xs) ->

195+(<*>) : Eff m (a -> b) xs (\v => xs) ->

196 Eff m a xs (\v => xs) -> Eff m b xs (\v => xs)

197−(<$>) prog v = do fn <- prog

197+(<*>) prog v = do fn <- prog

198 arg <- v

199 return (fn arg)

200

libs/prelude/Language/Reflection/Tactical.idr+1−1

@@ -44,7 +44,7 @@ instance Functor Tactical where

44

45instance Applicative Tactical where

46 pure x = prim__PureTactical x

47− f <$> x = prim__BindTactical f $ \g =>

47+ f <*> x = prim__BindTactical f $ \g =>

48 prim__BindTactical x $ \y =>

49 prim__PureTactical $ g y

50

libs/prelude/Prelude.idr+8−8

@@ -249,31 +249,31 @@ instance Functor (Either e) where

249instance Applicative PrimIO where

250 pure = prim_io_return

251

252− am <$> bm = prim_io_bind am (\f => prim_io_bind bm (prim_io_return . f))

252+ am <*> bm = prim_io_bind am (\f => prim_io_bind bm (prim_io_return . f))

253

254instance Applicative (IO' ffi) where

255 pure x = io_return x

256− f <$> a = io_bind f (\f' =>

256+ f <*> a = io_bind f (\f' =>

257 io_bind a (\a' =>

258 io_return (f' a')))

259

260instance Applicative Maybe where

261 pure = Just

262

263− (Just f) <$> (Just a) = Just (f a)

263+ (Just f) <*> (Just a) = Just (f a)

264− _ <$> _ = Nothing

264+ _ <*> _ = Nothing

265

266instance Applicative (Either e) where

267 pure = Right

268

269− (Left a) <$> _ = Left a

269+ (Left a) <*> _ = Left a

270− (Right f) <$> (Right r) = Right (f r)

270+ (Right f) <*> (Right r) = Right (f r)

271− (Right _) <$> (Left l) = Left l

271+ (Right _) <*> (Left l) = Left l

272

273instance Applicative List where

274 pure x = [x]

275

276− fs <$> vs = concatMap (\f => map f vs) fs

276+ fs <*> vs = concatMap (\f => map f vs) fs

277

278---- Alternative instances

279

libs/prelude/Prelude/Algebra.idr+37−37

@@ -5,7 +5,7 @@ import Builtins

5-- XXX: change?

6infixl 6 <->

7infixl 6 <+>

8−infixl 6 <*>

8+infixl 6 <.>

9infixl 5 <#>

10

11%access public

@@ -96,18 +96,18 @@ class (VerifiedGroup a, AbelianGroup a) => VerifiedAbelianGroup a where

96||| + Inverse for `<+>`:

97||| forall a, a <+> inverse a == neutral

98||| forall a, inverse a <+> a == neutral

99−||| + Associativity of `<*>`:

99+||| + Associativity of `<.>`:

100−||| forall a b c, a <*> (b <*> c) == (a <*> b) <*> c

100+||| forall a b c, a <.> (b <.> c) == (a <.> b) <.> c

101−||| + Distributivity of `<*>` and `<->`:

101+||| + Distributivity of `<.>` and `<->`:

102−||| forall a b c, a <*> (b <+> c) == (a <*> b) <+> (a <*> c)

102+||| forall a b c, a <.> (b <+> c) == (a <.> b) <+> (a <.> c)

103−||| forall a b c, (a <+> b) <*> c == (a <*> c) <+> (b <*> c)

103+||| forall a b c, (a <+> b) <.> c == (a <.> c) <+> (b <.> c)

104class AbelianGroup a => Ring a where

105− (<*>) : a -> a -> a

105+ (<.>) : a -> a -> a

106

107class (VerifiedAbelianGroup a, Ring a) => VerifiedRing a where

108− total ringOpIsAssociative : (l, c, r : a) -> l <*> (c <*> r) = (l <*> c) <*> r

108+ total ringOpIsAssociative : (l, c, r : a) -> l <.> (c <.> r) = (l <.> c) <.> r

109− total ringOpIsDistributiveL : (l, c, r : a) -> l <*> (c <+> r) = (l <*> c) <+> (l <*> r)

109+ total ringOpIsDistributiveL : (l, c, r : a) -> l <.> (c <+> r) = (l <.> c) <+> (l <.> r)

110− total ringOpIsDistributiveR : (l, c, r : a) -> (l <+> c) <*> r = (l <*> r) <+> (c <*> r)

110+ total ringOpIsDistributiveR : (l, c, r : a) -> (l <+> c) <.> r = (l <.> r) <+> (c <.> r)

111

112||| Sets equipped with two binary operations, one associative and commutative

113||| supplied with a neutral element, and the other associative supplied with a

@@ -124,20 +124,20 @@ class (VerifiedAbelianGroup a, Ring a) => VerifiedRing a where

124||| + Inverse for `<+>`:

125||| forall a, a <+> inverse a == neutral

126||| forall a, inverse a <+> a == neutral

127−||| + Associativity of `<*>`:

127+||| + Associativity of `<.>`:

128−||| forall a b c, a <*> (b <*> c) == (a <*> b) <*> c

128+||| forall a b c, a <.> (b <.> c) == (a <.> b) <.> c

129−||| + Neutral for `<*>`:

129+||| + Neutral for `<.>`:

130−||| forall a, a <*> unity == a

130+||| forall a, a <.> unity == a

131−||| forall a, unity <*> a == a

131+||| forall a, unity <.> a == a

132−||| + Distributivity of `<*>` and `<->`:

132+||| + Distributivity of `<.>` and `<->`:

133−||| forall a b c, a <*> (b <+> c) == (a <*> b) <+> (a <*> c)

133+||| forall a b c, a <.> (b <+> c) == (a <.> b) <+> (a <.> c)

134−||| forall a b c, (a <+> b) <*> c == (a <*> c) <+> (b <*> c)

134+||| forall a b c, (a <+> b) <.> c == (a <.> c) <+> (b <.> c)

135class Ring a => RingWithUnity a where

136 unity : a

137

138class (VerifiedRing a, RingWithUnity a) => VerifiedRingWithUnity a where

139− total ringWithUnityIsUnityL : (l : a) -> l <*> unity = l

139+ total ringWithUnityIsUnityL : (l : a) -> l <.> unity = l

140− total ringWithUnityIsUnityR : (r : a) -> unity <*> r = r

140+ total ringWithUnityIsUnityR : (r : a) -> unity <.> r = r

141

142||| Sets equipped with a binary operation that is commutative, associative and

143||| idempotent. Must satisfy the following laws:

@@ -281,31 +281,31 @@ class (VerifiedBoundedJoinSemilattice a, VerifiedBoundedMeetSemilattice a, Verif

281||| + Inverse for `<+>`:

282||| forall a, a <+> inverse a == neutral

283||| forall a, inverse a <+> a == neutral

284−||| + Associativity of `<*>`:

284+||| + Associativity of `<.>`:

285−||| forall a b c, a <*> (b <*> c) == (a <*> b) <*> c

285+||| forall a b c, a <.> (b <.> c) == (a <.> b) <.> c

286−||| + Unity for `<*>`:

286+||| + Unity for `<.>`:

287−||| forall a, a <*> unity == a

287+||| forall a, a <.> unity == a

288−||| forall a, unity <*> a == a

288+||| forall a, unity <.> a == a

289−||| + InverseM of `<*>`:

289+||| + InverseM of `<.>`:

290−||| forall a, a <*> inverseM a == unity

290+||| forall a, a <.> inverseM a == unity

291−||| forall a, inverseM a <*> a == unity

291+||| forall a, inverseM a <.> a == unity

292−||| + Distributivity of `<*>` and `<->`:

292+||| + Distributivity of `<.>` and `<->`:

293−||| forall a b c, a <*> (b <+> c) == (a <*> b) <+> (a <*> c)

293+||| forall a b c, a <.> (b <+> c) == (a <.> b) <+> (a <.> c)

294−||| forall a b c, (a <+> b) <*> c == (a <*> c) <+> (b <*> c)

294+||| forall a b c, (a <+> b) <.> c == (a <.> c) <+> (b <.> c)

295class RingWithUnity a => Field a where

296 inverseM : a -> a

297

298class (VerifiedRing a, Field a) => VerifiedField a where

299− total fieldInverseIsInverseL : (l : a) -> l <*> inverseM l = unity

299+ total fieldInverseIsInverseL : (l : a) -> l <.> inverseM l = unity

300− total fieldInverseIsInverseR : (r : a) -> inverseM r <*> r = unity

300+ total fieldInverseIsInverseR : (r : a) -> inverseM r <.> r = unity

301

302||| A module over a ring is an additive abelian group of 'vectors' endowed with a

303−||| scale operation multiplying vectors by ring elements, and distributivity laws

303+||| scale operation multiplying vectors by ring elements, and distributivity laws

304−||| relating the scale operation to both ring addition and module addition.

304+||| relating the scale operation to both ring addition and module addition.

305||| Must satisfy the following laws:

306|||

307||| + Compatibility of scalar multiplication with ring multiplication:

308−||| forall a b v, a <#> (b <#> v) = (a <*> b) <#> v

308+||| forall a b v, a <#> (b <#> v) = (a <.> b) <#> v

309||| + Ring unity is the identity element of scalar multiplication:

310||| forall v, unity <#> v = v

311||| + Distributivity of `<#>` and `<+>`:

@@ -315,7 +315,7 @@ class (RingWithUnity a, AbelianGroup b) => Module a b where

315 (<#>) : a -> b -> b

316

317class (VerifiedRingWithUnity a, VerifiedAbelianGroup b, Module a b) => VerifiedModule a b where

318− total moduleScalarMultiplyComposition : (x,y : a) -> (v : b) -> x <#> (y <#> v) = (x <*> y) <#> v

318+ total moduleScalarMultiplyComposition : (x,y : a) -> (v : b) -> x <#> (y <#> v) = (x <.> y) <#> v

319 total moduleScalarUnityIsUnity : (v : b) -> unity <#> v = v

320 total moduleScalarMultDistributiveWRTVectorAddition : (s : a) -> (v, w : b) -> s <#> (v <+> w) = (s <#> v) <+> (s <#> w)

321 total moduleScalarMultDistributiveWRTModuleAddition : (s, t : a) -> (v : b) -> (s <+> t) <#> v = (s <#> v) <+> (t <#> v)

libs/prelude/Prelude/Applicative.idr+17−17

@@ -9,46 +9,46 @@ import Prelude.Functor

9

10---- Applicative functors/Idioms

11

12−infixl 2 <$>

12+infixl 2 <*>

13

14class Functor f => Applicative (f : Type -> Type) where

15 pure : a -> f a

16− (<$>) : f (a -> b) -> f a -> f b

16+ (<*>) : f (a -> b) -> f a -> f b

17

18instance Applicative id where

19 pure a = a

20− f <$> a = f a

20+ f <*> a = f a

21

22class (Applicative f, VerifiedFunctor f) => VerifiedApplicative (f : Type -> Type) where

23 applicativeMap : (x : f a) -> (g : a -> b) ->

24− map g x = pure g <$> x

24+ map g x = pure g <*> x

25− applicativeIdentity : (x : f a) -> pure id <$> x = x

25+ applicativeIdentity : (x : f a) -> pure id <*> x = x

26 applicativeComposition : (x : f a) -> (g1 : f (a -> b)) -> (g2 : f (b -> c)) ->

27− ((pure (.) <$> g2) <$> g1) <$> x = g2 <$> (g1 <$> x)

27+ ((pure (.) <*> g2) <*> g1) <*> x = g2 <*> (g1 <*> x)

28 applicativeHomomorphism : (x : a) -> (g : a -> b) ->

29− (<$>) {f} (pure g) (pure x) = pure {f} (g x)

29+ (<*>) {f} (pure g) (pure x) = pure {f} (g x)

30 applicativeInterchange : (x : a) -> (g : f (a -> b)) ->

31− g <$> pure x = pure (\g' : a -> b => g' x) <$> g

31+ g <*> pure x = pure (\g' : a -> b => g' x) <*> g

32

33−infixl 2 <$

33+infixl 2 <*

34−(<$) : Applicative f => f a -> f b -> f a

34+(<*) : Applicative f => f a -> f b -> f a

35−a <$ b = map const a <$> b

35+a <* b = map const a <*> b

36

37−infixl 2 $>

37+infixl 2 *>

38−($>) : Applicative f => f a -> f b -> f b

38+(*>) : Applicative f => f a -> f b -> f b

39−a $> b = map (const id) a <$> b

39+a *> b = map (const id) a <*> b

40

41||| Lift a function to an applicative

42liftA : Applicative f => (a -> b) -> f a -> f b

43−liftA f a = pure f <$> a

43+liftA f a = pure f <*> a

44

45||| Lift a two-argument function to an applicative

46liftA2 : Applicative f => (a -> b -> c) -> f a -> f b -> f c

47−liftA2 f a b = (map f a) <$> b

47+liftA2 f a b = (map f a) <*> b

48

49||| Lift a three-argument function to an applicative

50liftA3 : Applicative f => (a -> b -> c -> d) -> f a -> f b -> f c -> f d

51−liftA3 f a b c = (map f a) <$> b <$> c

51+liftA3 f a b c = (map f a) <*> b <*> c

52

53infixl 3 <|>

54class Applicative f => Alternative (f : Type -> Type) where

libs/prelude/Prelude/Functor.idr+8

@@ -10,6 +10,14 @@ class Functor (f : Type -> Type) where

10 ||| @ m the morphism

11 map : (m : a -> b) -> f a -> f b

12

13+infixl 4 <$>

14+

15+||| An infix alias for `map`: the action of a functor on morphisms.

16+||| @ f the functor

17+||| @ m the morphism

18+(<$>) : Functor f => (m : a -> b) -> f a -> f b

19+m <$> x = map m x

20+

13class Functor f => VerifiedFunctor (f : Type -> Type) where

21class Functor f => VerifiedFunctor (f : Type -> Type) where

14 functorIdentity : {a : Type} -> (x : f a) -> map id x = id x

22 functorIdentity : {a : Type} -> (x : f a) -> map id x = id x

15 functorComposition : {a : Type} -> {b : Type} -> (x : f a) ->

23 functorComposition : {a : Type} -> {b : Type} -> (x : f a) ->

libs/prelude/Prelude/Monad.idr+1−1

@@ -16,7 +16,7 @@ class Applicative m => Monad (m : Type -> Type) where

16

17class (Monad m, VerifiedApplicative m) => VerifiedMonad (m : Type -> Type) where

18 monadApplicative : (mf : m (a -> b)) -> (mx : m a) ->

19− mf <$> mx = mf >>= \f =>

19+ mf <*> mx = mf >>= \f =>

20 mx >>= \x =>

21 pure (f x)

22 monadLeftIdentity : (x : a) -> (f : a -> m b) -> return x >>= f = f x

libs/prelude/Prelude/Stream.idr+1−1

@@ -111,7 +111,7 @@ scanr f (x :: xs) = f x (foldr f xs) :: scanr f xs

111

112instance Applicative Stream where

113 pure = repeat

114− (<$>) = zipWith apply

114+ (<*>) = zipWith apply

115

116instance Monad Stream where

117 s >>= f = diag (map f s)

libs/prelude/Prelude/Traversable.idr+2−2

@@ -8,10 +8,10 @@ import Prelude.Foldable

8import Prelude.Functor

9

10traverse_ : (Foldable t, Applicative f) => (a -> f b) -> t a -> f ()

11−traverse_ f = foldr (($>) . f) (pure ())

11+traverse_ f = foldr ((*>) . f) (pure ())

12

13sequence_ : (Foldable t, Applicative f) => t (f a) -> f ()

14−sequence_ = foldr ($>) (pure ())

14+sequence_ = foldr (*>) (pure ())

15

16for_ : (Foldable t, Applicative f) => t a -> (a -> f b) -> f ()

17for_ = flip traverse_

samples/interp.idr+2−2

@@ -37,8 +37,8 @@ using (G : Vect n Ty)

37 index_first = stop

38 index_next = pop

39

40− (<$>) : |(f : Expr G (TyFun a t)) -> Expr G a -> Expr G t

40+ (<*>) : |(f : Expr G (TyFun a t)) -> Expr G a -> Expr G t

41− (<$>) = \f, a => App f a

41+ (<*>) = \f, a => App f a

42

43 pure : Expr G a -> Expr G a

44 pure = id

src/Idris/AbsSyntaxTree.hs+1−1

@@ -1157,7 +1157,7 @@ updateSyntaxRules rules (SyntaxRules sr) = SyntaxRules newRules

1157

1158initDSL = DSL (PRef f (sUN ">>="))

1159 (PRef f (sUN "return"))

1160− (PRef f (sUN "<$>"))

1160+ (PRef f (sUN "<*>"))

1161 (PRef f (sUN "pure"))

1162 Nothing

1163 Nothing

test/reg027/reg027.idr+1−1

@@ -14,7 +14,7 @@ instance Functor IntFn where -- (\x => Int -> x) where

14

15instance Applicative (\x => Int -> x) where

16 pure v = \x => v

17− (<$>) f a = \x => f x (a x)

17+ (<*>) f a = \x => f x (a x)

18

19instance Monad IntFn where

20 f >>= k = \x => k (f x) x

test/reg050/expected+6−6

@@ -12,13 +12,13 @@ When elaborating an application of function Prelude.Monad.>>=:

12 \{uv0} => argTy -> uv

13./baddoublebang.idr:6:26: error: not

14 a terminator, expected: "$",

15− "$>", "&&", "*", "+", "++", "-",

15+ "&&", "*", "*>", "+", "++", "-",

16 "->", ".", "/", "/=", "::", ";",

17− "<", "<#>", "<$", "<$>", "<*>",

17+ "<", "<#>", "<$>", "<*", "<*>",

18− "<+>", "<->", "<<", "<=", "<|>",

18+ "<+>", "<->", "<.>", "<<", "<=",

19− "=", "==", ">", ">=", ">>",

19+ "<|>", "=", "==", ">", ">=",

20− ">>=", "\\\\", "`", "in", "||",

20+ ">>", ">>=", "\\\\", "`", "in",

21− "~=~",

21+ "||", "~=~",

22 ambiguous use of a left-associative operator,

23 ambiguous use of a non-associative operator,

24 ambiguous use of a right-associative operator,

test/reg053/four.idr+1−1

@@ -5,5 +5,5 @@ data FourFunctor y = Four y y y y

5traverseFourFunctor : Applicative f ->

6 (x -> f b) -> FourFunctor x -> f (FourFunctor b)

7traverseFourFunctor constr f (Four w x y z)

8− = pure Four <$> (f w) <$> (f x) <$> (f y) <$> (f z)

8+ = pure Four <*> (f w) <*> (f x) <*> (f y) <*> (f z)

9

test/sugar001/test007.idr+1−1

@@ -19,7 +19,7 @@ instance Functor Eval where

19instance Applicative Eval where

20 pure x = MkEval (\e => Just x)

21

22− (<$>) (MkEval f) (MkEval g) = MkEval (\x => appAux (f x) (g x)) where

22+ (<*>) (MkEval f) (MkEval g) = MkEval (\x => appAux (f x) (g x)) where

23 appAux : Maybe (a -> b) -> Maybe a -> Maybe b

24 appAux (Just fx) (Just gx) = Just (fx gx)

25 appAux _ _ = Nothing

test/tutorial003/tutorial003.idr+1−1

@@ -19,7 +19,7 @@ instance Functor Eval where

19instance Applicative Eval where

20 pure x = MkEval (\e => Just x)

21

22− (<$>) (MkEval f) (MkEval g) = MkEval (\x => app (f x) (g x)) where

22+ (<*>) (MkEval f) (MkEval g) = MkEval (\x => app (f x) (g x)) where

23 app : Maybe (a -> b) -> Maybe a -> Maybe b

24 app (Just fx) (Just gx) = Just (fx gx)

25 app _ _ = Nothing