Zulip Chat Archive

Stream: general

Topic: algorithms in the tactic monad


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.

Scott Morrison (Sep 09 2018 at 03:52):

What am I meant to do?

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.)

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".

Scott Morrison (Sep 09 2018 at 03:55):

But that seems unlikely. :-)

Mario Carneiro (Sep 09 2018 at 03:56):

Use a lazy_list

Scott Morrison (Sep 09 2018 at 03:57):

How does that interact with working in the tactic monad?

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

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

Mario Carneiro (Sep 09 2018 at 03:59):

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

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

Scott Morrison (Sep 09 2018 at 04:02):

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

Mario Carneiro (Sep 09 2018 at 04:07):

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

Mario Carneiro (Sep 09 2018 at 04:07):

also, that in no way resembles a list

Scott Morrison (Sep 09 2018 at 04:08):

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

Simon Hudon (Sep 09 2018 at 04:08):

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

Simon Hudon (Sep 09 2018 at 04:09):

@Scott Morrison Sure, let's have a look

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

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

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

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...

Mario Carneiro (Sep 09 2018 at 04:12):

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

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]

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 !"

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

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.

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

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 :)

Mario Carneiro (Sep 09 2018 at 04:25):

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

Simon Hudon (Sep 09 2018 at 04:26):

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

Mario Carneiro (Sep 09 2018 at 04:26):

:four_leaf_clover:

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

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.

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: Dec 20 2023 at 11:08 UTC