Zulip Chat Archive

Stream: general

Topic: Stating properties of the results of monads

Eric Wieser (Jan 05 2023 at 12:20):

Is there a nicer way to state "the value returned by a monad satisfies this property"? My attempt was

import control.random

universes u
variables {α : Type u} {g : Type}

/-- Chooses a random element from a list. -/
def list.random [random_gen g] : list α  rand_g g (option α)
| [] := pure none
| l@(h :: t) := do
  ulift.up i  uliftable.up $ (rand.random (fin t.length.succ) : rand_g g _),
  pure (l.nth_le i i.prop)

/-- When choosing a random element, the result is in the list. -/
lemma list.run_random_mem [random_gen g] (l : list α) (gen : g) :
  ((l.random : rand_g g (option α)).run gen⟩).fst.elim true ( l) :=
  cases l,
  { trivial },
  { exact list.nth_le_mem _ _ _ }

but this lemma feels impossible to actually use in any meaninful way

Reid Barton (Jan 05 2023 at 12:29):

In this case, returning a subtype in the first place seems like the obvious approach

Eric Wieser (Jan 05 2023 at 12:30):

That only works if you put every property you could possibly care about in the subtype though, right?

Reid Barton (Jan 05 2023 at 12:31):

Yes but in this case, there is only one such possible property.

Eric Wieser (Jan 05 2023 at 12:31):

Indeed; but presumably there are cases where this is not so

Reid Barton (Jan 05 2023 at 12:33):

It could also work more generally; try to write a refined version of the action that returns whatever subtype you're interested in at the moment

Reid Barton (Jan 05 2023 at 12:35):

I think this is effectively what you have to do in any case, since your goal is that you have some code like m >>= fun a => f a and you want, in the context of f, to also have some h : p a

Reid Barton (Jan 05 2023 at 12:36):

so you could try to rewrite this to m' >>= fun a => f a.val

Last updated: Aug 03 2023 at 10:10 UTC