``` unison id x = x structural ability Stream a where emit : a -> () Stream.foldl : (x ->{g} a ->{g} x) -> x -> '{g, Stream a} r -> '{g} x Stream.foldl f z str _ = h acc = cases { emit x -> k } -> handle !k with h (f acc x) { _ } -> acc handle !str with h z Stream.range : Nat -> Nat -> '{Stream Nat} () Stream.range m n = do f : Nat ->{Stream Nat} () f k = if k < n then emit k ; f (k+1) else () f m unique type Fold' g a b x = Fold' (x -> {g} a -> {g} x) x (x -> {g} b) unique type Fold g a b = Fold (∀ g2 r. (∀ x. Fold' g a b x -> {g2} r) -> {g2} r) Fold.fromFold' : Fold' g a b x -> Fold g a b Fold.fromFold' fold = Fold.Fold (f -> f fold) Fold.mkFold : (t -> {g} a -> {g} t) -> t -> (t -> {g} b) -> Fold g a b Fold.mkFold step init extract = Fold.fromFold' (Fold'.Fold' step init extract) folds.all : (a -> {g} Boolean) -> Fold g a Boolean folds.all predicate = Fold.mkFold (b -> a -> b && (predicate a)) true id Fold.Stream.fold : Fold g a b -> '{g, Stream a} r -> '{g} b Fold.Stream.fold = run: Fold' g a b x -> '{g, Stream a} r -> '{g} b run = cases Fold'.Fold' step init extract -> stream -> _ -> extract !(foldl step init stream) cases Fold f -> stream -> f (f' -> run f' stream) > folds.all.tests.stream = pred = n -> (Nat.gt n 2) res : 'Boolean res = Fold.Stream.fold (folds.all pred) (Stream.range 1 5) !res Universal.== false ``` ``` ucm Loading changes detected in scratch.u. I found and typechecked these definitions in scratch.u. If you do an `add` or `update`, here's how your codebase would change: ⍟ These new definitions are ok to `add`: type Fold g a b type Fold' g a b x structural ability Stream a Fold.Stream.fold : Fold g a b -> '{g, Stream a} r -> '{g} b Fold.fromFold' : Fold' g a b x -> Fold g a b Fold.mkFold : (t ->{g} a ->{g} t) -> t -> (t ->{g} b) -> Fold g a b Stream.foldl : (x ->{g} a ->{g} x) -> x -> '{g, Stream a} r -> '{g} x Stream.range : Nat -> Nat -> '{Stream Nat} () folds.all : (a ->{g} Boolean) -> Fold g a Boolean id : x -> x Now evaluating any watch expressions (lines starting with `>`)... Ctrl+C cancels. 44 | pred = n -> (Nat.gt n 2) ⧩ true ``` Tests some capabilities for catching runtime exceptions. ``` unison catcher : '{IO} () ->{IO} Result catcher act = handle tryEval act with cases { raise _ -> _ } -> Ok "caught" { _ } -> Fail "nothing to catch" tests _ = [ catcher do _ = 1/0 () , catcher '(bug "testing") , handle tryEval (do 1+1) with cases { raise _ -> _ } -> Fail "1+1 failed" { 2 } -> Ok "got the right answer" { _ } -> Fail "got the wrong answer" ] ``` ``` ucm Loading changes detected in scratch.u. I found and typechecked these definitions in scratch.u. If you do an `add` or `update`, here's how your codebase would change: ⍟ These new definitions are ok to `add`: catcher : '{IO} () ->{IO} Result tests : ∀ _. _ ->{IO} [Result] ``` ``` ucm scratch/main> add ⍟ I've added these definitions: catcher : '{IO} () ->{IO} Result tests : ∀ _. _ ->{IO} [Result] scratch/main> io.test tests New test results: 1. tests ◉ caught ◉ caught ◉ got the right answer ✅ 3 test(s) passing Tip: Use view 1 to view the source of a test. ```