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' : α.

• Why do we need functions n a -> m b which take an input of type n a when we already have a, which is an element of n a? Commented Apr 12, 2022 at 4:08
• I think it would help if you gave a practical example. It's not possible to promote a arbitrary functions of type n a -> m b to m a -> m b, so these functions must be structured in some way, e.g. maybe the are continuous or monotone. Commented Apr 12, 2022 at 4:08
• @KevinClancy I have added a concrete example of what I'm trying to do. However, I'm really unsure about my question right now as over the last two days I have been trying and failing to find a good definition of m, n and bind, aka Approx, Impl and bind.
– tom
Commented Apr 13, 2022 at 8:21
• Answer to you first question: a is often noncomputable value but n a is computable and propositionaly equal to a.
– tom
Commented Apr 13, 2022 at 9:04

• I think normal monad is recoverd if m just ignore the a : A, and n is identity on A, in Lean syntax @n A a = A. Furthermore, unit and bind ignore the the a b arguments, i e. forall a b a' b', @bind A B a b = @bind A B a' b'