Is there a collection of Dependent Pearls?

[JeffreyBenjaminBrown]

Years ago, when becoming familiar with functional programming, I really enjoyed functional pearls – short, succinct solutions to problems that might seem hard until you had seen the solution.

Haskell has permitted dependent programming for years, and it keeps getting more ergonomic. Maybe the interface is still too unstable for a collection of dependent pearls to make sense yet, but I nonetheless wonder if there is already a collection of them somewhere?

[jaror]

There’s a list of functional pearls on the Haskell Wiki: Research papers/Functional pearls - HaskellWiki

But of course only a few use dependent type features of Haskell. I could find these two recent pearls:

• Stitch: the sound type-indexed type checker
• Type your matrices for great good: a Haskell library of typed matrices and applications (there is a freely accessible version here: https://davinci.di.uminho.pt/publications/type-your-matrices.pdf)