Lysxia's blog

A blog about functional programming and stuff, preferably in Haskell and Coq. The source code of this blog is here.

Posts

Alpha-beta pruning is just minimax in a lattice of clamping functions - September 1, 2025
Twentyseven 1.0.0 - August 1, 2025
Unfolding trees breadth-first in Haskell - March 30, 2025
Where does the name "algebraic data type" come from? - July 26, 2024
Programming Turing machines with regexes - June 18, 2024
Abstract nonsense - September 5, 2023
From delimited continuations to algebraic effects in Haskell - January 2, 2023
The quantified constraint trick - September 21, 2022
Formalizing finite sets - May 27, 2022
The pro-PER meaning of "proper" - April 7, 2022
On proving lists infinite - October 26, 2021
Initial and final encodings of free monads - October 20, 2021
What is a type? - March 17, 2021
Defunctionalizing dependent type families in Haskell - January 16, 2021
Theory of iteration and recursion - January 3, 2021
hs-to-coq and Data.Sequence - November 23, 2020
Definitional lawfulness: proof by inspection testing - August 8, 2020
Generic traversals with applicative difference lists - August 5, 2020
The pl-a.net link aggregators - July 26, 2020
Programming totally with head and tail - April 13, 2020
Testing higher-order properties with QuickCheck - February 24, 2020
A monad is just a submonad of the continuation monad, what's the problem? - October 27, 2019
The reasonable effectiveness of the continuation monad - October 26, 2019
Infinite types and existential newtypes - October 25, 2019
Making Haskell run fast: the many faces of reverse - September 13, 2019
Functor, Applicative, Monad, a play - July 17, 2019
Free applicative functors in Coq - July 14, 2019
Free monads of free monads - June 9, 2019
Formalization of Reynolds's parametricity theorem in Coq - April 3, 2019
Higher-rank types in Standard Haskell - March 25, 2019
From C to Interaction trees: Specifying, Verifying, and Testing a networked server (CPP 2019 talk transcript) - January 14, 2019
Hiding code blocks in literate programming blogs - January 9, 2019
Naming abstraction - December 9, 2018
Surgery for data types - November 26, 2018
Overloaded type families - September 29, 2018
Haskell with only one type family - August 6, 2018
Type is an extensible GADT - July 9, 2018
Deriving instances with a twist - July 8, 2018
Heterogeneous lists with dependent types in Haskell - June 6, 2018
Pipes define a free monad - April 26, 2018
An old and a new library for generic deriving - March 28, 2018
Deriving Show for higher-kinded types - March 3, 2018
A quick tour of generic-random - January 5, 2018
Making a Show with reflection - October 21, 2017
Performance debugging in aeson - October 8, 2017
Fuzzing of concurrent programs - October 6, 2017
A terminal view of testing polymorphic functions - June 29, 2017
Canonical testing for polymorphic functions - June 7, 2017
Free monad transformers - May 28, 2017
Note to myself: a theory of injective arrows - April 22, 2017
Randomness in purely functional programs - March 4, 2017
Enumeration of multigraph DFS - March 1, 2017
Coupled reader and writer - January 4, 2017
Monadic profunctors for bidirectional programming - January 1, 2017
Applicative style programming with profunctors - December 23, 2016
Applicative lenses - November 2, 2016
Lookaheads - October 28, 2016
Typeclasses for bidirectional serialization, an example - October 20, 2016
Typeclasses for bidirectional serialization - October 19, 2016
Better invertible syntax descriptions - October 18, 2016
Towards monadic bidirectional serialization, a monadic example - October 17, 2016
Towards monadic bidirectional serialization, a step back - October 13, 2016
Towards monadic bidirectional serialization - October 12, 2016
Incremental updates for efficient bidirectional transformations - October 6, 2016
Parsing and unparsing with lenses - September 28, 2016