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
Thinking with Types, Sandy Maguire
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
Basic Type Level Programming: type level programming, types, higher order
Strongly Typed System F: stephanie weidrich, type level programming, higier order, system f, type system
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
A quick look at Impredicativity: jones, ghc, impredicativity, types, type-inference
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