Zulip Chat Archive

Stream: general

Topic: algorithms in the tactic monad


view this post on Zulip Scott Morrison (Sep 09 2018 at 03:51):

I need some remedial help with functional programming.

Say I have f : X -> tactic X, and x : X. Suppose that f is possibly very expensive to compute. I would like to recursively apply f to x, and produce an iterator-like object that can traversed elsewhere in the program, in such a way that f is never needlessly computed twice.

view this post on Zulip Scott Morrison (Sep 09 2018 at 03:52):

What am I meant to do?

view this post on Zulip Scott Morrison (Sep 09 2018 at 03:53):

(Oh, and f will eventually fail, and the iterator-like object needs to be able to report termination.)

view this post on Zulip Scott Morrison (Sep 09 2018 at 03:54):

I would love to be able to package this up as merely a tactic X, whose every invocation magically produces the next element of the sequence, and handles piping the value of f f f x into the calculation of f f f f x "behind the scenes".

view this post on Zulip Scott Morrison (Sep 09 2018 at 03:55):

But that seems unlikely. :-)

view this post on Zulip Mario Carneiro (Sep 09 2018 at 03:56):

Use a lazy_list

view this post on Zulip Scott Morrison (Sep 09 2018 at 03:57):

How does that interact with working in the tactic monad?

view this post on Zulip Simon Hudon (Sep 09 2018 at 03:58):

I think something is missing in lazy_list to allow this: the function is monadic. But I think we can make a monadic lazy list

view this post on Zulip Mario Carneiro (Sep 09 2018 at 03:59):

meta inductive mllist (m : Type u → Type u) (α : Type u) : Type u
| nil : mllist
| cons : α → m mllist → mllist

view this post on Zulip Mario Carneiro (Sep 09 2018 at 03:59):

sadly this has to be meta, since it's not necessarily positive

view this post on Zulip Simon Hudon (Sep 09 2018 at 04:01):

You could do something like:

inductive mlazy_list (m : Type u -> Type u) (a : Type u) : Type (u+1)
| nil : mlazy_list
| cons (b : Type u)  : m (a x b) -> (b -> mlazy_list) -> mlazy_list

view this post on Zulip Scott Morrison (Sep 09 2018 at 04:02):

Can you explain your one, Simon? I'm not understanding how to use it. :-)

view this post on Zulip Mario Carneiro (Sep 09 2018 at 04:07):

eww, you have to package up the whole state to use that

view this post on Zulip Mario Carneiro (Sep 09 2018 at 04:07):

also, that in no way resembles a list

view this post on Zulip Scott Morrison (Sep 09 2018 at 04:08):

Mario, I'm failing to write iterates for your version... A hint?

view this post on Zulip Simon Hudon (Sep 09 2018 at 04:08):

@Mario Carneiro you have to squint and cock your head left

view this post on Zulip Simon Hudon (Sep 09 2018 at 04:09):

@Scott Morrison Sure, let's have a look

view this post on Zulip Mario Carneiro (Sep 09 2018 at 04:09):

meta inductive mllist (m : Type u → Type u) (α : Type u) : Type u
| nil {} : mllist
| cons : α → m mllist → mllist

meta def fix {m : Type u → Type u} [monad m] [alternative m]
  {α} (f : α → m α) : α → m (mllist m α)
| x := (do a ← f x, return (mllist.cons a (fix a))) <|> pure mllist.nil

view this post on Zulip Mario Carneiro (Sep 09 2018 at 04:10):

the typeclass instances are a bit of a lie since the monad and alternative instances could potentially be giving different map operations, but since there are no axioms it doesn't matter

view this post on Zulip Mario Carneiro (Sep 09 2018 at 04:11):

oh wait

meta def fix {m : Type u → Type u} [alternative m]
  {α} (f : α → m α) : α → m (mllist m α)
| x := (λ a, mllist.cons a (fix a)) <$> f x <|> pure mllist.nil

view this post on Zulip Scott Morrison (Sep 09 2018 at 04:12):

Ah, okay, I'd just worked out a version of fix, but forgotten to check for failure...

view this post on Zulip Mario Carneiro (Sep 09 2018 at 04:12):

if you skip that you have a valid infinite list representation a la haskell

view this post on Zulip Mario Carneiro (Sep 09 2018 at 04:18):

meta def f : nat → tactic nat
| 0 := tactic.failed
| (n+1) := tactic.trace n $> n

run_cmd fix f 10 -- prints only 9

meta def mllist.force {m} [monad m] {α} : mllist m α → m (list α)
| mllist.nil := pure []
| (mllist.cons a l) := list.cons a <$> (l >>= mllist.force)

run_cmd (fix f 10 >>= mllist.force >>= tactic.trace) -- prints 9,...,0 and [9, ..., 0]

view this post on Zulip Scott Morrison (Sep 09 2018 at 04:18):

Oooh, and look at that:

meta inductive mllist (m : Type u → Type u) (α : Type u) : Type u
| nil {} : mllist
| cons : α → m mllist → mllist

open mllist

meta def fix {m : Type u → Type u} [alternative m]
  {α} (f : α → m α) : α → m (mllist m α)
| x := (λ a, mllist.cons a (fix a)) <$> f x <|> pure mllist.nil

meta def g (n : ℕ) : tactic ℕ :=
do trace n,
   return (n*n)

meta def foo : tactic unit :=
do L ← fix g 2,
   mllist.cons n L ← return L,
   trace "!",
   mllist.cons n L ← L,
   trace "!",
   mllist.cons n L ← L,
   trace "!",
   skip

example : 1 = 1 :=
begin
  foo,
  refl
end

Printing: "2 ! 4 ! 16 !"

view this post on Zulip Simon Hudon (Sep 09 2018 at 04:21):

If you stay in tactics, Mario's version is simpler. Mine is getting tricky because of universes

view this post on Zulip Scott Morrison (Sep 09 2018 at 04:24):

Thanks, Simon. I'm trapped in the bottom universe anyway,, expr-munging, so I'll go with Mario's for now.

view this post on Zulip Mario Carneiro (Sep 09 2018 at 04:24):

Basically you get into the standard universe issues with coinductive types. I don't know any way to avoid packing the entire state into the type

view this post on Zulip Simon Hudon (Sep 09 2018 at 04:25):

:) good I wish I could have made something that fits in a short snippet. But now, I have to bring in a whole F-algebra which I haven't implemented yet :)

view this post on Zulip Mario Carneiro (Sep 09 2018 at 04:25):

You can mathematically reason about the entire completed infinite process, but this has poor code behavior

view this post on Zulip Simon Hudon (Sep 09 2018 at 04:26):

Doesn't Lean allow you to substitute pure code with something that will be efficient?

view this post on Zulip Mario Carneiro (Sep 09 2018 at 04:26):

:four_leaf_clover:

view this post on Zulip Simon Hudon (Sep 09 2018 at 04:29):

:) since you mention coinductive types, you mentioned bounded natural functors a while back. Now I'm thinking my current approach might be getting out of hand so I think I'll give them a try

view this post on Zulip Reid Barton (Sep 09 2018 at 10:31):

bounded natural functors

Interesting. What you need to construct the initial algebra of a functor F : Set -> Set by transfinite induction is that F is accessible, that is, F commutes with κ\kappa-filtered colimits for some regular cardinal κ\kappa. For example, FX = (S -> X) is κ\kappa-accessible if S<κ|S| < \kappa. So I guess this "bounded" condition is related. Do CS people use regular cardinals too?
I found some paper on the topic which contains a lemma which bounds the cardinality of minimal algebras and the formula involves a successor cardinal, so I guess it is the same idea.

view this post on Zulip Simon Hudon (Sep 09 2018 at 17:37):

Thanks for the attempt at giving me an introduction. I'm afraid I'm more of a noob than that when it comes to category theory


Last updated: May 14 2021 at 22:15 UTC