Lysxia's blog

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

You may find me as Syrak on reddit, lyxia on libera.chat and a few other places.

Posts

• 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