Skip to content

Instantly share code, notes, and snippets.

@stevemao
Forked from haskie-lambda/bookmarks.md
Created April 19, 2020 00:48
Show Gist options
  • Save stevemao/6d9e9c17bc1db3ae5a1163f7e7ca928e to your computer and use it in GitHub Desktop.
Save stevemao/6d9e9c17bc1db3ae5a1163f7e7ca928e 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

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

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

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

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