## Stream: new members

### Topic: corecursive fibonacci and factorial

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


#### Mario Carneiro (Aug 19 2020 at 03:00):

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

#### 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⟩, ...)

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

#### 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 {}?

#### Mario Carneiro (Aug 19 2020 at 04:01):

Because multiset doesn't have insert, I think

#### Mario Carneiro (Aug 19 2020 at 04:01):

insert is kind of a weird operation for multisets

#### Mario Carneiro (Aug 19 2020 at 04:03):

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

#### Mario Carneiro (Aug 19 2020 at 04:03):

also

#check ({} : multiset ℕ)


works for me and produces ∅ : multiset ℕ

#### SnowFox (Aug 19 2020 at 04:04):

Right, but try finset.

#### Mario Carneiro (Aug 19 2020 at 04:06):

oh, the error is weirder than I thought

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


#### Mario Carneiro (Aug 19 2020 at 04:07):

It has interpreted the {} as an empty structure literal

#### Mario Carneiro (Aug 19 2020 at 04:07):

because finset is a structure

#### SnowFox (Aug 19 2020 at 04:07):

Yeah.. I should have included this. Sorry.

#### Mario Carneiro (Aug 19 2020 at 04:07):

and multiset isn't

Ah!

#### Mario Carneiro (Aug 19 2020 at 04:08):

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

#### Mario Carneiro (Aug 19 2020 at 04:08):

we're all about the unicode here

Heh, noted.

#### SnowFox (Aug 19 2020 at 04:09):

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

#### SnowFox (Aug 19 2020 at 04:10):

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

#### SnowFox (Aug 19 2020 at 04:11):

Well; without being explicitly provided.

#mwe?

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


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

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


#### Mario Carneiro (Aug 19 2020 at 04:20):

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

#### Mario Carneiro (Aug 19 2020 at 04:21):

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

#### SnowFox (Aug 19 2020 at 04:22):

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

#### Mario Carneiro (Aug 19 2020 at 04:22):

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


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

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