<p>Some of the following may be relevant:</p>
<ul>
<li><p><a href="http://www.cs.nott.ac.uk/%7Epsztxa/publ/Relative_Monads.pdf" rel="nofollow noreferrer">Relative monads</a> by Thorsten Altenkirch, James Chapman and Tarmo Uustalu.</p>
</li>
<li><p><a href="https://dylanm.org/drafts/flexibly-graded-monads.pdf" rel="nofollow noreferrer">Flexibly graded monads and graded algebras</a> by Dylan McDermott and Tarmo Uustalu.</p>
</li>
</ul>

CC BY-SA 4.0
2022-04-07T13:10:41.897Z
I just had a quick peek to the paper. It has a definition with identical interplay of two monads, but I don't see the dependent type there. I'm maybe mixing two things together, relative monad and dependent type monad. I have to think it through a bit more.
tom
CC BY-SA 4.0
2022-04-07T20:33:03.400Z
I misread the types in your post, sorry. Now that I read them again, it's not clear to me where the monads are supposed to be. How is an ordinary monad a special case of your setup?
Andrej Bauer
CC BY-SA 4.0
2022-04-08T09:34:37.537Z
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'`
tom
CC BY-SA 4.0
2022-04-08T15:01:10.447Z
Ah yes, sorry, I am dense. I can suggest some more places to look, but you'd have to assess the references, I updated the answer with another one.
Andrej Bauer
CC BY-SA 4.0
2022-04-06T20:33:45.707Z
2022-04-08T15:01:56.020Z
2022-04-08T15:01:56.020Z
Andrej Bauer
<p>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.</p>
<p>Let's have these two dependent type constructors</p>
<pre><code>m n : {A : Type} -&gt; (a : A) -&gt; Type
</code></pre>
<p>And something like bind and unit</p>
<pre><code>variables {A B : Type} {a : A} {b : B}
unit : n a -&gt; m a
bind : m a -&gt; (n a -&gt; m b) -&gt; m b
pure : (a : A) -&gt; n a
</code></pre>
<p>Application:</p>
<p>I want to build programs that do not compute values exactly but only approximately. In this context, the expression <code>n a</code> would be a value of type <code>A</code> that is propositionally equal to <code>a</code> and <code>m a</code> is an approximation to <code>a</code>. Maybe, <code>m a</code> holds a program that can compute <code>a</code> up to desired precision. I'm not sure about the exact details yet.</p>
<hr />
<p>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?</p>
<hr />
<p>Example of imagined do notation inspired by notation in Lean.</p>
<p>Composition of two functions:</p>
<pre><code>variables (x : m a) (g : n a -&gt; m b) (f : n b -&gt; m c)

do
 let (gx : n b) &lt;- g (&lt;- x)
 let (fgx : n c) &lt;- f gx
 pure fgx

</code></pre>
<hr />
<p>Here is an example that type checks in Lean 4(does not run as it is missing implementations). In the example:</p>
<ul>
<li><code>n = Impl</code> and given <code>a</code>, usually noncomputable, then <code>Impl a</code> is something prepositionally equal to <code>a</code> but computable.</li>
<li><code>m = Approx</code> and given <code>a : α</code>, usually noncomputable, then <code>Approx a</code> is a function <code>f : Nat → α</code> such that in the limit <code>n → ∞</code> the value <code>f n</code> converges to <code>a</code></li>
</ul>
<p>This is just a mock up, in practice <code>Approx</code> will be more complicated like storing additional propositions that needs to be proven(like continuity of certain functions) such that the limit actually holds.</p>
<p>The point of the example is to demonstrate how to use <code>bind</code> to build <code>NewtonSolveFD</code>(Newton solver that is using finite difference to approximate derivative) out of two simpler programs <code>NewtonSolve</code> and <code>FiniteDiff</code>.</p>
<pre><code>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) =&gt;
  NewtonSolve f y df
</code></pre>
<p>Unfortunately, the whole idea started falling apart when I tried to implement <code>bind</code>. There I need to apply <code>mf</code> to <code>a' : α</code> that is only approximately equal to <code>a</code>. Changing the type of <code>mf</code> to <code>α -&gt; Approx b</code> is not possible as you then can't give a guarantee that <code>f a'</code> is approximating <code>b</code> if you know nothing about the input <code>a' : α</code>.</p>

CC BY-SA 4.0
2022-04-12T04:08:09.903Z
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``?
Kevin Clancy
CC BY-SA 4.0
2022-04-12T04:08:54.543Z
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.
Kevin Clancy
CC BY-SA 4.0
2022-04-13T08:21:58.170Z
@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
CC BY-SA 4.0
2022-04-13T09:04:41.960Z
Answer to you first question: `a` is often noncomputable value but `n a` is computable and propositionaly equal to `a`.
tom
<dependent-type><monad>
Dependently typed monad
tom
# Dependently typed monad

(Asked by: username_0 on 2022-04-06)

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

**Tags:** dependent-type, monad

> **Comments:**
> **username_1**: 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``?  
> **username_1**: 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.  
> **username_0**: @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`.  
> **username_0**: Answer to you first question: `a` is often noncomputable value but `n a` is computable and propositionaly equal to `a`.  

---

## 1 answers

### Answer by username_2 on 2022-04-06. Score: 4

Some of the following may be relevant:

* [Relative monads](http://www.cs.nott.ac.uk/%7Epsztxa/publ/Relative_Monads.pdf) by Thorsten Altenkirch, James Chapman and Tarmo Uustalu.
* [Flexibly graded monads and graded algebras](https://dylanm.org/drafts/flexibly-graded-monads.pdf) by Dylan McDermott and Tarmo Uustalu.

> **Comments:**
> **username_0**: I just had a quick peek to the paper. It has a definition with identical interplay of two monads, but I don't see the dependent type there. I'm maybe mixing two things together, relative monad and dependent type monad. I have to think it through a bit more.  
> **username_2**: I misread the types in your post, sorry. Now that I read them again, it's not clear to me where the monads are supposed to be. How is an ordinary monad a special case of your setup?  
> **username_0**: 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'`  
> **username_2**: Ah yes, sorry, I am dense. I can suggest some more places to look, but you'd have to assess the references, I updated the answer with another one.  

---

