Playing with Infinity - Lazy Arithmetic

Question

Many modern programming languages ​​allow us to process potentially endless lists and perform certain operations on them.

Example [Python]:

EvenSquareNumbers = ( x * x for x in naturals() if x mod 2 == 0 ) 

Such lists may exist because only those items that are really required are computed. (Lazy assessment)

I just wondered if it is possible (or even practiced in certain languages) to expand the mechanism of lazy evaluation to arithmetic.

Example: Given an endless list of even numbers evens = [ x | x <- [1..], even x ] evens = [ x | x <- [1..], even x ] We could not calculate

 length evens 

since the calculation required here will never end.

But we could actually determine that

 length evens > 42 

without having to evaluate the entire term length .

Is this possible in any language? What about Haskell?

Edit: To make the point clearer: the question is not how to determine if a lazy list is shorter than a given number. This applies to the use of ordinary built-in functions in such a way that numerical calculations are performed lazily.

sdcvvc showed a solution for Haskell:

 data Nat = Zero | Succ Nat deriving (Show, Eq, Ord) toLazy :: Integer -> Nat toLazy 0 = Zero toLazy n = Succ (toLazy (n-1)) instance Num Nat where (+) (Succ x) y = Succ (x + y) (+) Zero y = y (*) Zero y = Zero (*) x Zero = Zero (*) (Succ x) y = y + (x * y) fromInteger = toLazy abs = id negate = error "Natural only" signum Zero = Zero signum (Succ x) = Succ Zero len [] = Zero len (_:x') = Succ $ len x' -- Test len [1..] < 42 

Is this possible in other languages?

Answer 1

You can create your own natural numbers ...

 data Nat = Zero | Succ Nat deriving (Show, Eq, Ord) len :: [a] -> Nat len = foldr (const Succ) Zero toLazy :: Int -> Nat toLazy 0 = Zero toLazy n = Succ (toLazy (n-1)) a = len [1..] > toLazy 42 

Then a is true, thanks to a lazy estimate. It is very important that len ​​uses foldr, foldl does not work in infinite lists. And you can do arithmetic too (not verified):

 instance Num Nat where (+) (Succ x) y = Succ (x + y) (+) Zero y = y (*) Zero y = Zero (*) x Zero = Zero (*) (Succ x) y = y + (x * y) fromInteger = toLazy abs = id negate = error "Natural only" signum Zero = Zero signum (Succ x) = Succ Zero 

For example, 2 * infinity + 3 is infinite:

 let infinity = Succ infinity *Main> 2 * infinity + 3 (Succ (Succ (Succ ^cCc (Succ (Succ (SuccInterrupted. 

Second solution

Another solution is to use lists () as lazy natural numbers.

 len = map (const ()) toLazy n = replicate n () a = len [1..] > toLazy 42 

Check Hackage .

Edit: Added Num instance.

Edit2:

Translation of the second solution in Python:

 import itertools def length(x): return itertools.imap(lambda: (), x) def to_lazy(n): return itertools.chain([()] * n) 

To add numbers, use itertools.chain; to multiply, use itertools.product. It is not as beautiful as in Haskell, but it works.

In any other strict closure language, you can simulate laziness using type () -> a instead of a. Using this, you can port the first solution from Haskell to other languages. However, it will quickly become unreadable.

See also a good article on single-line Python .

Answer 2

If not for laziness, I think this will work in F #:

 type Nat = Zero | Succ of Nat let rec toLazy x = if x = 0 then Zero else Succ(toLazy(x-1)) type Nat with static member (+)(x:Nat, y:Nat) = match x with | Succ(a) -> Succ(a+y) | Zero -> y static member (*)(x:Nat, y:Nat) = match x,y with | _, Zero -> Zero | Zero, _ -> Zero | Succ(a), b -> b + a*b module NumericLiteralQ = let FromZero() = toLazy 0 let FromOne() = toLazy 1 let FromInt32(x:int) = toLazy x let rec len = function | [] -> 0Q | _::t -> 1Q + len t printfn "%A" (len [1..42] < 100Q) printfn "%A" (len [while true do yield 1] < 100Q) 

But since we need to be lazy, it expands to this:

 let eqLazy<'T> (x:Lazy<'T>) (y:Lazy<'T>) : bool = //' let a = x.Force() let b = y.Force() a = b type Nat = Zero | Succ of LazyNat and [<StructuralComparison(false); StructuralEqualityAttribute(false)>] LazyNat = LN of Lazy<Nat> with override this.GetHashCode() = 0 override this.Equals(o) = match o with | :? LazyNat as other -> let (LN(a)) = this let (LN(b)) = other eqLazy ab | _ -> false interface System.IComparable with member this.CompareTo(o) = match o with | :? LazyNat as other -> let (LN(a)) = this let (LN(b)) = other match a.Force(),b.Force() with | Zero, Zero -> 0 | Succ _, Zero -> 1 | Zero, Succ _ -> -1 | Succ(a), Succ(b) -> compare ab | _ -> failwith "bad" let (|Force|) (ln : LazyNat) = match ln with LN(x) -> x.Force() let rec toLazyNat x = if x = 0 then LN(lazy Zero) else LN(lazy Succ(toLazyNat(x-1))) type LazyNat with static member (+)(((Force x) as lx), ((Force y) as ly)) = match x with | Succ(a) -> LN(lazy Succ(a+ly)) | Zero -> lx module NumericLiteralQ = let FromZero() = toLazyNat 0 let FromOne() = toLazyNat 1 let FromInt32(x:int) = toLazyNat x let rec len = function | LazyList.Nil -> 0Q | LazyList.Cons(_,t) -> LN(lazy Succ(len t)) let shortList = LazyList.of_list [1..42] let infiniteList = LazyList.of_seq (seq {while true do yield 1}) printfn "%A" (len shortList < 100Q) // true printfn "%A" (len infiniteList < 100Q) // false 

This demonstrates why people only write this stuff in Haskell.

Answer 3

Perhaps you will achieve what you want by trying to get more than 42 elements from the Evens.

Answer 4

Not sure I understand your question, but give it a try. You may be looking for threads. I only speak Erlang from the FP language family, so ...

 esn_stream() -> fun() -> esn_stream(1) end. esn_stream(N) -> {N*N, fun() -> esn_stream(N+2) end}. 

Calling a thread always returns the next element, and you have to call fun to get the next element. Thus, you achieve a lazy assessment.

Then you can define the is_stream_longer_than function as:

 is_stream_longer_than(end_of_stream, 0) -> false; is_stream_longer_than(_, 0) -> true; is_stream_longer_than(Stream, N) -> {_, NextStream} = Stream(), is_stream_longer_than(NextStream, N-1). 

Result:

 1> e:is_stream_longer_than(e:esn_stream(), 42). true 2> S0 = e:esn_stream(). #Fun<e.0.6417874> 3> {E1, S1} = S0(). {1,#Fun<e.1.62636971>} 4> {E2, S2} = S1(). {9,#Fun<e.1.62636971>} 5> {E3, S3} = S2(). {25,#Fun<e.1.62636971>}