## 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: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| < \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: May 14 2021 at 22:15 UTC