Upgrade to Pro — share decks privately, control downloads, hide ads and more …

Folding Cheat Sheet #3

Folding Cheat Sheetย #3

The universal property of fold.

Avatar for Philip Schwarz

Philip Schwarz

April 02, 2024
Tweet

More Decks by Philip Schwarz

Other Decks in Programming

Transcript

  1. CHEAT-SHEET Folding #3 โˆถ / \ ๐’‚๐ŸŽ โˆถ / \

    ๐’‚๐Ÿ โˆถ / \ ๐’‚๐Ÿ โˆถ / \ ๐’‚๐Ÿ‘ ๐’‡ / \ ๐’‚๐ŸŽ ๐’‡ / \ ๐’‚๐Ÿ ๐’‡ / \ ๐’‚๐Ÿ ๐’‡ / \ ๐’‚๐Ÿ‘ ๐’† @philip_schwarz slides by https://fpilluminated.com/
  2. The universal property of ๐’‡๐’๐’๐’… ... For finite lists, the

    universal property of ๐’‡๐’๐’๐’… can be stated as the following equivalence between two definitions for a function ๐’ˆ that processes lists: ๐’ˆ = ๐’— โŸบ ๐’ˆ = ๐’‡๐’๐’๐’… ๐’‡ ๐’— ๐’ˆ ๐‘ฅ โˆถ ๐‘ฅ๐‘  = ๐’‡ ๐‘ฅ ๐’ˆ ๐‘ฅ๐‘  In the right-to-left direction, substituting ๐’ˆ = ๐’‡๐’๐’๐’… ๐’‡ ๐’— into the two equations for ๐’ˆ gives the recursive definition for ๐’‡๐’๐’๐’…. Conversely, in the left-to-right direction the two equations for g are precisely the assumptions required to show that ๐’ˆ = ๐’‡๐’๐’๐’… ๐’‡ ๐’— using a simple proof by induction on finite listsโ€ฆ Taken as a whole, the universal property states that for finite lists the function ๐’‡๐’๐’๐’… ๐’‡ ๐’— is not just a solution to its defining equations, but in fact the unique solutionโ€ฆ. The universal property of ๐’‡๐’๐’๐’… can be generalised to handle partial and infinite listsโ€ฆ Graham Hutton @haskelhutt ๐‘“๐‘œ๐‘™๐‘‘ :: ๐›ผ โ†’ ๐›ฝ โ†’ ๐›ฝ โ†’ ๐›ฝ โ†’ ๐›ผ โ†’ ๐›ฝ ๐‘“๐‘œ๐‘™๐‘‘ ๐‘“ ๐‘ฃ = ๐‘ฃ ๐‘“๐‘œ๐‘™๐‘‘ ๐‘“ ๐‘ฃ ๐‘ฅ โˆถ ๐‘ฅ๐‘  = ๐‘“ ๐‘ฅ ๐‘“๐‘œ๐‘™๐‘‘ ๐‘“ ๐‘ฃ ๐‘ฅ๐‘ 
  3. ๐‘” = ๐‘ฃ ๐‘” ๐‘ฅ โˆถ ๐‘ฅ๐‘  = ๐‘“ ๐‘ฅ

    ๐‘” ๐‘ฅ๐‘  ๐‘ ๐‘ข๐‘š โˆท ๐ผ๐‘›๐‘ก โ†’ ๐ผ๐‘›๐‘ก ๐‘ ๐‘ข๐‘š = 0 ๐‘ ๐‘ข๐‘š ๐‘ฅ โˆถ ๐‘ฅ๐‘  = ๐‘ฅ + ๐‘ ๐‘ข๐‘š ๐‘ฅ๐‘  ๐‘ ๐‘ข๐‘š = ๐‘“๐‘œ๐‘™๐‘‘ + 0 โŸบ ๐‘” = ๐‘“๐‘œ๐‘™๐‘‘ ๐‘“ ๐‘ฃ โŸบ ๐‘๐‘Ÿ๐‘œ๐‘‘๐‘ข๐‘๐‘ก โˆท ๐ผ๐‘›๐‘ก โ†’ ๐ผ๐‘›๐‘ก ๐‘๐‘Ÿ๐‘œ๐‘‘๐‘ข๐‘๐‘ก = 1 ๐‘๐‘Ÿ๐‘œ๐‘‘๐‘ข๐‘๐‘ก ๐‘ฅ โˆถ ๐‘ฅ๐‘  = ๐‘ฅ ร— ๐‘๐‘Ÿ๐‘œ๐‘‘๐‘ข๐‘๐‘ก ๐‘ฅ๐‘  ๐‘๐‘Ÿ๐‘œ๐‘‘๐‘ข๐‘๐‘ก = ๐‘“๐‘œ๐‘™๐‘‘ (ร—) 1 โŸบ ๐‘™๐‘’๐‘›๐‘”๐‘กโ„Ž โˆท [ฮฑ] โ†’ ๐ผ๐‘›๐‘ก ๐‘™๐‘’๐‘›๐‘”๐‘กโ„Ž [ ] = 0 ๐‘™๐‘’๐‘›๐‘”๐‘กโ„Ž ๐‘ฅ โˆถ ๐‘ฅ๐‘  = 1 + ๐‘™๐‘’๐‘›๐‘”๐‘กโ„Ž ๐‘ฅ๐‘  ๐‘™๐‘’๐‘›๐‘”๐‘กโ„Ž = ๐‘“๐‘œ๐‘™๐‘‘ (๐œ†๐‘ฅ. ๐œ†๐‘›. 1 + ๐‘›) 0 โŸบ (โงบ) โˆท [ฮฑ] โ†’ [ฮฑ] โ†’ [ฮฑ] โงบ ๐‘ฆ๐‘  = ๐‘ฆ๐‘  ๐‘ฅ โˆถ ๐‘ฅ๐‘  โงบ ๐‘ฆ๐‘  = ๐‘ฅ โˆถ (๐‘ฅ๐‘  โงบ ๐‘ฆ๐‘ ) (โงบ ๐‘ฆ๐‘ ) = ๐‘“๐‘œ๐‘™๐‘‘ โˆถ ๐‘ฆ๐‘  โŸบ concat โˆท [ ฮฑ ] โ†’ [ฮฑ] concat = concat ๐‘ฅ๐‘  โˆถ ๐‘ฅ๐‘ ๐‘  = ๐‘ฅ๐‘  โงบ ๐‘๐‘œ๐‘›๐‘๐‘Ž๐‘ก ๐‘ฅ๐‘ ๐‘  โŸบ concat = ๐‘“๐‘œ๐‘™๐‘‘ (โงบ) [ ]
  4. The Triad of ๐‘š๐‘Ž๐‘, ๐‘“๐‘–๐‘™๐‘ก๐‘’๐‘Ÿ and ๐‘“๐‘œ๐‘™๐‘‘ ๐‘š๐‘Ž๐‘ ฮป The

    ๐‘๐‘Ÿ๐‘’๐‘Ž๐‘‘, ๐‘๐‘ข๐‘ก๐‘ก๐‘’๐‘Ÿ, and ๐‘—๐‘Ž๐‘š of Functional Programming =
  5. ๐‘” = ๐‘ฃ ๐‘” ๐‘ฅ โˆถ ๐‘ฅ๐‘  = ๐‘“ ๐‘ฅ

    ๐‘” ๐‘ฅ๐‘  ๐‘š๐‘Ž๐‘ โˆท ๐›ผ โ†’ ๐›ฝ โ†’ ๐›ผ โ†’ ๐›ฝ ๐‘š๐‘Ž๐‘ ๐‘“ = ๐‘š๐‘Ž๐‘ ๐‘“ ๐‘ฅ โˆถ ๐‘ฅ๐‘  = ๐‘“ ๐‘ฅ โˆถ ๐‘š๐‘Ž๐‘ ๐‘“ ๐‘ฅ๐‘  ๐‘š๐‘Ž๐‘ ๐‘“ = ๐‘“๐‘œ๐‘™๐‘‘๐‘Ÿ ๐œ†๐‘ฅ. ๐œ†๐‘ฅ๐‘ . ๐‘“ ๐‘ฅ โˆถ ๐‘ฅ๐‘  [ ] โŸบ ๐‘“๐‘–๐‘™๐‘ก๐‘’๐‘Ÿ โˆท (๐›ผ โ†’ ๐ต๐‘œ๐‘œ๐‘™) โ†’ ๐›ผ โ†’ ๐‘Ž ๐‘“๐‘–๐‘™๐‘ก๐‘’๐‘Ÿ p = ๐‘“๐‘–๐‘™๐‘ก๐‘’๐‘Ÿ p ๐‘ฅ โˆถ ๐‘ฅ๐‘  = ๐ข๐Ÿ ๐‘ ๐‘ฅ ๐ญ๐ก๐ž๐ง ๐‘ฅ โˆถ ๐‘“๐‘–๐‘™๐‘ก๐‘’๐‘Ÿ p ๐‘ฅ๐‘  ๐ž๐ฅ๐ฌ๐ž ๐‘“๐‘–๐‘™๐‘ก๐‘’๐‘Ÿ p ๐‘ฅ๐‘  ๐‘“๐‘–๐‘™๐‘ก๐‘’๐‘Ÿ p = ๐‘“๐‘œ๐‘™๐‘‘๐‘Ÿ (๐œ†๐‘ฅ. ๐œ†๐‘ฅ๐‘ . ๐ข๐Ÿ ๐‘ ๐‘ฅ ๐ญ๐ก๐ž๐ง ๐‘ฅ โˆถ ๐‘ฅ๐‘  ๐ž๐ฅ๐ฌ๐ž ๐‘ฅ๐‘ ) [ ] โŸบ ๐‘” = ๐‘“๐‘œ๐‘™๐‘‘๐‘Ÿ ๐‘“ ๐‘ฃ โŸบ ๐‘š๐‘Ž๐‘ ฮป ๐‘“๐‘œ๐‘™๐‘‘ =