Dependently typed monad

Question

I have came across something that looks like a dependently typed monad. I would like to know if something like this is studied and where can I find more information about it.

Let's have these two dependent type constructors

m n : {A : Type} -> (a : A) -> Type

And something like bind and unit

variables {A B : Type} {a : A} {b : B}
unit : n a -> m a
bind : m a -> (n a -> m b) -> m b
pure : (a : A) -> n a

Application:

I want to build programs that do not compute values exactly but only approximately. In this context, the expression n a would be a value of type A that is propositionally equal to a and m a is an approximation to a. Maybe, m a holds a program that can compute a up to desired precision. I'm not sure about the exact details yet.

---

Are dependently typed monad like this studied? Has someone done 'do' notation for this? Are there some caveats compared to 'do' notation for standard monads?

---

Example of imagined do notation inspired by notation in Lean.

Composition of two functions:

variables (x : m a) (g : n a -> m b) (f : n b -> m c)

do
 let (gx : n b) <- g (<- x)
 let (fgx : n c) <- f gx
 pure fgx

---

Here is an example that type checks in Lean 4(does not run as it is missing implementations). In the example:

• n = Impl and given a, usually noncomputable, then Impl a is something prepositionally equal to a but computable.
• m = Approx and given a : α, usually noncomputable, then Approx a is a function f : Nat → α such that in the limit n → ∞ the value f n converges to a

This is just a mock up, in practice Approx will be more complicated like storing additional propositions that needs to be proven(like continuity of certain functions) such that the limit actually holds.

The point of the example is to demonstrate how to use bind to build NewtonSolveFD(Newton solver that is using finite difference to approximate derivative) out of two simpler programs NewtonSolve and FiniteDiff.

noncomputable
constant inv : (ℝ → ℝ) → (ℝ → ℝ)  -- inverse of a function
noncomputable
constant ⅆ : (ℝ → ℝ) → (ℝ → ℝ)  -- derivative of a function
noncomputable
constant limit : (Nat → α) → α

def Approx {α : Type} (a : α) : Type := {f : Nat → α // limit f = a}
def Impl   {α : Type} (a : α) : Type := {a' : α // a' = a}

def bind {α β} {a : α} {b : β} (ma : Approx a) (mf : Impl a → Approx b) : Approx b := sorry

def FiniteDiff (f : ℝ → ℝ) : Approx (ⅆ f) := sorry
def NewtonSolve (f : ℝ → ℝ) (y : ℝ) (df : Impl (ⅆ f)) : Approx (inv f y) := sorry

def NewtonSolveFD (f : ℝ → ℝ) (y : ℝ) : Approx (inv f y) :=
  bind (FiniteDiff f) λ df : Impl (ⅆ f) =>
  NewtonSolve f y df

Unfortunately, the whole idea started falling apart when I tried to implement bind. There I need to apply mf to a' : α that is only approximately equal to a. Changing the type of mf to α -> Approx b is not possible as you then can't give a guarantee that f a' is approximating b if you know nothing about the input a' : α.

Answer 1

Some of the following may be relevant:

• Relative monads by Thorsten Altenkirch, James Chapman and Tarmo Uustalu.

• Flexibly graded monads and graded algebras by Dylan McDermott and Tarmo Uustalu.