A collection of bookmarks covering the topics of
- functional programming with haskell
- type theory
- category theory
- formal verification
- interesting stuff for haskellers
https://www.reddit.com/r/haskell
https://themonadreader.wordpress.com/
https://tech.fpcomplete.com/blog
https://homepages.inf.ed.ac.uk/wadler
https://wiki.haskell.org/The_Monad.Reader/Previous_issues
https://www.cambridge.org/core/journals/journal-of-functional-programming
The Implementation of Functional Programming Languages, Mark P. Jones: Very interesting book about programming a functional programming language from first principles; written in ML, but easily translatable
Dependent Types in Haskell: Theory and Practice, Richard A. Eisenberg
Advanced topics in types and programming languages, Benjamin C. Pierce
Optics by example, Chris Penner: An excellent introduction to all things optics related
Types and Programming Languages, Benjamin C. Pierce
Programming in Martin Löfs Type Theory
Homotopy Type Thoery: Univalent Foundations of Mathematics: very mathematical, but this is the foundations of "the next level of propositions as types"; practically a generalization of the Curry-Howard-Lambek-Isomorphism
Basic Category Theory, Tom Leistner: also for the mathemaically inclined, but evertheless very interesting; contains some good excercises.
Write Yourself a Scheme in 48 Hours
Purely Functional Data Structures, Chris Okasaki: An interesting book that captures common datastructures in functional programming languages such as queues and trees; The article "Monoids and Finger Trees" generalizes over all these datastructures, using finger trees; see below.
The Little Typer, Daniel P. Friedman and David Thrane Christiansen: a book on dependent types
The Logic of Provability, Boolos
Verified Functional Programming in Agda, Aaron Stump
Software Foundation Series, Bemjamin C. Pierce
Functional Programming with Overloading andHigher-Order Polymorphism, Mark P. Jones: typeclasses, jones
Kleisli arrows of outrageous fortune, CONOR McBRIDE: monads, category theory, functional pearl
Fast Incremental Regular Expression Matcihng: monoids, regex
Beyond Regurar Expressions: More incremental String Matching: monoids, regex
Word numbers, Part 1: Billion approaches: monoids
Extensible Effects: effect system
Arrows and Computation: arrows, category theory
Arrow Calculus: arrows, category theory, functional pearl, wadler
Evaluating Cellular Automata is Comonadic: comonad, automaton, theoretical cs
Comonads: comonad, milewski
The Essence of Dataflow Programming: comonads, stream
Catamorphisms: catamorphism, wiki, category theory
Functional programming with bananas, lenses, envelopes and barbed wire: datatypes, natural transformations, recursion schemes
Parametricity for Bifunctor: bifunctors, typeclasses
Hasochism: The Pleasure and Pain of Dependently Typed Haskell Programming: dependent types
The Yoneda Lemma: category theory, yoneda
Backwards IxApplicative for IxBackwards: applicatives, typeclasses
Can we have infinite sum types?: datatypes, sum types, category theory
The reasonable effectiveness of the continuation monad: continuations, monads
Does seq cause mutation?: evaluation, seq, mutation
Web Programming and Streaming Data in Haskell: slides, conduit, streaming, yesod, web
The rio library: rio, library, commercial, prelude
rio: A standard library: rio, library, commercial, prelude
Beware of readFile: snoyman, readFile, file, read, commercial
Parse don't validate: parsing, validation, input, types
The Monad.Reader Mini Issue 24: Predicates, Trees, GADTs: monad reader, predicates, trees, gadts
Monoids and Finger Trees: monoid, data structues, datatypes, okasaki, finger trees
Applicative programming with effects, CONOR MCBRIDE: applicatives, effects, functional pearl, effect system
Parametricity: Money for Nothing and Theorems for Free: milewski, theorems for free, category theory, types
Parsing context-sensitive languages with Applicative: parsing, applicative, theoretical cs
The Mother of all Monads: monads, continuations, category theory
Dependently Typed Haskell in Industry (Experience Report): galois, commertial, dependent types, verificaion, conference, lecture
A Role for Dependent Types in Haskell: dependent types, conference, lecture
Using the Indexed State Monad and Dependent Types to represent a Game of Texas Hold ‘Em: monad, state, game, gadts
From Löb's Theorem to Spreadsheet Evaluation: theoretical cs, comonads
Monad Transformer State: snoyman, monad transformer, conference, lecture
A Little Taste of Dependent Types: christiansen, dependent types, little typer
Asynchronous Exception Handling in Haskell: exceptions, parallel, async
How to Handle Asynchronous Exceptions in Haskell: exceptions, parallel, async, lecture
How to Script with Stack: stack, scripting, devenv
Lenses: lenses, tutorial
IO Inside: wiki, io, monads
stm: Software Transactional Memory: stm, parallel, async
The ReaderT Design Pattern: reader, monad transformer, design
Strict WriterT monad transformer: writer, monad transformer
Revisiting pattern match overlap checks in Haskell : jones, conference, lecture, pattern matching, completeness, exhaustive
Escape from the ivory tower: the Haskell journey: jones, conference, lecture, history
Can Programming Be Liberated from the von Neumann Style? A Functional Style and Its Algebra of Programs: backus, turing award, paradigms, algebra
Semigroup Resonance FizzBuzz: catamorphism, lazyness, stream, fizzbuzz
Haskell2010 Language Report: language report, documentation
Intro to Parsing with Parsec in Haskell: library, parsing, tutorial
Haskell Problems For a New Decade: diehl, problems
String Types: text, string, bytestring, lazy, strict, tutorial
Covariance and Contravariance: snoyman, covariance, contravariance, category theory, functors
The constraint trick for instances: constraints, typeclasses, ~
Partial Type Constructors - Or, Making Ad Hoc Datatypes Less Ad Hoc: datatypes, partial, complete, exhaustive, language
Haskell List Syntax and construction: lists, syntax, constructors, typeclasses, typeclass recursion
Primitive Haskell: primitives, lowlevel, implementation
Evaluation order and state tokens: evaluation, monads, state, io
Applied Haskell Syllabus: commertial, tutorial
Type Safety Back and Forth: types, safe
The Design and Use of QuickCheck: quickcheck, testing, tutorial
Existential Quantification: quantification, forall, existential, types
Plucking Constraints: constraints, typeclasses, design
Lenses, Folds and Traversals: An Introduction to the Lens Library with Edward Kmett: ekmett, lens, fold, traversal, lecture
Haskell's kind system - a primer: kinds, types, polymorphism, unboxed, dependent types
Linear Haskell: practical linearity in a higher-order polymorphic language: linear types, omega, jones
Announcing n-ary-functor-1.0: functors, arity
Levity Polymorphism: eisenberg, levity, polymorphism, lifted
Categories for the Working Hacker: wadler, conference, lecture, category theory
A practical Template Haskell tutorial: template, meta programming, tutorial
Template Meta Programming for Haskell: jones, template, meta programming
Algebraic lenses: algebra, lenses, penner, category theory
Parsers and Builders as Prisms: parsing, prisms, category theory
Software Design and Architecture in Haskell: collection, links, design, commertial
Pattern Synonyms Proposal: pattern synonyms, pattern matching
Pattern Synonyms: jones, eisenberg, pattern synonyms, pattern matching
GADTs meet their match: pattern-matching warnings that account for GADTs, guards, and laziness: jones, pattern matching, warnings, gadts, lazyness, guards
The Structure of Interaction: curry-howard, linear logic, inference, girard
Practical Data Processing With Haskell and Putting Cloud Haskell to Work: data processing, commertial, web, cloud
Introduction to Singletons: singleton, tutorial, dependent types, gadts
Haskell generics explained: generics, tutorial
Understanding F-Algebras: milewski, algebra, category theory, catamorphisms
Maybe catamorphism: catamorphism, maybe
Five benefits to using StandaloneKindSignatures: kinds, standalone, signature
A Type-Safe Approach to Categorized Data: categorized data, types, safe, design
Case study: migrating from lens to optics: lens, optics
Transformations on Applicative Concurrent Computations: transformations, applicative, concurrently
The Thoralf Plugin: For Your Fancy Type Needs: eisenberg, plugin, compiler, fancy types
OutsideIn(X) - Modular type inference with local assumptions: type inference, dependent types, jones, gadts, typeclasses
Getting a Quick Fix on Comonads: comonads, tutorial, lecture
GHC Users Guide: ghc, users guide, documentation
Faking It - Simulating Dependent Types in Haskell: dependent types
Preventing memoization in (AI) search problems: memoization, ai
Generalised Algebraic Datatypes: gadts, wiki
Gadt:AlmostDependentTypes: lecture, slides, gadts, dependent types
Dependent Types In Haskell: dependent types, tutorial
Programming with Refinement Types - Tutorial: refinement types, liquid types, tutorial
Programming with Refinement Types: refinement types, liquid types
From Design Patterns to Category Theory: design patterns
Do monad transformers, generally speaking, arise out of adjunctions?: monad transformers, adjunctions
Monads for functional programming: wadler, monads
Comprehending Monads: wadler, monads, tutorial
Propositions as Types: wadler, propositions, logic, type theory, verification
Catamorphisms: catamorphisms
Category Theory for Pogrammers I: milewski, lecture
Category Theory for Programmers II: milewski, lecture
Category Theory for Programmers III: milewski, lecture
A Unifying Theory of Dependent Types - the schematic approach: dependent types
Intuitionistic logic: intuitionistic logic, löf, dependent types, lambda cube, fomega
Calculus of constructions: coq, inductive constructions, calculus, lambda cube, lambdac
Curry-Howard correspondence: curry-howard, correspondence, isomorphism
Homotopy type theory: hott, homotopy, topology, infinite groupoids
Typed lambda calculus: types, lambda calculus, church
Hindley-Milner type inference: type inference, types, milner, hindley
Simply typed lambda calculus: church, types, lambda calculus
LF (logical framework): logical, framework, higher order logic
Example of type in System F that is not available in Hindley Milner type inference: system f, hindley, milner, types, inference
Dependent Type theory: dependent types
Intuitionistic Type Theory: löf, intuitionistic type theory
Pure Type System: type system, pure, generalised
Lambda Cube: higher order, type system, system f, fomega, typed, coq, constructions
Second Order Lambda Calculus: higher order, calculus, system f, girard, reynolds
Girard's paradox: girard, paradox
Propositions as Types: wadler, propositions, logic, type theory, category theory, verification
The Fun of Programming - Fun with Phantom Types: phantom types
Developing Bug-Free Machine Learning SystemsWith Formal Mathematics: ai
Lean: proof assistant
Verified Programming Based on Univalent Foundations in Agda - Part 0: hott, agda, tutorial
Arend: proof assistant
Twelf: proof assistant
Lecture Series for Software Foundation Series: lecture, pierce, software foundations
Agda vs. Coq vs. Idris: agda, coq, idris
Propositions as Types: wadler, propositions, logic, type theory, category theory, verification
HOL Theorem Prover: proof assistant, theorem proover
Isabelle: theorem prover, proof assistant
FStar: programming language
An Intuition for propagators: propagators, electrical circuits, simulation, computatoinal model
On the Expressive Power of Programming Languages: expression, semantics, translation, thinking process
What is your favourite academic paper on Programming Language Theory?: collection, links
dex-lang - Research Language for Array Processing in the Haskell/ML family: programming language, google, dex, array, index, list
Incorrectness Logic by Example: logic, incorrectness
What are the major open problems/issues with functional programming or Haskell right now?: problems, issues, functional
Executable Grammars: Seeking the minimal extensible self-compiling compiler (2009): grammar, compiler, plt
ghcid: Very low feature GHCi based IDE
The rio library: rio, library, commercial, prelude
Grapefruit: library, reactive
tweag/asterius - A Haskell to WebAssembly compiler: webassembly, web, transpiler
Typable and Data in Haskell: library, typeclasses, polymorphism, ad-hoc, tutorial
optparse-applicative - Applicative option parser: library, commandline options, parsing
A fast, flexible, fused effect system for Haskell: effect system, fused-effects, library, effects, monads
polysemy - higher-order, no-boilerplate, zero-cost monads: effect system, effects, library, monads
eff - a work in progress effect system for Haskell: effect system, effects, monads, library
ComonadSheet - A library for expressing "spreadsheet-like" computations: library, comonads, spreadsheets, cellular automatons, plt
LiquidHaskell - Liquid Types For Haskell: library, liquid types
The Power of Prolog: prolog
Typechecking Uses of the jQuery Language: jquery, web, types
Thinking the unthinkable: barriers, generations, point of view, science
Math is your insurance policy: correctness, safe, milewski, meta
Why Functional Programming Matters: huges, meta, safety
Haskell vs. Ada vs. C++ vs. Awk vs. ... - An Experiment in Software Prototyping Productivity: hudak, jones, meta
HalVM - Galois Inc.: virtual machine, architecture, efficiency, galois