Documentation

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

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.instEmptyCollection {m : Type u_1 → Type u_1} {α : Type u_1} :
                              Equations
                                instance MLList.instInhabited {m : Type u_1 → Type u_1} {α : Type u_1} :
                                Equations
                                  @[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
                                    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} (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
                                              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
                                                              Instances For
                                                                @[specialize #[]]
                                                                def MLList.casesM {m : 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} [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
                                                                      Instances For
                                                                        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
                                                                          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} [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
                                                                                          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} [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
                                                                                                  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 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 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} [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
                                                                                                                                  Instances For
                                                                                                                                    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
                                                                                                                                      Instances For
                                                                                                                                        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 : TypeType} {ω σ α : 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} [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} [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} [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.instMonad {m : Type u_1 → Type u_1} [Monad m] :
                                                                                                                                                                            Equations
                                                                                                                                                                              instance MLList.instAlternativeOfMonad {m : Type u_1 → Type u_1} [Monad m] :
                                                                                                                                                                              Equations
                                                                                                                                                                                instance MLList.instMonadLiftOfMonad {m : Type u_1 → Type u_1} [Monad m] :
                                                                                                                                                                                Equations