Documentation

Std.Data.MLList.Basic

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} :
Equations
def MLList (m : Type u → Type u) (α : Type u) :

A monadic lazy list, controlled by an arbitrary monad.

Equations
Instances For
    @[inline]
    def MLList.nil {m : Type u_1 → Type u_1} {α : Type u_1} :
    MLList m α

    The empty MLList.

    Equations
    Instances For
      @[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
      Instances For
        @[inline]
        def MLList.thunk {m : Type u_1 → Type u_1} {α : Type u_1} :
        (UnitMLList m α)MLList m α

        Embed a non-monadic thunk as a lazy list.

        Equations
        Instances For
          def MLList.squash {m : Type u_1 → Type u_1} {α : Type u_1} :
          (Unitm (MLList m α))MLList m α

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

          Equations
          Instances For
            @[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
            Instances For
              @[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
              Instances For
                instance MLList.instEmptyCollectionMLList {m : Type u_1 → Type u_1} {α : Type u_1} :
                Equations
                • MLList.instEmptyCollectionMLList = { emptyCollection := MLList.nil }
                instance MLList.instInhabitedMLList {m : Type u_1 → Type u_1} {α : Type u_1} :
                Equations
                • MLList.instInhabitedMLList = { 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} {δ : 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 α) α
                Equations
                • MLList.instForInMLList = { forIn := fun {β : Type u_1} [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
                Instances For
                  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
                  Instances For
                    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} {β : 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.

                    Equations
                    Instances For
                      def MLList.isEmpty {m : Type u_1 → Type u_1} {α : Type u_1} [Monad m] (xs : MLList m α) :

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

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

                        Convert a List to a MLList.

                        Equations
                        Instances For
                          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
                          Instances For
                            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.
                            Instances For
                              @[specialize #[]]
                              def MLList.casesM {m : Type u_1 → Type u_1} {α : Type u_1} {β : Type u_1} [Monad m] (xs : MLList m α) (hnil : Unitm (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
                              Instances For
                                @[specialize #[]]
                                def MLList.cases {m : Type u_1 → Type u_1} {α : Type u_1} {β : Type u_1} [Monad m] (xs : MLList m α) (hnil : UnitMLList 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.
                                Instances For
                                  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₁, ...].

                                  Equations
                                  Instances For
                                    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
                                    Instances For
                                      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
                                      Instances For
                                        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 α) :
                                        NatMLList m α

                                        Take the first n elements.

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

                                        Drop the first n elements.

                                        Equations
                                        Instances For
                                          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.

                                          Equations
                                          Instances For
                                            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
                                            Instances For
                                              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.

                                              Equations
                                              Instances For
                                                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
                                                Instances For
                                                  partial def MLList.append {m : Type u_1 → Type u_1} {α : Type u_1} [Monad m] (xs : MLList m α) (ys : UnitMLList 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
                                                  Instances For
                                                    def MLList.range {m : TypeType} [Monad m] :

                                                    The infinite monadic lazy list of natural numbers.

                                                    Equations
                                                    Instances For
                                                      def MLList.fin {m : TypeType} (n : Nat) :
                                                      MLList m (Fin n)

                                                      Iterate through the elements of Fin n.

                                                      Equations
                                                      Instances For
                                                        partial def MLList.fin.go {m : TypeType} (n : Nat) (i : Nat) :
                                                        MLList m (Fin n)

                                                        Implementation of MLList.fin.

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

                                                        Convert an array to a monadic lazy list.

                                                        Equations
                                                        Instances For
                                                          partial def MLList.ofArray.go {m : TypeType} {α : 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
                                                          Instances For
                                                            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.

                                                            Equations
                                                            Instances For
                                                              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.

                                                              Equations
                                                              Instances For
                                                                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.

                                                                Equations
                                                                Instances For
                                                                  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 : TypeType} {ω : 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
                                                                  Instances For
                                                                    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
                                                                    Instances For
                                                                      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
                                                                      Instances For
                                                                        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
                                                                        Instances For
                                                                          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.

                                                                          Equations
                                                                          Instances For
                                                                            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.

                                                                            Equations
                                                                            Instances For
                                                                              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
                                                                              Instances For
                                                                                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.

                                                                                Equations
                                                                                Instances For
                                                                                  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
                                                                                  Instances For
                                                                                    instance MLList.instMonadMLList {m : Type u_1 → Type u_1} [Monad m] :
                                                                                    Equations
                                                                                    • MLList.instMonadMLList = Monad.mk
                                                                                    instance MLList.instAlternativeMLList {m : Type u_1 → Type u_1} [Monad m] :
                                                                                    Equations
                                                                                    • MLList.instAlternativeMLList = Alternative.mk (fun {α : Type u_1} => MLList.nil) fun {α : Type u_1} => MLList.append
                                                                                    instance MLList.instMonadLiftMLList {m : Type u_1 → Type u_1} [Monad m] :
                                                                                    Equations
                                                                                    • MLList.instMonadLiftMLList = { monadLift := fun {α : Type u_1} => MLList.monadLift }