The Curious Engineer

All blogs / Haskell

Donnacha Oisín Kidney's Blog

doisinkidney.com

Mainly writing about programming

HaskellFunctional / PL theoryAlgorithms / data structures

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

  1. Tries for Polynomials
  2. Monuses and Heaps

2025 1

  1. POPL Paper—Hyperfunctions: Communicating Continuations

2024 1

  1. POPL Paper—Formalising Graph Algorithms with Coinduction

2023 1

  1. POPL Paper—Algebraic Effects Meet Hoare Logic in Cubical Agda

2022 2

  1. Lazily Grouping in Haskell
  2. Depth Comonads

2021 4

  1. Weighted Search Package
  2. ICFP Paper—Algebras for Weighted Search
  3. Hyperfunctions
  4. Master's Thesis

2020 11

  1. Trees indexed by a Cayley Monoid
  2. Enumerating Trees
  3. A Queue for Effectful Breadth-First Traversals
  4. How to set up GitHub Actions for your Agda project
  5. Fun with Combinators
  6. Some More List Algorithms
  7. Presentation on Purely Functional Data Structures
  8. More Random Access Lists
  9. Another Breadth-First Traversal
  10. Typing TABA
  11. Terminating Tricky Traversals

2019 18

  1. Lazy Constructive Numbers and the Stern-Brocot Tree
  2. A Small Proof that Fin is Injective
  3. How to do Binary Random-Access Lists Simply
  4. What is Good About Haskell?
  5. Bachelor's Thesis
  6. Solving Programming Puzzles without using your Brain
  7. Deriving a Linear-Time Applicative Traversal of a Rose Tree
  8. Implicit Corecursive Queues
  9. Concatenative Programming; The Free Monoid of Programming Languages
  10. Some Tricks for List Manipulation
  11. List Syntax in Agda
  12. Probability Monads in Cubical Agda
  13. Permutations By Sorting
  14. Lazy Binary Numbers
  15. More Agda Tips
  16. Finger Trees in Agda
  17. A New Ring Solver for Agda
  18. A Binomial Urn

2018 28

  1. Drawing Trees
  2. 2018 12 29 nary uncurry lhs
  3. Balancing Scans
  4. Pure and Lazy Breadth-First Traversals of Graphs in Haskell
  5. Prime Sieves in Agda
  6. Keeping Formal Verification in Bounds
  7. A Very Simple Prime Sieve in Haskell
  8. Total Combinations
  9. Agda Beginner(-ish) Tips, Tricks, and Pitfalls
  10. Verified AVL Trees in Haskell and Agda
  11. Probabilistic Functional Programming
  12. Probability 5 Ways
  13. Scheduling Effects
  14. Rotations
  15. Breadth-First Traversals in Far Too Much Detail
  16. Breadth-First Rose Trees: Traversals and the Cofree Comonad
  17. Swapping
  18. Sorting Small Things in Haskell
  19. Type-Level Induction in Haskell
  20. 5 Cool Things You Can Do With Pattern Synonyms
  21. Strict Applicative Transformer
  22. Countdown
  23. Convolutions
  24. Rose Trees, Breadth-First
  25. Choose a random item from a list in one pass
  26. Single-Pass Huffman Coding
  27. Monadic List Functions
  28. groupBy

2017 8

  1. Unfoldl
  2. Balancing Folds
  3. Convolutions and Semirings
  4. Applicative Arithmetic
  5. Verifying Data Structures in Haskell
  6. Unparsing
  7. Fun with Recursion Schemes
  8. Constrained Applicatives

2016 6

  1. Semirings
  2. Probability Trees
  3. A Different Probability Monad
  4. Revisiting a Trie in Haskell
  5. Lenses are Static Selectors
  6. Folding Two Things at Once

2015 8

  1. 2048 in Python
  2. A Trie in Haskell
  3. Faking dependent types in Swift
  4. Using Protocols to Build a (very) Generic Deque
  5. A Trie in Swift
  6. Monty Hall
  7. Deques, Queues, and Lists in Swift with Indirect
  8. A Strategy for Swift Protocols