Last active
September 19, 2019 13:39
-
-
Save clojj/fec280b0cad87562005cdb4dcbc07168 to your computer and use it in GitHub Desktop.
Lazy lists for Unison
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
use .builtin | |
use .builtin.Nat | |
use .builtin.Int | |
use .builtin.List | |
use .builtin.Optional | |
-- TODO use Fix type | |
type Fix f = Fix (f (Fix f)) | |
type LazyList a = LazyNil | LazyCons a (() -> LazyList a) | |
f : Nat -> LazyList Nat -> LazyList Nat | |
f x xs = | |
let | |
xInc = Nat.increment x | |
next = '(f xInc xs) | |
LazyList.LazyCons xInc next | |
> xs = f 0 LazyList.LazyNil | |
lazyhead : LazyList a -> Optional a | |
lazyhead xs = | |
case xs of | |
LazyList.LazyCons f ts -> Some f | |
LazyList.LazyNil -> None | |
> lazyhead xs | |
lazytail : LazyList a -> LazyList a | |
lazytail xs = | |
case xs of | |
LazyList.LazyCons f ts -> !ts | |
LazyList.LazyNil -> LazyList.LazyNil | |
> lazytail xs | |
lazytake : Int -> LazyList Nat -> List Nat -> List Nat | |
lazytake n xs rs = | |
if n == (toInt 0) | |
then rs | |
else let | |
hd = lazyhead xs | |
rs_ = case hd of | |
Some n -> cons n rs | |
None -> rs | |
xs_ = lazytail xs | |
lazytake (n - (toInt 1)) xs_ rs_ | |
> lazytake (toInt 42 ) xs [] |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment