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