Playing with infinity - Lazy arithmetics

Question

Many modern programming languages allow us to handle potentially infinite lists and to perform certain operations on them.

Example [Python]:

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

Such lists can exist because only elements that are actually required are computed. (Lazy evaluation)

I just wondered out of interest whether it's possible (or even practised in certain languages) to extend the mechanism of lazy evaluation to arithmetics.

Example: Given the infinite list of even numbers evens = [ x | x <- [1..], even x ] We couldn't compute

length evens

since the computation required here would never terminate.

But we could actually determine that

length evens > 42

without having to evaluate the whole length term.

Is this possible in any language? What about Haskell?

Edit: To make the point clearer: The question is not about how to determine whether a lazy list is shorter than a given number. It's about using conventional builtin functions in a way that numeric computation is done 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 also 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 lazy evaluation. It's crucial that len uses foldr, foldl doesn't work on infinite lists. And you can do some arithmetic too (not tested):

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 infinity:

let infinity = Succ infinity

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

Second solution

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

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

Check Hackage.

Edit: Added instance Num.

Edit2:

Translation of second solution to 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. This isn't as pretty as in Haskell, but it works.

In any other strict language with closures, you can simulate laziness using the type () -> a instead of a. Using that it is possible to translate the first solution from Haskell to other languages. This will quickly get unreadable, however.

See also a nice article on Python one-liners.

Answer 2

If it were not for laziness, I think this would 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 a b
            | _ -> 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 a b
                | _ -> 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

You can probably achieve what you want by trying to get more than 42 elements out of evens.

Answer 4

Not sure I understand your question, but let's give this a try. Perhaps you are looking for streams. I only speak Erlang, out of the FP language family, so...

esn_stream() ->
  fun() -> esn_stream(1) end.

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

Calling the stream always returns the next element, and a fun you should call to retrieve the next element. This way you achieve lazy evaluation.

Then you can define an 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>}