Folding Cheat Sheet #1

Folding over recursively defined data structures for natural numbers and lists.

Keywords: folding, list, lists, nat, natural numbers, recursive datatype, recursive function, right fold.

Transcript

1. CHEAT-SHEET Folding #1 ∶ / \ 𝒂𝟎 ∶ / \ 𝒂𝟏 ∶ / \ 𝒂𝟐 ∶ / \ 𝒂𝟑 𝒇 / \ 𝒂𝟎 𝒇 / \ 𝒂𝟏 𝒇 / \ 𝒂𝟐 𝒇 / \ 𝒂𝟑 𝒆 @philip_schwarz slides by https://fpilluminated.com/
2. 𝐝𝐚𝐭𝐚 𝑵𝒂𝒕 = 𝒁𝒆𝒓𝒐 | 𝑺𝒖𝒄𝒄 𝑵𝒂𝒕 𝐝𝐚𝐭𝐚 𝑳𝒊𝒔𝒕 α = 𝑵𝒊𝒍 | 𝑪𝒐𝒏𝒔 α (𝑳𝒊𝒔𝒕 α) 𝑓 :: 𝑵𝒂𝒕 → 𝛼 𝑓 𝒁𝒆𝒓𝒐 = 𝑐 𝑓 𝑺𝒖𝒄𝒄 𝑛 = ℎ 𝑓 𝑛 𝑓𝑜𝑙𝑑𝑛 ∷ 𝛼 → 𝛼 → 𝛼 → 𝑵𝒂𝒕 → 𝛼 𝑓𝑜𝑙𝑑𝑛 ℎ 𝑐 𝒁𝒆𝒓𝒐 = 𝑐 𝑓𝑜𝑙𝑑𝑛 ℎ 𝑐 𝑺𝒖𝒄𝒄 𝑛 = ℎ 𝑓𝑜𝑙𝑑𝑛 ℎ 𝑐 𝑛 𝑚 + 𝑛 = 𝑓𝑜𝑙𝑑𝑛 𝑺𝒖𝒄𝒄 𝑚 𝑛 𝑚 × 𝑛 = 𝑓𝑜𝑙𝑑𝑛 𝜆𝑥. 𝑥 + 𝑚 𝒁𝒆𝒓𝒐 𝑛 𝑚 ↑ 𝑛 = 𝑓𝑜𝑙𝑑𝑛 𝜆𝑥. 𝑥 × 𝑚 𝑺𝒖𝒄𝒄 𝒁𝒆𝒓𝒐 𝑛 + ∷ 𝑵𝒂𝒕 → 𝑵𝒂𝒕 → 𝑵𝒂𝒕 𝑚 + 𝒁𝒆𝒓𝒐 = 𝑚 𝑚 + 𝑺𝒖𝒄𝒄 𝑛 = 𝑺𝒖𝒄𝒄 𝑚 + 𝑛 (×) ∷ 𝑵𝒂𝒕 → 𝑵𝒂𝒕 → 𝑵𝒂𝒕 𝑚 × 𝒁𝒆𝒓𝒐 = 𝒁𝒆𝒓𝒐 𝑚 × 𝑺𝒖𝒄𝒄 𝑛 = 𝑚 × 𝑛 + 𝑚 (↑) ∷ 𝑵𝒂𝒕 → 𝑵𝒂𝒕 → 𝑵𝒂𝒕 𝑚 ↑ 𝒁𝒆𝒓𝒐 = 𝑺𝒖𝒄𝒄 𝒁𝒆𝒓𝒐 𝑚 ↑ 𝑺𝒖𝒄𝒄 𝑛 = 𝑚 ↑ 𝑛 × 𝑚 𝑓𝑜𝑙𝑑𝑟 ∷ 𝛼 → 𝛽 → 𝛽 → 𝛽 → 𝛼 → 𝛽 𝑓𝑜𝑙𝑑𝑟 𝑓 𝑏 𝑵𝒊𝒍 = 𝑏 𝑓𝑜𝑙𝑑𝑟 𝑓 𝑏 (𝑪𝒐𝒏𝒔 𝑥 𝑥𝑠) = 𝑓 𝑥 𝑓𝑜𝑙𝑑𝑟 𝑓 𝑏 𝑥𝑠 𝑓 :: 𝑳𝒊𝒔𝒕 𝛼 → 𝛽 𝑓 𝑵𝒊𝒍 = 𝑐 𝑓 𝑪𝒐𝒏𝒔 𝑥 𝑥𝑠 = ℎ 𝑥 (𝑓 𝑥𝑠) 𝑠𝑢𝑚 ∷ 𝑳𝒊𝒔𝒕 𝑵𝒂𝒕 → 𝑵𝒂𝒕 𝑠𝑢𝑚 𝑵𝒊𝒍 = 𝒁𝒆𝒓𝒐 𝑠𝑢𝑚 𝑪𝒐𝒏𝒔 𝑥 𝑥𝑠 = 𝑥 + (𝑠𝑢𝑚 𝑥𝑠) 𝑎𝑝𝑝𝑒𝑛𝑑 ∷ 𝑳𝒊𝒔𝒕 𝛼 → 𝑳𝒊𝒔𝒕 𝛼 → 𝑳𝒊𝒔𝒕 𝛼 𝑎𝑝𝑝𝑒𝑛𝑑 𝑵𝒊𝒍 𝑦𝑠 = 𝑦𝑠 𝑎𝑝𝑝𝑒𝑛𝑑 𝑪𝒐𝒏𝒔 𝑥 𝑥𝑠 𝑦𝑠 = 𝑪𝒐𝒏𝒔 𝑥 (𝑎𝑝𝑝𝑒𝑛𝑑 𝑥𝑠 𝑦𝑠) 𝑙𝑒𝑛𝑔𝑡ℎ ∷ 𝑳𝒊𝒔𝒕 𝛼 → 𝑵𝒂𝒕 𝑙𝑒𝑛𝑔𝑡ℎ 𝑵𝒊𝒍 = 𝒁𝒆𝒓𝒐 𝑙𝑒𝑛𝑔𝑡ℎ 𝑪𝒐𝒏𝒔 𝑥 𝑥𝑠 = 𝑺𝒖𝒄𝒄 𝒁𝒆𝒓𝒐 + (𝑙𝑒𝑛𝑔𝑡ℎ 𝑥𝑠) 𝑠𝑢𝑚 𝑥𝑠 = 𝑓𝑜𝑙𝑑𝑟 + 𝒁𝒆𝒓𝒐 𝑥𝑠 𝑙𝑒𝑛𝑔𝑡ℎ 𝑥𝑠 = 𝑓𝑜𝑙𝑑𝑟 𝜆𝑥. 𝜆𝑛. 𝑛 + 𝑺𝒖𝒄𝒄 𝒁𝒆𝒓𝒐 𝒁𝒆𝒓𝒐 𝑥𝑠 𝑎𝑝𝑝𝑒𝑛𝑑 𝑥𝑠 𝑦𝑠 = 𝑓𝑜𝑙𝑑𝑟 𝑪𝒐𝒏𝒔 𝑦𝑠 𝑥𝑠 Common pattern for many recursive functions over 𝑵𝒂𝒕 : Common pattern for many recursive functions over 𝑳𝒊𝒔𝒕: 𝑐 :: 𝛼 ℎ :: 𝛼 → 𝛼 𝑐 :: 𝛽 ℎ :: 𝛼 → 𝛽 Three examples of such functions: Three examples of such functions: The common pattern can be captured in a function: The common pattern can be captured in a function: The three sample functions implemented using 𝑓𝑜𝑙𝑑𝑛: The three sample functions implemented using 𝑓𝑜𝑙𝑑𝑟:
3. https://fpilluminated.com/ inspired by