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.

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

@[inline]

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

The empty MLList.

@[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.

@[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.

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.

@[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.

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

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

@[specialize #[]]

partial def MLList.forIn {m : Type u_1 → Type u_1} {n : Type u_1 → Type u_2} {α : Type u_1} {δ : 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.instForInMLList {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 α) α

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 u_1 → Type u_1} {α : Type u_1} [Monad m] (f : α → m (Option α)) (x : α) : MLList m α

Construct a MLList recursively. If f returns none the list will terminate.

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} {β : 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} {β : 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.

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.

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

@[specialize #[]]

def MLList.casesM {m : Type u_1 → 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.

@[specialize #[]]

def MLList.cases {m : Type u_1 → 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.)

partial def MLList.foldsM {m : Type u_1 → 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} {α : 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₁, ...].

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.

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.

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

• MLList.drop xs 0 = xs
• MLList.drop xs (Nat.succ r_1) = MLList.cases xs (fun x => MLList.nil) fun x l => MLList.drop l r_1

partial def MLList.mapM {m : Type u_1 → 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} {β : Type u_1} [Monad m] (f : α → β) (L : MLList m α) : MLList m β

Apply a function to every element of a MLList.

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.

partial def MLList.filterMapM {m : Type u_1 → 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} {β : Type u_1} [Monad m] (f : α → Option β) : MLList m α → MLList m β

Filter and transform a MLList using an Option valued function.

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.

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.

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

The infinite monadic lazy list of natural numbers.

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

Iterate through the elements of Fin n.

partial def MLList.fin.go {m : Type → Type} (n : Nat) (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.

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

partial def MLList.chunk.go {m : Type u_1 → Type u_1} {α : Type u_1} [Monad m] (n : Nat) (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.

partial def MLList.zip {m : Type u → 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} {β : 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.

partial def MLList.liftM {m : Type u_1 → Type u_1} {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} {α : 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} {α : 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.

partial def MLList.runReader {m : Type u → 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} {σ : 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.

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.

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.

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.

def MLList.foldM {m : Type u_1 → 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.

def MLList.fold {m : Type u_1 → 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.

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.

def MLList.firstM {m : Type u_1 → 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.

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.

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

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

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