git.iko.soy/Idris-dev
on master help sign in
Add laziness to values which aren't evaluated in all branches of a function.

Most notably, this includes making (&&) and (||) lazy in their second arguments, allowing conventional short-circuiting behavior. Correspondingly, the foldable functions `and` and `or` now short-circuit as well by applying foldables which contain lazy Bool values. Unlike Haskell, short-circuiting occurs from right to left on lists, because as Idris is a strict language, `foldr` evaluates from the inside (right side) out.

commit75b80818d6de050f39e289cb5a2fedb0c2eab5a3 authorbmsherman <ben.sherman@example.com> dateThu 1 May 2014, 01:28 (12 years ago) parent04801ec
8 files changed+22−22
compare with master
unifiedsplit
libs/effects/Effects.idr+2−2 libs/oldeffects/Effects.idr+1−1 libs/prelude/Prelude/Applicative.idr+2−2 libs/prelude/Prelude/Bool.idr+2−2 libs/prelude/Prelude/Either.idr+4−4 libs/prelude/Prelude/Foldable.idr+6−6 libs/prelude/Prelude/List.idr+2−2 libs/prelude/Prelude/Maybe.idr+3−3
libs/effects/Effects.idr+2−2
@@ -337,8 +337,8 @@ mapVE f [] = pure []
337337mapVE f (x :: xs) = [| f x :: mapVE f xs |]
338338
339339
340−when : Applicative m => Bool -> ({xs} Eff m ()) -> {xs} Eff m ()
341−when True e = e
340+when : Applicative m => Bool -> Lazy ({xs} Eff m ()) -> {xs} Eff m ()
341+when True e = Force e
342342when False e = pure ()
343343
344344-- --------------------------------------------------------------------- [ EOF ]
libs/oldeffects/Effects.idr+1−1
@@ -303,6 +303,6 @@ mapE : Applicative m => (a -> Eff m xs b) -> List a -> Eff m xs (List b)
303303mapE f [] = pure []
304304mapE f (x :: xs) = [| f x :: mapE f xs |]
305305
306−when : Applicative m => Bool -> Eff m xs () -> Eff m xs ()
306+when : Applicative m => Bool -> Lazy (Eff m xs ()) -> Eff m xs ()
307307when True e = e
308308when False e = pure ()
libs/prelude/Prelude/Applicative.idr+2−2
@@ -41,5 +41,5 @@ class Applicative f => Alternative (f : Type -> Type) where
4141guard : Alternative f => Bool -> f ()
4242guard a = if a then pure () else empty
4343
44−when : Applicative f => Bool -> f () -> f ()
45−when a f = if a then f else pure ()
44+when : Applicative f => Bool -> Lazy (f ()) -> f ()
45+when a f = if a then Force f else pure ()
libs/prelude/Prelude/Bool.idr+2−2
@@ -23,12 +23,12 @@ syntax if [test] then [t] else [e] = boolElim test (Delay t) (Delay e)
2323infixl 4 &&, ||
2424
2525||| Boolean OR
26−(||) : Bool -> Bool -> Bool
26+(||) : Bool -> Lazy Bool -> Bool
2727(||) False x = x
2828(||) True _ = True
2929
3030||| Boolean AND
31−(&&) : Bool -> Bool -> Bool
31+(&&) : Bool -> Lazy Bool -> Bool
3232(&&) True x = x
3333(&&) False _ = False
3434
libs/prelude/Prelude/Either.idr+4−4
@@ -39,9 +39,9 @@ choose False = Right oh
3939||| @ f the action to take on Left
4040||| @ g the action to take on Right
4141||| @ e the sum to analyze
42−either : (f : a -> c) -> (g : b -> c) -> (e : Either a b) -> c
43−either l r (Left x) = l x
44−either l r (Right x) = r x
42+either : (f : Lazy (a -> c)) -> (g : Lazy (b -> c)) -> (e : Either a b) -> c
43+either l r (Left x) = (Force l) x
44+either l r (Right x) = (Force r) x
4545
4646||| Keep the payloads of all Left constructors in a list of Eithers
4747lefts : List (Either a b) -> List a
@@ -74,7 +74,7 @@ fromEither (Right r) = r
7474
7575||| Convert a Maybe to an Either by using a default value in case of Nothing
7676||| @ e the default value
77−maybeToEither : (def : e) -> Maybe a -> Either e a
77+maybeToEither : (def : Lazy e) -> Maybe a -> Either e a
7878maybeToEither def (Just j) = Right j
7979maybeToEither def Nothing = Left def
8080
libs/prelude/Prelude/Foldable.idr+6−6
@@ -20,17 +20,17 @@ concat = foldr (<+>) neutral
2020concatMap : (Foldable t, Monoid m) => (a -> m) -> t a -> m
2121concatMap f = foldr ((<+>) . f) neutral
2222
23−and : Foldable t => t Bool -> Bool
24−and = foldr (&&) True
23+and : Foldable t => t (Lazy Bool) -> Bool
24+and = foldr (flip (&&)) True
2525
26−or : Foldable t => t Bool -> Bool
27−or = foldr (||) False
26+or : Foldable t => t (Lazy Bool) -> Bool
27+or = foldr (flip (||)) False
2828
2929any : Foldable t => (a -> Bool) -> t a -> Bool
30−any p = foldr ((||) . p) False
30+any p = foldr (flip (||) . Delay . p) False
3131
3232all : Foldable t => (a -> Bool) -> t a -> Bool
33−all p = foldr ((&&) . p) True
33+all p = foldr (flip (&&) . Delay . p) True
3434
3535sum : (Foldable t, Num a) => t a -> a
3636sum = foldr (+) 0
libs/prelude/Prelude/List.idr+2−2
@@ -182,9 +182,9 @@ dropWhile p (x::xs) = if p x then dropWhile p xs else x::xs
182182||| @ nil what to return at the end of the list
183183||| @ cons what to do at each step of recursion
184184||| @ xs the list to recurse over
185−list : (nil : b) -> (cons : a -> List a -> b) -> (xs : List a) -> b
185+list : (nil : Lazy b) -> (cons : Lazy (a -> List a -> b)) -> (xs : List a) -> b
186186list nil cons [] = nil
187−list nil cons (x::xs) = cons x xs
187+list nil cons (x::xs) = (Force cons) x xs
188188
189189--------------------------------------------------------------------------------
190190-- Building (bigger) lists
libs/prelude/Prelude/Maybe.idr+3−3
@@ -28,15 +28,15 @@ isJust (Just j) = True
2828-- Misc
2929--------------------------------------------------------------------------------
3030
31−maybe : Lazy b -> (a -> b) -> Maybe a -> b
31+maybe : Lazy b -> Lazy (a -> b) -> Maybe a -> b
3232maybe n j Nothing = n
33−maybe n j (Just x) = j x
33+maybe n j (Just x) = (Force j) x
3434
3535fromMaybe : (Lazy a) -> Maybe a -> a
3636fromMaybe def Nothing = def
3737fromMaybe def (Just j) = j
3838
39−toMaybe : Bool -> a -> Maybe a
39+toMaybe : Bool -> Lazy a -> Maybe a
4040toMaybe True j = Just j
4141toMaybe False j = Nothing
4242