functional programming in lean

Stream: general

[grafoo]

i've been reading through chapter 1.6 but got stuck on the exercise to write a function with the type α × (β ⊕ γ) → (α × β) ⊕ (α × γ).
Don't know how much i should go into the detail, to not spoil the exercise for other but my current approach would give me either α × β : Type or α × γ : Type, depending on how things are arranged.
can't wrap my head around, how to return both choices of the sum. what am i missing here?

[Chris Bailey]

It sounds like you pretty much have the idea: how do you express either α × β : Type or α × γ as a single type?

[Yury G. Kudryashov]

Hint: use docs#Sum.inl or docs#Sum.inr depending on context.

[grafoo]

no way, this seems so wrong to me.
don't know why this wasn't obvious in the first place.
but still something feels really off looking at it.
maybe i should call it a day for now :D

thanks anyway!

[grafoo]

maybe due to the unicode symbols, it looks so much like multiplication and addition, that it seems like somehow you'd loose information when returning the products like this.

[Kyle Miller]

It's meant to be analogous to multiplication and addition. There's is a sort of distributive law for product and sum types.

[grafoo]

sure, as a concept it absolutely makes sense. but in terms of syntax, looking at it just deeply confused me.
great experience though : )

[Yury G. Kudryashov]

These two types are equivalent, see docs#Equiv.prodSumDistrib

[Yury G. Kudryashov]

A more readable version is docs#Equiv.sumProdDistrib

[grafoo]

(deleted)