41554 blogs · [ { "id": "01a0876e-7581-7198-ac47-26f2e8a76a42", "title": "Tries for Polynomials", "url": "https://doisinkidney.com/posts/2026-04-28-poly-trie.html", "published_at": null }, { "id": "01a0876e-7581-7198-ac47-26f2e8a78ca9", "title": "Monuses and Heaps", "url": "https://doisinkidney.com/posts/2026-03-03-monus-heaps.html", "published_at": null }, { "id": "01a0876e-7581-7198-ac47-26f2e9782c46", "title": "POPL Paper—Hyperfunctions: Communicating Continuations", "url": "https://doisinkidney.com/posts/2025-11-18-hyperfunctions.html", "published_at": null }, { "id": "01a0876e-7581-7198-ac47-26f2e9e8c6bd", "title": "POPL Paper—Formalising Graph Algorithms with Coinduction", "url": "https://doisinkidney.com/posts/2024-11-08-formalising-graphs-coinduction.html", "published_at": null }, { "id": "01a0876e-7581-7198-ac47-26f2eac0a9b1", "title": "POPL Paper—Algebraic Effects Meet Hoare Logic in Cubical Agda", "url": "https://doisinkidney.com/posts/2023-11-07-algebraic-free-monads.html", "published_at": null }, { "id": "01a0876e-7581-7198-ac47-26f2ebbf3da1", "title": "Lazily Grouping in Haskell", "url": "https://doisinkidney.com/posts/2022-10-17-lazy-group-on.html", "published_at": null }, { "id": "01a0876e-7581-7198-ac47-26f2ec4492fd", "title": "Depth Comonads", "url": "https://doisinkidney.com/posts/2022-05-03-depth-comonads.html", "published_at": null }, { "id": "01a0876e-7581-7198-ac47-26f2ece29c9e", "title": "Weighted Search Package", "url": "https://doisinkidney.com/posts/2021-08-29-weighted-search-package.html", "published_at": null }, { "id": "01a0876e-7581-7198-ac47-26f2ecfb8207", "title": "ICFP Paper—Algebras for Weighted Search", "url": "https://doisinkidney.com/posts/2021-06-21-icfp-paper.html", "published_at": null }, { "id": "01a0876e-7581-7198-ac47-26f2edf25c09", "title": "Hyperfunctions", "url": "https://doisinkidney.com/posts/2021-03-14-hyperfunctions.html", "published_at": null }, { "id": "01a0876e-7581-7198-ac47-26f2edf91d82", "title": "Master's Thesis", "url": "https://doisinkidney.com/posts/2021-01-04-masters-thesis.html", "published_at": null }, { "id": "01a0876e-7581-7198-ac47-26f2ee8c3bbb", "title": "Trees indexed by a Cayley Monoid", "url": "https://doisinkidney.com/posts/2020-12-27-cayley-trees.html", "published_at": null }, { "id": "01a0876e-7581-7198-ac47-26f2eee75e30", "title": "Enumerating Trees", "url": "https://doisinkidney.com/posts/2020-12-14-enumerating-trees.html", "published_at": null }, { "id": "01a0876e-7581-7198-ac47-26f2ef902273", "title": "A Queue for Effectful Breadth-First Traversals", "url": "https://doisinkidney.com/posts/2020-11-23-applicative-queue.html", "published_at": null }, { "id": "01a0876e-7581-7198-ac47-26f2efc66021", "title": "How to set up GitHub Actions for your Agda project", "url": "https://doisinkidney.com/posts/2020-11-18-agda-github-action.html", "published_at": null }, { "id": "01a0876e-7581-7198-ac47-26f2efe42bf5", "title": "Fun with Combinators", "url": "https://doisinkidney.com/posts/2020-10-17-ski.html", "published_at": null }, { "id": "01a0876e-7581-7198-ac47-26f2f0c56ca6", "title": "Some More List Algorithms", "url": "https://doisinkidney.com/posts/2020-08-22-some-more-list-algorithms.html", "published_at": null }, { "id": "01a0876e-7581-7198-ac47-26f2f0e41738", "title": "Presentation on Purely Functional Data Structures", "url": "https://doisinkidney.com/posts/2020-05-19-purely-functional-data-structures-slides.html", "published_at": null }, { "id": "01a0876e-7581-7198-ac47-26f2f187fe43", "title": "More Random Access Lists", "url": "https://doisinkidney.com/posts/2020-05-02-more-random-access-lists.html", "published_at": null }, { "id": "01a0876e-7581-7198-ac47-26f2f1dae34b", "title": "Another Breadth-First Traversal", "url": "https://doisinkidney.com/posts/2020-02-20-final-bft.html", "published_at": null }, { "id": "01a0876e-7581-7198-ac47-26f2f2a0d660", "title": "Typing TABA", "url": "https://doisinkidney.com/posts/2020-02-15-taba.html", "published_at": null }, { "id": "01a0876e-7581-7198-ac47-26f2f37e5762", "title": "Terminating Tricky Traversals", "url": "https://doisinkidney.com/posts/2020-01-29-terminating-tricky-traversals.html", "published_at": null }, { "id": "01a0876e-7581-7198-ac47-26f2f3c27a62", "title": "Lazy Constructive Numbers and the Stern-Brocot Tree", "url": "https://doisinkidney.com/posts/2019-12-14-stern-brocot.html", "published_at": null }, { "id": "01a0876e-7581-7198-ac47-26f2f45f09c6", "title": "A Small Proof that Fin is Injective", "url": "https://doisinkidney.com/posts/2019-11-15-small-proof-fin-inj.html", "published_at": null }, { "id": "01a0876e-7581-7198-ac47-26f2f48043fd", "title": "How to do Binary Random-Access Lists Simply", "url": "https://doisinkidney.com/posts/2019-11-02-how-to-binary-random-access-list.html", "published_at": null }, { "id": "01a0876e-7581-7198-ac47-26f2f4de3219", "title": "What is Good About Haskell?", "url": "https://doisinkidney.com/posts/2019-10-02-what-is-good-about-haskell.html", "published_at": null }, { "id": "01a0876e-7582-7116-b74e-3525543fa916", "title": "Bachelor's Thesis", "url": "https://doisinkidney.com/posts/2019-07-14-bsc-thesis.html", "published_at": null }, { "id": "01a0876e-7582-7116-b74e-352554b36941", "title": "Solving Programming Puzzles without using your Brain", "url": "https://doisinkidney.com/posts/2019-06-04-solving-puzzles-without-your-brain.html", "published_at": null }, { "id": "01a0876e-7582-7116-b74e-3525554dd71e", "title": "Deriving a Linear-Time Applicative Traversal of a Rose Tree", "url": "https://doisinkidney.com/posts/2019-05-28-linear-phases.html", "published_at": null }, { "id": "01a0876e-7582-7116-b74e-352555a76475", "title": "Implicit Corecursive Queues", "url": "https://doisinkidney.com/posts/2019-05-14-corecursive-implicit-queues.html", "published_at": null }, { "id": "01a0876e-7582-7116-b74e-352555c89a46", "title": "Concatenative Programming; The Free Monoid of Programming Languages", "url": "https://doisinkidney.com/posts/2019-05-11-concatenative-free.html", "published_at": null }, { "id": "01a0876e-7582-7116-b74e-352556c564ab", "title": "Some Tricks for List Manipulation", "url": "https://doisinkidney.com/posts/2019-05-08-list-manipulation-tricks.html", "published_at": null }, { "id": "01a0876e-7582-7116-b74e-35255779182d", "title": "List Syntax in Agda", "url": "https://doisinkidney.com/posts/2019-04-20-ListSyntax.html", "published_at": null }, { "id": "01a0876e-7582-7116-b74e-352557ca5d02", "title": "Probability Monads in Cubical Agda", "url": "https://doisinkidney.com/posts/2019-04-17-cubical-probability.html", "published_at": null }, { "id": "01a0876e-7582-7116-b74e-352558c5b709", "title": "Permutations By Sorting", "url": "https://doisinkidney.com/posts/2019-03-24-permutations-by-sorting.html", "published_at": null }, { "id": "01a0876e-7582-7116-b74e-3525591bffd0", "title": "Lazy Binary Numbers", "url": "https://doisinkidney.com/posts/2019-03-21-binary-logic-search.html", "published_at": null }, { "id": "01a0876e-7582-7116-b74e-352559950d6f", "title": "More Agda Tips", "url": "https://doisinkidney.com/posts/2019-03-14-more-agda-tips.html", "published_at": null }, { "id": "01a0876e-7582-7116-b74e-35255a3b105b", "title": "Finger Trees in Agda", "url": "https://doisinkidney.com/posts/2019-02-25-agda-fingertrees.html", "published_at": null }, { "id": "01a0876e-7582-7116-b74e-35255b1154d5", "title": "A New Ring Solver for Agda", "url": "https://doisinkidney.com/posts/2019-01-25-agda-ring-solver.html", "published_at": null }, { "id": "01a0876e-7582-7116-b74e-35255b21b1fe", "title": "A Binomial Urn", "url": "https://doisinkidney.com/posts/2019-01-15-binomial-urn.html", "published_at": null }, { "id": "01a0876e-7582-7116-b74e-35255b755167", "title": "Drawing Trees", "url": "https://doisinkidney.com/posts/2018-12-30-drawing-trees-lhs.html", "published_at": null }, { "id": "01a0876e-7582-7116-b74e-35255b7a13ea", "title": "liftAN", "url": "https://doisinkidney.com/posts/2018-12-29-nary-uncurry-lhs.html", "published_at": null }, { "id": "01a0876e-7582-7116-b74e-35255bc3f6a5", "title": "Balancing Scans", "url": "https://doisinkidney.com/posts/2018-12-21-balancing-scans.html", "published_at": null }, { "id": "01a0876e-7582-7116-b74e-35255c4ab905", "title": "Pure and Lazy Breadth-First Traversals of Graphs in Haskell", "url": "https://doisinkidney.com/posts/2018-12-18-traversing-graphs.html", "published_at": null }, { "id": "01a0876e-7582-7116-b74e-35255d3336a0", "title": "Prime Sieves in Agda", "url": "https://doisinkidney.com/posts/2018-12-14-primes-in-agda.html", "published_at": null }, { "id": "01a0876e-7582-7116-b74e-35255d533406", "title": "Keeping Formal Verification in Bounds", "url": "https://doisinkidney.com/posts/2018-11-20-fast-verified-structures.html", "published_at": null }, { "id": "01a0876e-7582-7116-b74e-35255e03706f", "title": "A Very Simple Prime Sieve in Haskell", "url": "https://doisinkidney.com/posts/2018-11-10-a-very-simple-prime-sieve.html", "published_at": null }, { "id": "01a0876e-7582-7116-b74e-35255e4fbded", "title": "Total Combinations", "url": "https://doisinkidney.com/posts/2018-10-16-total-combinations.html", "published_at": null }, { "id": "01a0876e-7582-7116-b74e-35255f09dfa3", "title": "Agda Beginner(-ish) Tips, Tricks, and Pitfalls", "url": "https://doisinkidney.com/posts/2018-09-20-agda-tips.html", "published_at": null }, { "id": "01a0876e-7582-7116-b74e-35255fa941c2", "title": "Verified AVL Trees in Haskell and Agda", "url": "https://doisinkidney.com/posts/2018-07-30-verified-avl.html", "published_at": null }, { "id": "01a0876e-7582-7116-b74e-35256086057d", "title": "Probabilistic Functional Programming", "url": "https://doisinkidney.com/posts/2018-07-17-probability-presentation.html", "published_at": null }, { "id": "01a0876e-7582-7116-b74e-352560ddaf73", "title": "Probability 5 Ways", "url": "https://doisinkidney.com/posts/2018-06-30-probability-5-ways.html", "published_at": null }, { "id": "01a0876e-7582-7116-b74e-352560e2d36a", "title": "Scheduling Effects", "url": "https://doisinkidney.com/posts/2018-06-23-scheduling-effects.html", "published_at": null }, { "id": "01a0876e-7582-7116-b74e-352561b0a5a5", "title": "Rotations", "url": "https://doisinkidney.com/posts/2018-06-03-rotations-lhs.html", "published_at": null }, { "id": "01a0876e-7582-7116-b74e-352562a9560d", "title": "Breadth-First Traversals in Far Too Much Detail", "url": "https://doisinkidney.com/posts/2018-06-03-breadth-first-traversals-in-too-much-detail.html", "published_at": null }, { "id": "01a0876e-7582-7116-b74e-3525639db97d", "title": "Breadth-First Rose Trees: Traversals and the Cofree Comonad", "url": "https://doisinkidney.com/posts/2018-06-01-rose-trees-breadth-first-traversing.html", "published_at": null }, { "id": "01a0876e-7582-7116-b74e-3525644d9498", "title": "Swapping", "url": "https://doisinkidney.com/posts/2018-05-30-swapping-lhs.html", "published_at": null }, { "id": "01a0876e-7582-7116-b74e-352565081070", "title": "Sorting Small Things in Haskell", "url": "https://doisinkidney.com/posts/2018-05-06-sorting-small.html", "published_at": null }, { "id": "01a0876e-7582-7116-b74e-352565aff438", "title": "Type-Level Induction in Haskell", "url": "https://doisinkidney.com/posts/2018-05-05-induction.html", "published_at": null }, { "id": "01a0876e-7582-7116-b74e-352565ea6b17", "title": "5 Cool Things You Can Do With Pattern Synonyms", "url": "https://doisinkidney.com/posts/2018-04-12-pattern-synonyms.html", "published_at": null }, { "id": "01a0876e-7582-7116-b74e-352566953815", "title": "Strict Applicative Transformer", "url": "https://doisinkidney.com/posts/2018-03-21-strictify-lhs.html", "published_at": null }, { "id": "01a0876e-7582-7116-b74e-352566d14b3e", "title": "Countdown", "url": "https://doisinkidney.com/posts/2018-03-20-countdown.html", "published_at": null }, { "id": "01a0876e-7582-7116-b74e-35256707842c", "title": "Convolutions", "url": "https://doisinkidney.com/posts/2018-03-19-convolutions-lhs.html", "published_at": null }, { "id": "01a0876e-7582-7116-b74e-3525674d77bb", "title": "Rose Trees, Breadth-First", "url": "https://doisinkidney.com/posts/2018-03-17-rose-trees-breadth-first.html", "published_at": null }, { "id": "01a0876e-7582-7116-b74e-352567642db1", "title": "Choose a random item from a list in one pass", "url": "https://doisinkidney.com/posts/2018-03-15-one-pass-choose-lhs.html", "published_at": null }, { "id": "01a0876e-7582-7116-b74e-3525676a013b", "title": "Single-Pass Huffman Coding", "url": "https://doisinkidney.com/posts/2018-02-17-single-pass-huffman.html", "published_at": null }, { "id": "01a0876e-7582-7116-b74e-35256869381f", "title": "Monadic List Functions", "url": "https://doisinkidney.com/posts/2018-02-11-monadic-list.functions.html", "published_at": null }, { "id": "01a0876e-7582-7116-b74e-352568e6b2bb", "title": "groupBy", "url": "https://doisinkidney.com/posts/2018-01-07-groupBy.html", "published_at": null }, { "id": "01a0876e-7582-7116-b74e-35256975522a", "title": "Unfoldl", "url": "https://doisinkidney.com/posts/2017-12-14-unfoldl-lhs.html", "published_at": null }, { "id": "01a0876e-7582-7116-b74e-352569f5ea2c", "title": "Balancing Folds", "url": "https://doisinkidney.com/posts/2017-10-30-balancing-folds.html", "published_at": null }, { "id": "01a0876e-7582-7116-b74e-35256a28fba9", "title": "Convolutions and Semirings", "url": "https://doisinkidney.com/posts/2017-10-13-convolutions-and-semirings.html", "published_at": null }, { "id": "01a0876e-7582-7116-b74e-35256a5caf9e", "title": "Applicative Arithmetic", "url": "https://doisinkidney.com/posts/2017-09-25-applicative-arithmetic.html", "published_at": null }, { "id": "01a0876e-7582-7116-b74e-35256a7f4372", "title": "Verifying Data Structures in Haskell", "url": "https://doisinkidney.com/posts/2017-04-23-verifying-data-structures-in-haskell-lhs.html", "published_at": null }, { "id": "01a0876e-7582-7116-b74e-35256aca0a95", "title": "Unparsing", "url": "https://doisinkidney.com/posts/2017-04-01-unparsing-lhs.html", "published_at": null }, { "id": "01a0876e-7582-7116-b74e-35256b9a5e9f", "title": "Fun with Recursion Schemes", "url": "https://doisinkidney.com/posts/2017-03-30-fun-with-recursion-schemes.html", "published_at": null }, { "id": "01a0876e-7582-7116-b74e-35256be489f5", "title": "Constrained Applicatives", "url": "https://doisinkidney.com/posts/2017-03-08-constrained-applicatives.html", "published_at": null }, { "id": "01a0876e-7582-7116-b74e-35256cc88712", "title": "Semirings", "url": "https://doisinkidney.com/posts/2016-11-17-semirings-lhs.html", "published_at": null }, { "id": "01a0876e-7582-7116-b74e-35256d211428", "title": "Probability Trees", "url": "https://doisinkidney.com/posts/2016-09-30-prob-trees-lhs.html", "published_at": null }, { "id": "01a0876e-7582-7116-b74e-35256df7094f", "title": "A Different Probability Monad", "url": "https://doisinkidney.com/posts/2016-09-27-odds-lhs.html", "published_at": null }, { "id": "01a0876e-7582-7116-b74e-35256e161916", "title": "Revisiting a Trie in Haskell", "url": "https://doisinkidney.com/posts/2016-09-26-revisiting-trie-lhs.html", "published_at": null }, { "id": "01a0876e-7582-7116-b74e-35256e4381d5", "title": "Lenses are Static Selectors", "url": "https://doisinkidney.com/posts/2016-06-16-lenses-are-static-selectors.html", "published_at": null }, { "id": "01a0876e-7582-7116-b74e-35256f21af24", "title": "Folding Two Things at Once", "url": "https://doisinkidney.com/posts/2016-04-17-folding-two-at-once.html", "published_at": null }, { "id": "01a0876e-7582-7116-b74e-35256f5d94b0", "title": "2048 in Python", "url": "https://doisinkidney.com/posts/2015-10-20-2048.html", "published_at": null }, { "id": "01a0876e-7582-7116-b74e-35256fa38a8e", "title": "A Trie in Haskell", "url": "https://doisinkidney.com/posts/2015-10-06-haskell-trie-lhs.html", "published_at": null }, { "id": "01a0876e-7582-7116-b74e-35256fb8b9e1", "title": "Faking dependent types in Swift", "url": "https://doisinkidney.com/posts/2015-09-06-dependent-types.html", "published_at": null }, { "id": "01a0876e-7582-7116-b74e-35257040d658", "title": "Using Protocols to Build a (very) Generic Deque", "url": "https://doisinkidney.com/posts/2015-08-24-generic-deque.html", "published_at": null }, { "id": "01a0876e-7582-7116-b74e-3525710b1a17", "title": "A Trie in Swift", "url": "https://doisinkidney.com/posts/2015-08-11-swift-trie.html", "published_at": null }, { "id": "01a0876e-7582-7116-b74e-3525713d1087", "title": "Monty Hall", "url": "https://doisinkidney.com/posts/2015-08-03-monty-hall.html", "published_at": null }, { "id": "01a0876e-7582-7116-b74e-352571bc24d1", "title": "Deques, Queues, and Lists in Swift with Indirect", "url": "https://doisinkidney.com/posts/2015-07-29-swift-queues.html", "published_at": null }, { "id": "01a0876e-7582-7116-b74e-352572ad4d89", "title": "A Strategy for Swift Protocols", "url": "https://doisinkidney.com/posts/2015-07-17-swift-protocols-a-strategy.html", "published_at": null } ] posts Claim your blog

Back to doisinkidney.com

Blog · corpus.blog/blogs/doisinkidney.com/posts

doisinkidney.com

doisinkidney.com

Undated

Tries for Polynomials original ↗

—

Monuses and Heaps original ↗

—

POPL Paper—Hyperfunctions: Communicating Continuations original ↗

—

POPL Paper—Formalising Graph Algorithms with Coinduction original ↗

—

POPL Paper—Algebraic Effects Meet Hoare Logic in Cubical Agda original ↗

—

Lazily Grouping in Haskell original ↗

—

Depth Comonads original ↗

—

Weighted Search Package original ↗

—

ICFP Paper—Algebras for Weighted Search original ↗

—

Hyperfunctions original ↗

—

Master's Thesis original ↗

—

Trees indexed by a Cayley Monoid original ↗

—

Enumerating Trees original ↗

—

A Queue for Effectful Breadth-First Traversals original ↗

—

How to set up GitHub Actions for your Agda project original ↗

—

Fun with Combinators original ↗

—

Some More List Algorithms original ↗

—

Presentation on Purely Functional Data Structures original ↗

—

More Random Access Lists original ↗

—

Another Breadth-First Traversal original ↗

—

Typing TABA original ↗

—

Terminating Tricky Traversals original ↗

—

Lazy Constructive Numbers and the Stern-Brocot Tree original ↗

—

A Small Proof that Fin is Injective original ↗

—

How to do Binary Random-Access Lists Simply original ↗

—

What is Good About Haskell?original ↗

—

Bachelor's Thesis original ↗

—

Solving Programming Puzzles without using your Brain original ↗

—

Deriving a Linear-Time Applicative Traversal of a Rose Tree original ↗

—

Implicit Corecursive Queues original ↗

—

Concatenative Programming; The Free Monoid of Programming Languages original ↗

—

Some Tricks for List Manipulation original ↗

—

List Syntax in Agda original ↗

—

Probability Monads in Cubical Agda original ↗

—

Permutations By Sorting original ↗

—

Lazy Binary Numbers original ↗

—

More Agda Tips original ↗

—

Finger Trees in Agda original ↗

—

A New Ring Solver for Agda original ↗

—

A Binomial Urn original ↗

—

Drawing Trees original ↗

—

liftAN original ↗

—

Balancing Scans original ↗

—

Pure and Lazy Breadth-First Traversals of Graphs in Haskell original ↗

—

Prime Sieves in Agda original ↗

—

Keeping Formal Verification in Bounds original ↗

—

A Very Simple Prime Sieve in Haskell original ↗

—

Total Combinations original ↗

—

Agda Beginner(-ish) Tips, Tricks, and Pitfalls original ↗

—

Verified AVL Trees in Haskell and Agda original ↗

—

Probabilistic Functional Programming original ↗

—

Probability 5 Ways original ↗

—

Scheduling Effects original ↗

—

Rotations original ↗

—

Breadth-First Traversals in Far Too Much Detail original ↗

—

Breadth-First Rose Trees: Traversals and the Cofree Comonad original ↗

—

Swapping original ↗

—

Sorting Small Things in Haskell original ↗

—

Type-Level Induction in Haskell original ↗

—

5 Cool Things You Can Do With Pattern Synonyms original ↗

—

Strict Applicative Transformer original ↗

—

Countdown original ↗

—

Convolutions original ↗

—

Rose Trees, Breadth-First original ↗

—

Choose a random item from a list in one pass original ↗

—

Single-Pass Huffman Coding original ↗

—

Monadic List Functions original ↗

—

groupBy original ↗

—

Unfoldl original ↗

—

Balancing Folds original ↗

—

Convolutions and Semirings original ↗

—

Applicative Arithmetic original ↗

—

Verifying Data Structures in Haskell original ↗

—

Unparsing original ↗

—

Fun with Recursion Schemes original ↗

—

Constrained Applicatives original ↗

—

Semirings original ↗

—

Probability Trees original ↗

—

A Different Probability Monad original ↗

—

Revisiting a Trie in Haskell original ↗

—

Lenses are Static Selectors original ↗

—

Folding Two Things at Once original ↗

—

2048 in Python original ↗

—

A Trie in Haskell original ↗

—

Faking dependent types in Swift original ↗

—

Using Protocols to Build a (very) Generic Deque original ↗

—

A Trie in Swift original ↗

—

Monty Hall original ↗

—

Deques, Queues, and Lists in Swift with Indirect original ↗

—

A Strategy for Swift Protocols original ↗

—