Monadic lazy lists.

Lazy lists with "laziness" controlled by an arbitrary monad.

In an initial section we describe the specification of MLList, and provide a private unsafe implementation, and then a public opaque wrapper of this implementation, satisfying the specification.

theorem MLList.instNonemptySpec {m : Type u_1 → Type u_1} : Nonempty (MLList.Spec✝ m)

def MLList (m : Type u → Type u) (α : Type u) : Type u

A monadic lazy list, controlled by an arbitrary monad.

Equations

• MLList m α = (MLList.spec✝ m).listM α

@[inline]

def MLList.nil {m : Type u_1 → Type u_1} {α : Type u_1} : MLList m α

The empty MLList.

Equations

• MLList.nil = (MLList.spec✝ m).nil

@[inline]

def MLList.cons {α : Type u_1} {m : Type u_1 → Type u_1} : α → MLList m α → MLList m α

Constructs a MLList from head and tail.

Equations

• MLList.cons = (MLList.spec✝ m).cons

@[inline]

def MLList.thunk {m : Type u_1 → Type u_1} {α : Type u_1} : (Unit → MLList m α) → MLList m α

Embed a non-monadic thunk as a lazy list.

Equations

• MLList.thunk = (MLList.spec✝ m).thunk

def MLList.squash {m : Type u_1 → Type u_1} {α : Type u_1} : (Unit → m (MLList m α)) → MLList m α

Lift a monadic lazy list inside the monad to a monadic lazy list.

Equations

• MLList.squash = (MLList.spec✝ m).squash

@[inline]

def MLList.uncons {m : Type u → Type u} {α : Type u} [Monad m] : MLList m α → m (Option (α × MLList m α))

Deconstruct a MLList, returning inside the monad an optional pair α × MLList m α representing the head and tail of the list.

Equations

• MLList.uncons = (MLList.spec✝ m).uncons

@[inline]

def MLList.uncons? {m : Type u → Type u} {α : Type u} : MLList m α → Option (Option (α × MLList m α))

Try to deconstruct a MLList, returning an optional pair α × MLList m α representing the head and tail of the list if it is already evaluated, and none otherwise.

Equations

• MLList.uncons? = (MLList.spec✝ m).uncons?

instance MLList.instEmptyCollection {m : Type u_1 → Type u_1} {α : Type u_1} : EmptyCollection (MLList m α)

Equations

• MLList.instEmptyCollection = { emptyCollection := MLList.nil }

instance MLList.instInhabited {m : Type u_1 → Type u_1} {α : Type u_1} : Inhabited (MLList m α)

Equations

• MLList.instInhabited = { default := MLList.nil }

@[specialize #[]]

partial def MLList.forIn {m : Type u_1 → Type u_1} {n : Type u_1 → Type u_2} {α δ : Type u_1} [Monad m] [Monad n] [MonadLiftT m n] (as : MLList m α) (init : δ) (f : α → δ → n (ForInStep δ)) : n δ

The implementation of ForIn, which enables for a in L do ... notation.

instance MLList.instForInOfMonadOfMonadLiftT {m : Type u_1 → Type u_1} {n : Type u_1 → Type u_2} {α : Type u_1} [Monad m] [MonadLiftT m n] : ForIn n (MLList m α) α

Equations

• MLList.instForInOfMonadOfMonadLiftT = { forIn := fun {β : Type ?u.35} [Monad n] => MLList.forIn }

def MLList.singletonM {m : Type u_1 → Type u_1} {α : Type u_1} [Monad m] (x : m α) : MLList m α

Construct a singleton monadic lazy list from a single monadic value.

Equations

• MLList.singletonM x = MLList.squash fun (x_1 : Unit) => do let __do_lift ← x pure (MLList.cons __do_lift MLList.nil)

def MLList.singleton {m : Type u_1 → Type u_1} {α : Type u_1} [Monad m] (x : α) : MLList m α

Construct a singleton monadic lazy list from a single value.

Equations

• MLList.singleton x = MLList.singletonM (pure x)

partial def MLList.fix {m : Type u_1 → Type u_1} {α : Type u_1} [Monad m] (f : α → m α) (x : α) : MLList m α

Construct a MLList recursively. Failures from f will result in uncons failing.

partial def MLList.fix?' {m : Type (max u_1 u_2) → Type (max u_1 u_2)} {α : Type u_2} {β : Type (max u_1 u_2)} [Monad m] (f : α → m (Option (β × α))) (init : α) : MLList m β

Constructs an MLList recursively, with state in α, recording terms from β. If f returns none the list will terminate.

Variant of MLList.fix? that allows returning values of a different type.

partial def MLList.fix? {m : Type u_1 → Type u_1} {α : Type u_1} [Monad m] (f : α → m (Option α)) (x : α) : MLList m α

Constructs an MLList recursively. If f returns none the list will terminate.

Returns the initial value as the first element.

partial def MLList.iterate {m : Type u_1 → Type u_1} {α : Type u_1} [Monad m] (f : m α) : MLList m α

Construct a MLList by iteration. (m must be a stateful monad for this to be useful.)

partial def MLList.fixlWith {m : Type u → Type u} [Monad m] {α β : Type u} (f : α → m (α × List β)) (s : α) (l : List β) : MLList m β

Repeatedly apply a function f : α → m (α × List β) to an initial a : α, accumulating the elements of the resulting List β as a single monadic lazy list.

(This variant allows starting with a specified List β of elements, as well. )

def MLList.fixl {m : Type u → Type u} [Monad m] {α β : Type u} (f : α → m (α × List β)) (s : α) : MLList m β

Repeatedly apply a function f : α → m (α × List β) to an initial a : α, accumulating the elements of the resulting List β as a single monadic lazy list.

Equations

• MLList.fixl f s = MLList.fixlWith f s []

def MLList.isEmpty {m : Type u_1 → Type u_1} {α : Type u_1} [Monad m] (xs : MLList m α) : m (ULift Bool)

Compute, inside the monad, whether a MLList is empty.

Equations

• xs.isEmpty = (ULift.up ∘ Option.isSome) <$> xs.uncons

def MLList.ofList {α : Type u_1} {m : Type u_1 → Type u_1} : List α → MLList m α

Convert a List to a MLList.

Equations

• MLList.ofList [] = MLList.nil
• MLList.ofList (h :: t) = MLList.cons h (MLList.thunk fun (x : Unit) => MLList.ofList t)

def MLList.ofListM {m : Type u_1 → Type u_1} {α : Type u_1} [Monad m] : List (m α) → MLList m α

Convert a List of values inside the monad into a MLList.

Equations

• MLList.ofListM [] = MLList.nil
• MLList.ofListM (h :: t) = MLList.squash fun (x : Unit) => do let __do_lift ← h pure (MLList.cons __do_lift (MLList.ofListM t))

partial def MLList.force {m : Type u_1 → Type u_1} {α : Type u_1} [Monad m] (L : MLList m α) : m (List α)

Extract a list inside the monad from a MLList.

def MLList.asArray {m : Type u_1 → Type u_1} {α : Type u_1} [Monad m] (L : MLList m α) : m (Array α)

Extract an array inside the monad from a MLList.

Equations

• One or more equations did not get rendered due to their size.

@[specialize #[]]

def MLList.casesM {m : Type u_1 → Type u_1} {α β : Type u_1} [Monad m] (xs : MLList m α) (hnil : Unit → m (MLList m β)) (hcons : α → MLList m α → m (MLList m β)) : MLList m β

Performs a monadic case distinction on a MLList when the motive is a MLList as well.

Equations

• xs.casesM hnil hcons = MLList.squash fun (x : Unit) => do let __do_lift ← xs.uncons match __do_lift with | none => hnil () | some (x, xs) => hcons x xs

@[specialize #[]]

def MLList.cases {m : Type u_1 → Type u_1} {α β : Type u_1} [Monad m] (xs : MLList m α) (hnil : Unit → MLList m β) (hcons : α → MLList m α → MLList m β) : MLList m β

Performs a case distinction on a MLList when the motive is a MLList as well. (We need to be in a monadic context to distinguish a nil from a cons.)

Equations

• One or more equations did not get rendered due to their size.

partial def MLList.foldsM {m : Type u_1 → Type u_1} {β α : Type u_1} [Monad m] (f : β → α → m β) (init : β) (L : MLList m α) : MLList m β

Gives the monadic lazy list consisting all of folds of a function on a given initial element. Thus [a₀, a₁, ...].foldsM f b will give [b, ← f b a₀, ← f (← f b a₀) a₁, ...].

def MLList.folds {m : Type u_1 → Type u_1} {β α : Type u_1} [Monad m] (f : β → α → β) (init : β) (L : MLList m α) : MLList m β

Gives the monadic lazy list consisting all of folds of a function on a given initial element. Thus [a₀, a₁, ...].foldsM f b will give [b, f b a₀, f (f b a₀) a₁, ...].

Equations

• MLList.folds f init L = MLList.foldsM (fun (b : β) (a : α) => pure (f b a)) init L

def MLList.takeAsList {m : Type u_1 → Type u_1} {α : Type u_1} [Monad m] (xs : MLList m α) (n : Nat) : m (List α)

Take the first n elements, as a list inside the monad.

Equations

• xs.takeAsList n = MLList.takeAsList.go n [] xs

partial def MLList.takeAsList.go {m : Type u_1 → Type u_1} {α : Type u_1} [Monad m] (r : Nat) (acc : List α) (xs : MLList m α) : m (List α)

Implementation of MLList.takeAsList.

def MLList.takeAsArray {m : Type u_1 → Type u_1} {α : Type u_1} [Monad m] (xs : MLList m α) (n : Nat) : m (Array α)

Take the first n elements, as an array inside the monad.

Equations

• xs.takeAsArray n = MLList.takeAsArray.go n #[] xs

partial def MLList.takeAsArray.go {m : Type u_1 → Type u_1} {α : Type u_1} [Monad m] (r : Nat) (acc : Array α) (xs : MLList m α) : m (Array α)

Implementation of MLList.takeAsArray.

partial def MLList.take {m : Type u_1 → Type u_1} {α : Type u_1} [Monad m] (xs : MLList m α) : Nat → MLList m α

Take the first n elements.

def MLList.drop {m : Type u_1 → Type u_1} {α : Type u_1} [Monad m] (xs : MLList m α) : Nat → MLList m α

Drop the first n elements.

Equations

• xs.drop 0 = xs
• xs.drop r_1.succ = xs.cases (fun (x : Unit) => MLList.nil) fun (x : α) (l : MLList m α) => l.drop r_1

partial def MLList.mapM {m : Type u_1 → Type u_1} {α β : Type u_1} [Monad m] (f : α → m β) (xs : MLList m α) : MLList m β

Apply a function which returns values in the monad to every element of a MLList.

def MLList.map {m : Type u_1 → Type u_1} {α β : Type u_1} [Monad m] (f : α → β) (L : MLList m α) : MLList m β

Apply a function to every element of a MLList.

Equations

• MLList.map f L = MLList.mapM (fun (a : α) => pure (f a)) L

partial def MLList.filterM {m : Type u_1 → Type u_1} {α : Type u_1} [Monad m] (p : α → m (ULift Bool)) (L : MLList m α) : MLList m α

Filter a MLList using a monadic function.

def MLList.filter {m : Type u_1 → Type u_1} {α : Type u_1} [Monad m] (p : α → Bool) (L : MLList m α) : MLList m α

Filter a MLList.

Equations

• MLList.filter p L = MLList.filterM (fun (a : α) => pure { down := p a }) L

partial def MLList.filterMapM {m : Type u_1 → Type u_1} {α β : Type u_1} [Monad m] (f : α → m (Option β)) (xs : MLList m α) : MLList m β

Filter and transform a MLList using a function that returns values inside the monad.

def MLList.filterMap {m : Type u_1 → Type u_1} {α β : Type u_1} [Monad m] (f : α → Option β) : MLList m α → MLList m β

Filter and transform a MLList using an Option valued function.

Equations

• MLList.filterMap f = MLList.filterMapM fun (a : α) => pure (f a)

partial def MLList.takeWhileM {m : Type u_1 → Type u_1} {α : Type u_1} [Monad m] (f : α → m (ULift Bool)) (L : MLList m α) : MLList m α

Take the initial segment of the lazy list, until the function f first returns false.

def MLList.takeWhile {m : Type u_1 → Type u_1} {α : Type u_1} [Monad m] (f : α → Bool) : MLList m α → MLList m α

Take the initial segment of the lazy list, until the function f first returns false.

Equations

• MLList.takeWhile f = MLList.takeWhileM fun (a : α) => pure { down := f a }

partial def MLList.append {m : Type u_1 → Type u_1} {α : Type u_1} [Monad m] (xs : MLList m α) (ys : Unit → MLList m α) : MLList m α

Concatenate two monadic lazy lists.

partial def MLList.join {m : Type u_1 → Type u_1} {α : Type u_1} [Monad m] (xs : MLList m (MLList m α)) : MLList m α

Join a monadic lazy list of monadic lazy lists into a single monadic lazy list.

partial def MLList.enumFrom {m : Type u_1 → Type u_1} {α : Type u_1} [Monad m] (n : Nat) (xs : MLList m α) : MLList m (Nat × α)

Enumerate the elements of a monadic lazy list, starting at a specified offset.

def MLList.enum {m : Type u_1 → Type u_1} {α : Type u_1} [Monad m] : MLList m α → MLList m (Nat × α)

Enumerate the elements of a monadic lazy list.

Equations

• MLList.enum = MLList.enumFrom 0

def MLList.range {m : Type → Type} [Monad m] : MLList m Nat

The infinite monadic lazy list of natural numbers.

Equations

• MLList.range = MLList.fix (fun (n : Nat) => pure (n + 1)) 0

def MLList.fin {m : Type → Type} (n : Nat) : MLList m (Fin n)

Iterate through the elements of Fin n.

Equations

• MLList.fin n = MLList.fin.go n 0

partial def MLList.fin.go {m : Type → Type} (n i : Nat) : MLList m (Fin n)

Implementation of MLList.fin.

def MLList.ofArray {m : Type → Type} {α : Type} (L : Array α) : MLList m α

Convert an array to a monadic lazy list.

Equations

• MLList.ofArray L = MLList.ofArray.go L 0

partial def MLList.ofArray.go {m : Type → Type} {α : Type} (L : Array α) (i : Nat) : MLList m α

Implementation of MLList.ofArray.

def MLList.chunk {m : Type u_1 → Type u_1} {α : Type u_1} [Monad m] (L : MLList m α) (n : Nat) : MLList m (Array α)

Group the elements of a lazy list into chunks of a given size. If the lazy list is finite, the last chunk may be smaller (possibly even length 0).

Equations

• L.chunk n = MLList.chunk.go n n #[] L

partial def MLList.chunk.go {m : Type u_1 → Type u_1} {α : Type u_1} [Monad m] (n r : Nat) (acc : Array α) (M : MLList m α) : MLList m (Array α)

Implementation of MLList.chunk.

def MLList.concat {m : Type u_1 → Type u_1} {α : Type u_1} [Monad m] (L : MLList m α) (a : α) : MLList m α

Add one element to the end of a monadic lazy list.

Equations

• L.concat a = L.append fun (x : Unit) => MLList.cons a MLList.nil

partial def MLList.zip {m : Type u → Type u} {α β : Type u} [Monad m] (L : MLList m α) (M : MLList m β) : MLList m (α × β)

Take the product of two monadic lazy lists.

partial def MLList.bind {m : Type u_1 → Type u_1} {α β : Type u_1} [Monad m] (xs : MLList m α) (f : α → MLList m β) : MLList m β

Apply a function returning a monadic lazy list to each element of a monadic lazy list, joining the results.

def MLList.monadLift {m : Type u_1 → Type u_1} {α : Type u_1} [Monad m] (x : m α) : MLList m α

Convert any value in the monad to the singleton monadic lazy list.

Equations

• MLList.monadLift x = MLList.squash fun (x_1 : Unit) => do let __do_lift ← x pure (MLList.cons __do_lift MLList.nil)

partial def MLList.liftM {m n : Type u_1 → Type u_1} {α : Type u_1} [Monad m] [Monad n] [MonadLiftT m n] (L : MLList m α) : MLList n α

Lift the monad of a lazy list.

partial def MLList.runState {m : Type u → Type u} {σ α : Type u} [Monad m] (L : MLList (StateT σ m) α) (s : σ) : MLList m (α × σ)

Given a lazy list in a state monad, run it on some initial state, recording the states.

def MLList.runState' {m : Type u → Type u} {σ α : Type u} [Monad m] (L : MLList (StateT σ m) α) (s : σ) : MLList m α

Given a lazy list in a state monad, run it on some initial state.

Equations

• L.runState' s = MLList.map (fun (x : α × σ) => x.fst) (L.runState s)

partial def MLList.runReader {m : Type u → Type u} {ρ α : Type u} [Monad m] (L : MLList (ReaderT ρ m) α) (r : ρ) : MLList m α

Run a lazy list in a ReaderT monad on some fixed state.

partial def MLList.runStateRef {m : Type → Type} {ω σ α : Type} [Monad m] [MonadLiftT (ST ω) m] (L : MLList (StateRefT' ω σ m) α) (s : σ) : MLList m α

Run a lazy list in a StateRefT' monad on some initial state.

def MLList.head? {m : Type u_1 → Type u_1} {α : Type u_1} [Monad m] (L : MLList m α) : m (Option α)

Return the head of a monadic lazy list if it exists, as an Option in the monad.

Equations

• L.head? = do let __do_lift ← L.uncons pure (Option.map (fun (x : α × MLList m α) => x.fst) __do_lift)

partial def MLList.takeUpToFirstM {m : Type u_1 → Type u_1} {α : Type u_1} [Monad m] (L : MLList m α) (f : α → m (ULift Bool)) : MLList m α

Take the initial segment of the lazy list, up to and including the first place where f gives true.

def MLList.takeUpToFirst {m : Type u_1 → Type u_1} {α : Type u_1} [Monad m] (L : MLList m α) (f : α → Bool) : MLList m α

Take the initial segment of the lazy list, up to and including the first place where f gives true.

Equations

• L.takeUpToFirst f = L.takeUpToFirstM fun (a : α) => pure { down := f a }

def MLList.getLast? {m : Type u_1 → Type u_1} {α : Type u_1} [Monad m] (L : MLList m α) : m (Option α)

Gets the last element of a monadic lazy list, as an option in the monad. This will run forever if the list is infinite.

Equations

• L.getLast? = do let __do_lift ← L.uncons match __do_lift with | none => pure none | some (x, xs) => MLList.getLast?.aux x xs

partial def MLList.getLast?.aux {m : Type u_1 → Type u_1} {α : Type u_1} [Monad m] (x : α) (L : MLList m α) : m (Option α)

Implementation of MLList.aux.

def MLList.getLast! {m : Type u_1 → Type u_1} {α : Type u_1} [Monad m] [Inhabited α] (L : MLList m α) : m α

Gets the last element of a monadic lazy list, or the default value if the list is empty. This will run forever if the list is infinite.

Equations

• L.getLast! = Option.get! <$> L.getLast?

def MLList.foldM {m : Type u_1 → Type u_1} {β α : Type u_1} [Monad m] (f : β → α → m β) (init : β) (L : MLList m α) : m β

Folds a binary function across a monadic lazy list, from an initial starting value. This will run forever if the list is infinite.

Equations

• MLList.foldM f init L = do let __do_lift ← (MLList.foldsM f init L).getLast? pure (__do_lift.getD init)

def MLList.fold {m : Type u_1 → Type u_1} {β α : Type u_1} [Monad m] (f : β → α → β) (init : β) (L : MLList m α) : m β

Folds a binary function across a monadic lazy list, from an initial starting value. This will run forever if the list is infinite.

Equations

• MLList.fold f init L = MLList.foldM (fun (b : β) (a : α) => pure (f b a)) init L

def MLList.head {m : Type u_1 → Type u_1} {α : Type u_1} [Monad m] [Alternative m] (L : MLList m α) : m α

Return the head of a monadic lazy list, as a value in the monad. Fails if the list is empty.

Equations

• L.head = do let __discr ← L.uncons match __discr with | some (r, snd) => pure r | x => failure

def MLList.firstM {m : Type u_1 → Type u_1} {α β : Type u_1} [Monad m] [Alternative m] (L : MLList m α) (f : α → m (Option β)) : m β

Apply a function returning values inside the monad to a monadic lazy list, returning only the first successful result.

Equations

• L.firstM f = (MLList.filterMapM f L).head

def MLList.first {m : Type u_1 → Type u_1} {α : Type u_1} [Monad m] [Alternative m] (L : MLList m α) (p : α → Bool) : m α

Return the first value on which a predicate returns true.

Equations

• L.first p = (MLList.filter p L).head

instance MLList.instMonad {m : Type u_1 → Type u_1} [Monad m] : Monad (MLList m)

Equations

• MLList.instMonad = Monad.mk

instance MLList.instAlternativeOfMonad {m : Type u_1 → Type u_1} [Monad m] : Alternative (MLList m)

Equations

• MLList.instAlternativeOfMonad = Alternative.mk (fun {α : Type ?u.19} => MLList.nil) fun {α : Type ?u.19} => MLList.append

instance MLList.instMonadLiftOfMonad {m : Type u_1 → Type u_1} [Monad m] : MonadLift m (MLList m)

Equations

• MLList.instMonadLiftOfMonad = { monadLift := fun {α : Type ?u.18} => MLList.monadLift }