Idris Language - Lazy Code

From libs/prelude/Builtins.idr

||| Two types of delayed computation: that arising from lazy functions, and that
||| arising from infinite data. They differ in their totality condition.
data DelayReason = Infinite | LazyValue

||| The underlying implementation of Lazy and Inf.
%error_reverse
data Delayed : DelayReason -> Type -> Type where
     ||| A delayed computation.
     |||
     ||| Delay is inserted automatically by the elaborator where necessary.
     |||
     ||| Note that compiled code gives `Delay` special semantics.
     ||| @ t   whether this is laziness from an infinite structure or lazy evaluation
     ||| @ a   the type of the eventual value
     ||| @ val a computation that will produce a value
     Delay : {t, a : _} -> (val : a) -> Delayed t a

||| Compute a value from a delayed computation.
|||
||| Inserted by the elaborator where necessary.
Force : {t, a : _} -> Delayed t a -> a
Force (Delay x) = x

||| Lazily evaluated values.
||| At run time, the delayed value will only be computed when required by
||| a case split.
%error_reverse
Lazy : Type -> Type
Lazy t = Delayed LazyValue t

||| Possibly infinite data.
||| A value which may be infinite is accepted by the totality checker if
||| it appears under a data constructor. At run time, the delayed value will
||| only be computed when required by a case split.
%error_reverse
Inf : Type -> Type
Inf t = Delayed Infinite t

from: https://groups.google.com/g/idris-lang/c/QWhCihTtI_w

we already have `Data.List.Lazy` in contrib. Could you please quickly explain what the difference is between that one (which, if I understand correctly, could also be potentially infinite) and your `Colist` data type? The only difference is the use of `Inf` vs `Lazy` and I never really understood this distinction.

I think the distinction is mostly in terms of what is used for termination checking.

If you're using `Lazy`, you are still in the inductive subset of the language (you're just not evaluating the thunk until you actually need it). This means that the right criterion for totality is "making a recursive call on a strict subterm". As a consequence,

```idris
eval : LazyList a -> ()
eval [] = ()
eval (_ :: xs) = eval xs

is total because the recursive call `eval xs` is on an argument `xs` smaller than the input `_ :: xs`. Its effect will be to force all of the thunks in your lazylist.

On the other hand if you use `Inf`, you are now in the coinductive subset of the language and every `Inf`-wrapped subterm may potentially be infinite. If you try to write:

```idris
eval : Colist a -> ()
eval [] = ()
eval (_ :: xs) = eval xs
```

in case of a LazyList, the totality checker will allow me to force the whole list but will stop me from creating a potentially infinite one, while with `Colist` it's the other way round: I am allowed to create a potentially infinite `Colist`, but may not try to evaluate the whole structure without the totality checker complaining.

To experiment with lazy code I created 'x' of type Inf Int but the REPL does not seem to be able to convert to Int:

*myParser> :let x = the (inf True Int) 1
*myParser> x
Delay 1 : Inf Int
*myParser> show x
Can't find implementation for Show (Inf Int)
*myParser> :let y = x+1
Can't find implementation for Num (Inf Int)

but when I add this:

Show x => Show (Inf x) where
  show y = show (Force y)

Show x => Show (Lazy x) where
  show y = show (Force y)

then I get:

*myParser> :let x = the (inf True Int) 1
*myParser> x
Delay 1 : Inf Int
*myParser> show x
"1" : String
*myParser>

Automatic Conversion

I created this file

import public Control.Delayed

getOne : inf True Int
getOne = 1

getTwo : inf True Int
getTwo = 2

getSum : Int
getSum = getOne + getTwo

runtest : String
runtest = show getSum

then complied and ran

mjb@localhost:~/testFiles> idris testlazy -p contrib
     ____    __     _                                          
    /  _/___/ /____(_)____                                     
    / // __  / ___/ / ___/     Version 1.3.2
  _/ // /_/ / /  / (__  )      http://www.idris-lang.org/      
 /___/\__,_/_/  /_/____/       Type :? for help               

Idris is free software with ABSOLUTELY NO WARRANTY.            
For details type :warranty.
Type checking ./testlazy.idr
*testlazy> runtest
"3" : String
*testlazy> 

As you can see, the getSum function can get an 'Int' type from the sum of two 'inf True Int' types even though there was no explicit conversion.

However this does not seem to work with show, I changed the file as follows:

import public Control.Delayed

getOne : inf True Int
getOne = 1

getTwo : inf True Int
getTwo = 2

getSum2 : inf True Int
getSum2 = getOne + getTwo

runtest : String
runtest = show getSum2

this gave:

mjb@localhost:~/testFiles> idris testlazy -p contrib
     ____    __     _                                          
    /  _/___/ /____(_)____                                     
    / // __  / ___/ / ___/     Version 1.3.2
  _/ // /_/ / /  / (__  )      http://www.idris-lang.org/      
 /___/\__,_/_/  /_/____/       Type :? for help               

Idris is free software with ABSOLUTELY NO WARRANTY.            
For details type :warranty.
Type checking ./testlazy.idr
testlazy.idr:16:11-22:
   |
16 | runtest = show getSum2
   |           ~~~~~~~~~~~~
When checking right hand side of runtest with expected type
        String

Can't find implementation for Show (inf True Int)

Holes: Main.runtest
*testlazy> 

As you can see, the getSum function can get an 'Int' type from the sum of two 'inf True Int' types even though there was no explicit conversion.

InfList

Here is a better example from 'Type-Driven Development with Idris' chapter 11. I created a file called testlazy.idr and put this text in it:

data InfList : Type -> Type where
  (::) : (value : elim) -> Inf (InfList elim) -> (InfList elim)

countFrom : Integer -> InfList Integer
countFrom x = x :: Delay (countFrom (x + 1))

Then loaded it:

mjb@localhost> idris testlazy -p contrib
     ____    __     _                                          
    /  _/___/ /____(_)____                                     
    / // __  / ___/ / ___/     Version 1.3.2
  _/ // /_/ / /  / (__  )      http://www.idris-lang.org/      
 /___/\__,_/_/  /_/____/       Type :? for help               

Idris is free software with ABSOLUTELY NO WARRANTY.            
For details type :warranty.
Type checking ./testlazy.idr
*testlazy> countFrom 0
0 :: Delay (countFrom 1) : InfList Integer
*testlazy> 

So how can we debug using show?

Show t => Show (InfList t) where
  show ((::) v e) = "inflist " ++ (show v) ++ ":" ++ (show e)

The above definition of show would be the natural way to do it, but there are infinite values so this shows the unevaluated code:

*testlazy> show (countFrom 0)
prim__concat "inflist "
             (prim__concat "0"
                           (prim__concat ":"
                                         (Main.InfList t implementation of Prelude.Show.Show,
                                                            method show (countFrom 1)))) : String
*testlazy> 

It would be very hard to debug with this type of output, so a pragmatic solution is to just show the first 3 entries:

getPrefix : (count : Nat) -> InfList a -> List a
getPrefix Z xs = []
getPrefix (S k) (value :: xs) = value :: (getPrefix k xs)

Show t => Show (InfList t) where
  show (v :: e) = (show (getPrefix 3 (v :: e))) ++ "..."

This gives a much more readable output:

*testlazy> show (countFrom 2)
"[2, 3, 4]..." : String
*testlazy> 

 


metadata block
see also:
Correspondence about this page

This site may have errors. Don't use for critical systems.

Copyright (c) 1998-2023 Martin John Baker - All rights reserved - privacy policy.