Zulip Chat Archive

Stream: new members

Topic: corecursive fibonacci and factorial


view this post on Zulip SnowFox (Aug 19 2020 at 02:30):

Hello world. While experimenting with some Rosetta Code tasks to learn Lean; I've encountered a few obscure type synthesis failures. Can someone shed any light as to why and how often these issues are?

-- corecursive factorial works perfectly
def cofac := stream.corec prod.snd (λ a, b, (a + 1, a * b)) (1, 1)
-- corecursive fibonacci however, fails to synthesize the type of the first function
def cofib := stream.corec prod.fst (λ a, b, (b, a + b)) (0, 1)
-- which requires annotating it as either `(prod.fst : prod \nat \nat -> \nat)` or the
-- second lambda body as `(b + 0, a + b)` (adding `+ 0`)
-- or rewriting to use `corec_on` where `(0, 1)` is passed before the lambdas
def cofib' := stream.corec_on (0, 1) prod.fst (λ a, b, (b, a + b))

I also hit these inconsistencies.

-- `multiset` can be constructed with `{}` but `finset` cannot
#check ({} : multiset nat)
#check ({} : finset nat)
-- `finset` has `finset.empty` but `multiset` does not have `multiset.empty`

view this post on Zulip Mario Carneiro (Aug 19 2020 at 03:00):

multiset uses additive notation, so it is (0 : multiset nat)

view this post on Zulip Mario Carneiro (Aug 19 2020 at 03:01):

as for the lambda match, those require the type to be known when reading left to right. I think that from the pattern stream.corec prod.fst _ _ you can't determine that the first _ has type A x B -> C which is necessary to interpret (λ ⟨a, b⟩, ...)

view this post on Zulip SnowFox (Aug 19 2020 at 03:55):

Mario Carneiro said:

as for the lambda match, those require the type to be known when reading left to right. I think that from the pattern stream.corec prod.fst _ _ you can't determine that the first _ has type A x B -> C which is necessary to interpret (λ ⟨a, b⟩, ...)

I suspected as much; but then I tried stream.unfolds (0, 1) .. because this pushes the type of (0,1) all the way to the left, but this has the same issue.

view this post on Zulip SnowFox (Aug 19 2020 at 04:01):

Mario Carneiro said:

multiset uses additive notation, so it is (0 : multiset nat)

The weird detail there is that ({} : multiset nat) does work but ({} : finset nat) does not. I did notice \empty works for both.. but why doesn't {}?

view this post on Zulip Mario Carneiro (Aug 19 2020 at 04:01):

Because multiset doesn't have insert, I think

view this post on Zulip Mario Carneiro (Aug 19 2020 at 04:01):

insert is kind of a weird operation for multisets

view this post on Zulip Mario Carneiro (Aug 19 2020 at 04:03):

actually correction, insert works for multiset, it's just cons

view this post on Zulip Mario Carneiro (Aug 19 2020 at 04:03):

also

#check ({} : multiset )

works for me and produces ∅ : multiset ℕ

view this post on Zulip SnowFox (Aug 19 2020 at 04:04):

Right, but try finset.

view this post on Zulip Mario Carneiro (Aug 19 2020 at 04:06):

oh, the error is weirder than I thought

view this post on Zulip Mario Carneiro (Aug 19 2020 at 04:07):

#check ({} : finset )
-- invalid structure value { ... }, field 'val' was not provided
-- invalid structure value { ... }, field 'nodup' was not provided

view this post on Zulip Mario Carneiro (Aug 19 2020 at 04:07):

It has interpreted the {} as an empty structure literal

view this post on Zulip Mario Carneiro (Aug 19 2020 at 04:07):

because finset is a structure

view this post on Zulip SnowFox (Aug 19 2020 at 04:07):

Yeah.. I should have included this. Sorry.

view this post on Zulip Mario Carneiro (Aug 19 2020 at 04:07):

and multiset isn't

view this post on Zulip SnowFox (Aug 19 2020 at 04:07):

Ah!

view this post on Zulip Mario Carneiro (Aug 19 2020 at 04:08):

I should note that we don't usually write {} for the empty set

view this post on Zulip Mario Carneiro (Aug 19 2020 at 04:08):

we're all about the unicode here

view this post on Zulip SnowFox (Aug 19 2020 at 04:08):

Heh, noted.

view this post on Zulip SnowFox (Aug 19 2020 at 04:09):

Any idea why the corecursive fib doesn't work when using the unfolds variant?

view this post on Zulip SnowFox (Aug 19 2020 at 04:10):

The alpha type is as far left as it gets; yet still fails

view this post on Zulip SnowFox (Aug 19 2020 at 04:11):

Well; without being explicitly provided.

view this post on Zulip Mario Carneiro (Aug 19 2020 at 04:12):

#mwe?

view this post on Zulip SnowFox (Aug 19 2020 at 04:16):

Er, I misremembered. That was a different thing I tried. It was stream.corec_on which pushes the (0, 1) to the start and works as expected.

import data.stream
def cofib := stream.corec prod.fst (λ a, b, (b + 0, a + b)) (0, 1)
def cofib2 := stream.corec_on (0, 1) prod.fst (λ a, b, (b, a + b))
def cofib3 := stream.unfolds prod.fst (λ a, b, (b, a + b)) (0, 1)

view this post on Zulip SnowFox (Aug 19 2020 at 04:18):

The first one works because of the + 0, the second works because (0, 1) is first, and the 3rd fails along with s/unfolds/corec, so is the same problem. Except I suspected unfolds might work where corec didn't because unfolds puts all bindings on the left-hand-side of the colon in the type. Unsure if that'd make any difference. It didn't.

view this post on Zulip Mario Carneiro (Aug 19 2020 at 04:20):

here's another trick for the toolbox:

def cofib3 := stream.unfolds prod.fst (by exact λ a, b, (b, a + b)) (0, 1)

view this post on Zulip Mario Carneiro (Aug 19 2020 at 04:20):

by exact is a way to say "elaborate this last"

view this post on Zulip Mario Carneiro (Aug 19 2020 at 04:21):

also you can (should) just give more type ascriptions when this happens

view this post on Zulip SnowFox (Aug 19 2020 at 04:22):

Huh! Nice to know. Thanks. Though I'll just go with the corec_on variant for simplicity.

view this post on Zulip Mario Carneiro (Aug 19 2020 at 04:22):

def cofib3 := stream.unfolds prod.fst (λ a, b, (b, a + b) :  ×    × ) (0, 1)

view this post on Zulip SnowFox (Aug 19 2020 at 04:23):

Yeah, as I had earlier, I annotated the prod.fst part, as that was where the error was.

view this post on Zulip SnowFox (Aug 19 2020 at 04:25):

Thanks again. I need to take a break, have a headache due to insufficient sleep. TTYL. o/


Last updated: May 17 2021 at 22:15 UTC