Documentation

Lake.Build.Topological

Topological / Suspending Recursive Builder #

This module defines a recursive build function that topologically (ι.e., via a depth-first search with memoization) builds the elements of a build store.

This is called a suspending scheduler in Build systems à la carte.

Recursive Fetching #

In this section, we define the primitives that make up a builder.

@[inline, reducible]
abbrev Lake.DFetchFn (α : Type u) (β : αType v) (m : Type v → Type w) :
Type (max u w)

A dependently typed monadic fetch function.

That is, a function within the monad m and takes an input a : α describing what to fetch and and produces some output b : β a (dependently typed) or b : B (not) describing what was fetched. All build functions are fetch functions, but not all fetch functions need build something.

Equations
Instances For

    In order to nest builds / fetches within one another, we equip the monad m with a fetch function of its own.

    @[inline, reducible]
    abbrev Lake.DFetchT (α : Type u) (β : αType v) (m : Type v → Type w) (α : Type v) :
    Type (max (max w u) w)

    A transformer that equips a monad with a DFetchFn.

    Equations
    Instances For
      @[inline, reducible]
      abbrev Lake.FetchT (α : Type u) (β : Type v) (m : Type v → Type w) (α : Type v) :
      Type (max (max w u) w)

      A DFetchT that is not dependently typed.

      Equations
      Instances For

        We can then use the such a monad as the basis for a fetch function itself.

        @[inline, reducible]
        abbrev Lake.DRecFetchFn (α : Type u) (β : αType v) (m : Type v → Type w) :
        Type (max u w u)
        Equations
        Instances For
          @[inline, reducible]
          abbrev Lake.RecFetchFn (α : Type u) (β : Type v) (m : Type v → Type w) :
          Type (max u w)

          A DRecFetchFn that is not dependently typed.

          Equations
          Instances For
            @[specialize #[]]
            partial def Lake.recFetch {m : Type u → Type u_1} {α : Type u_2} {β : αType u} [∀ (α : Type u), Nonempty (m α)] (fetch : Lake.DRecFetchFn α β m) :

            A DFetchFn that provides its base DRecFetchFn with itself.

            The basic recFetch can fail to terminate in a variety of ways, it can even cycle (i.e., a fetches b which fetches a). Thus, we define the acyclicRecFetch below to guard against such cases.

            @[inline]
            def Lake.recFetchAcyclic {κ : Type u_1} {m : Type u_1 → Type u_2} {α : Type u_3} {β : αType u_1} [BEq κ] [Monad m] (keyOf : ακ) (fetch : Lake.DRecFetchFn α β (Lake.CycleT κ m)) :

            A recFetch augmented by a CycleT to guard against recursive cycles. If the set of visited keys is finite, this function should provably terminate.

            We use keyOf to the derive the unique key of a fetch from its descriptor a : α. We do this because descriptors may not be comparable and/or contain more information than necessary to determine uniqueness.

            Equations
            Instances For

              When building, we usually do not want to build the same thing twice during a single build pass. At the same time, separate builds may both wish to fetch the same thing. Thus, we need to store past build results to return them upon future fetches. This is what recFetchMemoize below does.

              @[inline]
              def Lake.recFetchMemoize {κ : Type u_1} {m : Type u_1 → Type u_2} {β : κType u_1} {α : Type u_3} [BEq κ] [Monad m] [Lake.MonadDStore κ β m] (keyOf : ακ) (fetch : Lake.DRecFetchFn α (fun a => β (keyOf a)) (Lake.CycleT κ m)) :
              Lake.DFetchFn α (fun a => β (keyOf a)) (Lake.CycleT κ m)

              recFetchAcyclic augmented with a MonadDStore to memoize fetch results and thus avoid computing the same result twice.

              Equations
              Instances For

                Building #

                In this section, we use the abstractions we have just created to define the desired topological recursive build function (a.k.a. a suspending scheduler).

                @[inline]
                def Lake.buildAcyclic {κ : Type u_1} {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [BEq κ] [Monad m] (keyOf : ακ) (a : α) (build : Lake.RecFetchFn α β (Lake.CycleT κ m)) :

                Recursively builds objects for the keys κ, avoiding cycles.

                Equations
                Instances For
                  @[inline]
                  def Lake.buildDTop {κ : Type u_1} {m : Type u_1 → Type u_2} {α : Type u_3} (β : κType u_1) [BEq κ] [Monad m] [Lake.MonadDStore κ β m] (keyOf : ακ) (a : α) (build : Lake.DRecFetchFn α (fun a => β (keyOf a)) (Lake.CycleT κ m)) :
                  ExceptT (Lake.Cycle κ) m (β (keyOf a))

                  Dependently typed version of buildTop.

                  Equations
                  Instances For
                    @[inline]
                    def Lake.buildTop {κ : Type u_1} {m : Type u_1 → Type u_2} {β : Type u_1} {α : Type u_3} [BEq κ] [Monad m] [Lake.MonadStore κ β m] (keyOf : ακ) (a : α) (build : Lake.RecFetchFn α β (Lake.CycleT κ m)) :

                    Recursively fills a MonadStore of key-object pairs by building objects topologically (ι.e., depth-first with memoization). If a cycle is detected, the list of keys traversed is thrown.

                    Equations
                    Instances For