Donnacha Oisín Kidney's Blog
Mainly writing about programming
- Posts
- 90 from 17 Jul 2015 to 28 Apr 2026
- Posting
- now and then (3 in the last year)
- Kind
- personal blog
- Feed
- https://doisinkidney.com/rss.xml
2026 2
2025 1
2024 1
2023 1
2022 2
2021 4
2020 11
- Trees indexed by a Cayley Monoid
- Enumerating Trees
- A Queue for Effectful Breadth-First Traversals
- How to set up GitHub Actions for your Agda project
- Fun with Combinators
- Some More List Algorithms
- Presentation on Purely Functional Data Structures
- More Random Access Lists
- Another Breadth-First Traversal
- Typing TABA
- Terminating Tricky Traversals
2019 18
- Lazy Constructive Numbers and the Stern-Brocot Tree
- A Small Proof that Fin is Injective
- How to do Binary Random-Access Lists Simply
- What is Good About Haskell?
- Bachelor's Thesis
- Solving Programming Puzzles without using your Brain
- Deriving a Linear-Time Applicative Traversal of a Rose Tree
- Implicit Corecursive Queues
- Concatenative Programming; The Free Monoid of Programming Languages
- Some Tricks for List Manipulation
- List Syntax in Agda
- Probability Monads in Cubical Agda
- Permutations By Sorting
- Lazy Binary Numbers
- More Agda Tips
- Finger Trees in Agda
- A New Ring Solver for Agda
- A Binomial Urn
2018 28
- Drawing Trees
- 2018 12 29 nary uncurry lhs
- Balancing Scans
- Pure and Lazy Breadth-First Traversals of Graphs in Haskell
- Prime Sieves in Agda
- Keeping Formal Verification in Bounds
- A Very Simple Prime Sieve in Haskell
- Total Combinations
- Agda Beginner(-ish) Tips, Tricks, and Pitfalls
- Verified AVL Trees in Haskell and Agda
- Probabilistic Functional Programming
- Probability 5 Ways
- Scheduling Effects
- Rotations
- Breadth-First Traversals in Far Too Much Detail
- Breadth-First Rose Trees: Traversals and the Cofree Comonad
- Swapping
- Sorting Small Things in Haskell
- Type-Level Induction in Haskell
- 5 Cool Things You Can Do With Pattern Synonyms
- Strict Applicative Transformer
- Countdown
- Convolutions
- Rose Trees, Breadth-First
- Choose a random item from a list in one pass
- Single-Pass Huffman Coding
- Monadic List Functions
- groupBy