4
$\begingroup$

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

$\endgroup$
4
  • $\begingroup$ 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? $\endgroup$ Apr 12, 2022 at 4:08
  • $\begingroup$ 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. $\endgroup$ Apr 12, 2022 at 4:08
  • $\begingroup$ @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. $\endgroup$
    – tom
    Apr 13, 2022 at 8:21
  • $\begingroup$ Answer to you first question: a is often noncomputable value but n a is computable and propositionaly equal to a. $\endgroup$
    – tom
    Apr 13, 2022 at 9:04

1 Answer 1

4
$\begingroup$

Some of the following may be relevant:

$\endgroup$
4
  • $\begingroup$ 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. $\endgroup$
    – tom
    Apr 7, 2022 at 13:10
  • $\begingroup$ 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? $\endgroup$ Apr 7, 2022 at 20:33
  • $\begingroup$ 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' $\endgroup$
    – tom
    Apr 8, 2022 at 9:34
  • 1
    $\begingroup$ 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. $\endgroup$ Apr 8, 2022 at 15:01

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.