Skip to content

Instantly share code, notes, and snippets.

@haskie-lambda
Last active August 11, 2021 09:15
Show Gist options
  • Save haskie-lambda/55f74dba1f3c1a2408ce545d4984159b to your computer and use it in GitHub Desktop.
Save haskie-lambda/55f74dba1f3c1a2408ce545d4984159b to your computer and use it in GitHub Desktop.
A collection of bookmarks

Bookmarks

A collection of bookmarks covering the topics of

  • functional programming with haskell
  • type theory
  • category theory
  • formal verification
  • interesting stuff for haskellers

Sites for rescources

http://blog.sigfpe.com

https://bartoszmilewski.com

https://www.reddit.com/r/haskell

https://www.snoyman.com

https://themonadreader.wordpress.com/

https://apfelmus.nfshost.com/

https://tech.fpcomplete.com/blog

https://www.parsonsmatt.org

https://homepages.inf.ed.ac.uk/wadler

https://chrisdone.com/posts/

https://chrispenner.ca/posts/

https://markkarpov.com/

https://blog.ploeh.dk/

https://wiki.haskell.org/The_Monad.Reader/Previous_issues

https://byorgey.wordpress.com

https://www.cambridge.org/core/journals/journal-of-functional-programming

Books

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

Up to date Real World Haskell

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

Mastering Haskell

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

Category Theory

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

TypeTheory

A Unifying Theory of Dependent Types - the schematic approach: dependent types

Wikipedia Links

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

Formal Verification related

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

PLT

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

Tools and libraries

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

Compiler Related

A quick look at Impredicativity: jones, ghc, impredicativity, types, type-inference

Functional Graphics

LambdaCube3D

Futhark

Rumpus

Misc

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

Interesting Companies

Galois

tweag I/O

Serokell

FPComplete

Conferences

ICFP - International Conference on Functional Programming

MuniHac

ZuriHac

Monadic Party

Strageloop

Curry On

Other Conferences

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment