Skip to content

Instantly share code, notes, and snippets.

@haskie-lambda

haskie-lambda/bookmarks.md

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.
Download ZIP

Revisions

  1. haskie-lambda revised this gist Aug 29, 2020. 1 changed file with 2 additions and 0 deletions.
    2 changes: 2 additions & 0 deletions bookmarks.md
    View file
    Original file line number Diff line number Diff line change
    @@ -444,6 +444,8 @@ https://www.cambridge.org/core/journals/journal-of-functional-programming

    ### Conferences

    [ICFP - International Conference on Functional Programming](http://www.icfpconference.org/)

    [MuniHac](https://munihac.de/2018.html)

    [ZuriHac](https://zfoh.ch/zurihac2020/)
  2. haskie-lambda revised this gist Aug 29, 2020. 1 changed file with 4 additions and 0 deletions.
    4 changes: 4 additions & 0 deletions bookmarks.md
    View file
    Original file line number Diff line number Diff line change
    @@ -404,6 +404,10 @@ https://www.cambridge.org/core/journals/journal-of-functional-programming

    [LiquidHaskell - Liquid Types For Haskell](https://github.com/ucsd-progsys/liquidhaskell): library, liquid types

    ## Compiler Related

    [A quick look at Impredicativity](https://www.reddit.com/r/haskell/comments/gjni4q/video_for_a_quick_look_at_impredicativity_simon/?utm_source=share&utm_medium=ios_app&utm_name=iossmf): jones, ghc, impredicativity, types, type-inference

    ### Functional Graphics

    [LambdaCube3D](https://lambdacube3d.wordpress.com/)
  3. haskie-lambda revised this gist Jun 22, 2020. 1 changed file with 4 additions and 0 deletions.
    4 changes: 4 additions & 0 deletions bookmarks.md
    View file
    Original file line number Diff line number Diff line change
    @@ -275,6 +275,10 @@ https://www.cambridge.org/core/journals/journal-of-functional-programming

    [Programming with Refinement Types](http://ucsd-progsys.github.io/liquidhaskell-tutorial/book.pdf): refinement types, liquid types

    [Basic Type Level Programming](https://www.parsonsmatt.org/2017/04/26/basic_type_level_programming_in_haskell.html): type level programming, types, higher order

    [Strongly Typed System F](https://www.youtube.com/watch?v=j2xYSxMkXeQ): stephanie weidrich, type level programming, higier order, system f, type system

    ## Category Theory

    [From Design Patterns to Category Theory](https://blog.ploeh.dk/2017/10/04/from-design-patterns-to-category-theory/): design patterns
  4. haskie-lambda revised this gist Jun 22, 2020. 1 changed file with 2 additions and 0 deletions.
    2 changes: 2 additions & 0 deletions bookmarks.md
    View file
    Original file line number Diff line number Diff line change
    @@ -72,6 +72,8 @@ https://www.cambridge.org/core/journals/journal-of-functional-programming

    [Software Foundation Series, Bemjamin C. Pierce](https://softwarefoundations.cis.upenn.edu/current/index.html)

    [Thinking with Types, Sandy Maguire](https://leanpub.com/thinking-with-types)

    ## Mastering Haskell

    [Functional Programming with Overloading andHigher-Order Polymorphism, Mark P. Jones](http://web.cecs.pdx.edu/~mpj/pubs/springschool95.pdf): typeclasses, jones
  5. haskie-lambda revised this gist Apr 18, 2020. 1 changed file with 190 additions and 0 deletions.
    190 changes: 190 additions & 0 deletions bookmarks.md
    View file
    Original file line number Diff line number Diff line change
    @@ -41,218 +41,408 @@ https://byorgey.wordpress.com
    https://www.cambridge.org/core/journals/journal-of-functional-programming

    ## Books

    [The Implementation of Functional Programming Languages, Mark P. Jones](https://www.microsoft.com/en-us/research/uploads/prod/1987/01/slpj-book-1987-r90.pdf): 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](https://arxiv.org/pdf/1610.07978.pdf)

    [Advanced topics in types and programming languages, Benjamin C. Pierce](https://b-ok.cc/book/490535/9f7156)

    [Optics by example, Chris Penner](https://b-ok.cc/book/5332887/d426b5): An excellent introduction to all things optics related

    [Types and Programming Languages, Benjamin C. Pierce](https://b-ok.cc/book/655939/ecbfc7)

    [Programming in Martin Löfs Type Theory](https://b-ok.cc/book/687341/f5b77b)

    [Homotopy Type Thoery: Univalent Foundations of Mathematics](https://hott.github.io/book/nightly/hott-online-1246-g494c5db.pdf): 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](https://arxiv.org/pdf/1612.09375.pdf): also for the mathemaically inclined, but evertheless very interesting; contains some good excercises.

    [Write Yourself a Scheme in 48 Hours](https://en.wikibooks.org/wiki/Write_Yourself_a_Scheme_in_48_Hours/)

    [Up to date Real World Haskell](https://github.com/tssm/up-to-date-real-world-haskell)

    [Purely Functional Data Structures, Chris Okasaki](https://www.cs.cmu.edu/~rwh/theses/okasaki.pdf): 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](https://www.thelittletyper.com/): a book on dependent types

    [The Logic of Provability, Boolos](https://www.amazon.com/Logic-Provability-George-S-Boolos/dp/0521483255)

    [Verified Functional Programming in Agda, Aaron Stump](https://dl.acm.org/doi/pdf/10.1145/2841316?download=false)

    [Software Foundation Series, Bemjamin C. Pierce](https://softwarefoundations.cis.upenn.edu/current/index.html)

    ## Mastering Haskell

    [Functional Programming with Overloading andHigher-Order Polymorphism, Mark P. Jones](http://web.cecs.pdx.edu/~mpj/pubs/springschool95.pdf): typeclasses, jones

    [Kleisli arrows of outrageous fortune, CONOR McBRIDE](https://personal.cis.strath.ac.uk/conor.mcbride/Kleisli.pdf): monads, category theory, functional pearl

    [Fast Incremental Regular Expression Matcihng](http://blog.sigfpe.com/2009/01/fast-incremental-regular-expression.html): monoids, regex

    [Beyond Regurar Expressions: More incremental String Matching](http://blog.sigfpe.com/2009/01/beyond-regular-expressions-more.html): monoids, regex

    [Word numbers, Part 1: Billion approaches](http://conway.rutgers.edu/~ccshan/wiki/blog/posts/WordNumbers1/): monoids

    [Extensible Effects](http://okmij.org/ftp/Haskell/extensible/exteff.pdf): effect system

    [Arrows and Computation](http://www.staff.city.ac.uk/~ross/papers/fop.html): arrows, category theory

    [Arrow Calculus](http://homepages.inf.ed.ac.uk/wadler/papers/arrows/arrows.pdf): arrows, category theory, functional pearl, wadler

    [Evaluating Cellular Automata is Comonadic](http://blog.sigfpe.com/2006/12/evaluating-cellular-automata-is.html): comonad, automaton, theoretical cs

    [Comonads](https://bartoszmilewski.com/2017/01/02/comonads/): comonad, milewski

    [The Essence of Dataflow Programming](http://cs.ioc.ee/~tarmo/papers/essence.pdf): comonads, stream

    [Catamorphisms](https://wiki.haskell.org/Catamorphisms): catamorphism, wiki, category theory

    [Functional programming with bananas, lenses, envelopes and barbed wire](https://link.springer.com/chapter/10.1007%2F3540543961_7): datatypes, natural transformations, recursion schemes

    [Parametricity for Bifunctor](https://byorgey.wordpress.com/2018/03/30/parametricity-for-bifunctor/): bifunctors, typeclasses

    [Hasochism: The Pleasure and Pain of Dependently Typed Haskell Programming](https://personal.cis.strath.ac.uk/conor.mcbride/pub/hasochism.pdf): dependent types

    [The Yoneda Lemma](http://blog.sigfpe.com/2006/11/yoneda-lemma.html): category theory, yoneda

    [Backwards IxApplicative for IxBackwards](https://www.reddit.com/r/haskell/comments/dtntre/backwards_ixapplicative_for_ixbackwards/): applicatives, typeclasses

    [Can we have infinite sum types?](https://www.reddit.com/r/haskell/comments/e7kon1/can_we_have_infinite_sum_types): datatypes, sum types, category theory


    [The reasonable effectiveness of the continuation monad](https://blog.poisson.chat/posts/2019-10-26-reasonable-continuations.html): continuations, monads

    [Does seq cause mutation?](https://www.reddit.com/r/haskell/comments/e9nbx1/does_seq_cause_mutation/): evaluation, seq, mutation

    [Web Programming and Streaming Data in Haskell](https://www.snoyman.com/reveal/conduit-yesod#/25): slides, conduit, streaming, yesod, web

    [The rio library](https://github.com/commercialhaskell/rio#readme): rio, library, commercial, prelude

    [rio: A standard library](https://tech.fpcomplete.com/haskell/library/rio): rio, library, commercial, prelude

    [Beware of readFile](https://www.snoyman.com/blog/2016/12/beware-of-readfile): snoyman, readFile, file, read, commercial

    [Parse don't validate](https://lexi-lambda.github.io/blog/2019/11/05/parse-don-t-validate/): parsing, validation, input, types

    [The Monad.Reader Mini Issue 24: Predicates, Trees, GADTs](https://themonadreader.files.wordpress.com/2015/08/issue24.pdf): monad reader, predicates, trees, gadts

    [Monoids and Finger Trees](https://apfelmus.nfshost.com/articles/monoid-fingertree.html): monoid, data structues, datatypes, okasaki, finger trees

    [Applicative programming with effects, CONOR MCBRIDE](http://strictlypositive.org/IdiomLite.pdf): applicatives, effects, functional pearl, effect system

    [Parametricity: Money for Nothing and Theorems for Free](https://bartoszmilewski.com/2014/09/22/parametricity-money-for-nothing-and-theorems-for-free/): milewski, theorems for free, category theory, types

    [Parsing context-sensitive languages with Applicative](https://byorgey.wordpress.com/2012/01/05/parsing-context-sensitive-languages-with-applicative/): parsing, applicative, theoretical cs

    [The Mother of all Monads](http://blog.sigfpe.com/2008/12/mother-of-all-monads.html): monads, continuations, category theory

    [Dependently Typed Haskell in Industry (Experience Report)](https://www.reddit.com/r/haskell/comments/e9sjmz/dependently_typed_haskell_in_industry_experience/): galois, commertial, dependent types, verificaion, conference, lecture

    [A Role for Dependent Types in Haskell](https://www.youtube.com/watch?v=0udX2HqFUD8): dependent types, conference, lecture

    [Using the Indexed State Monad and Dependent Types to represent a Game of Texas Hold ‘Em](https://santiagoweight.wordpress.com/2019/10/25/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](http://blog.sigfpe.com/2006/11/from-l-theorem-to-spreadsheet.html): theoretical cs, comonads

    [Monad Transformer State](https://www.youtube.com/watch?v=KZIN9f9rI34): snoyman, monad transformer, conference, lecture

    [A Little Taste of Dependent Types](https://www.youtube.com/watch?v=VxINoKFm-S4): christiansen, dependent types, little typer

    [Asynchronous Exception Handling in Haskell](https://tech.fpcomplete.com/blog/2018/04/async-exception-handling-haskell): exceptions, parallel, async

    [How to Handle Asynchronous Exceptions in Haskell](https://tech.fpcomplete.com/blog/how-to-handle-asynchronous-exceptions-in-haskell): exceptions, parallel, async, lecture

    [How to Script with Stack](https://tech.fpcomplete.com/haskell/tutorial/stack-script): stack, scripting, devenv

    [Lenses](https://tech.fpcomplete.com/haskell/tutorial/lens): lenses, tutorial

    [IO Inside](https://wiki.haskell.org/IO_inside): wiki, io, monads

    [stm: Software Transactional Memory](https://tech.fpcomplete.com/haskell/library/stm): stm, parallel, async

    [The ReaderT Design Pattern](https://tech.fpcomplete.com/blog/2017/06/readert-design-pattern): reader, monad transformer, design

    [Strict WriterT monad transformer](https://mail.haskell.org/pipermail/libraries/2012-October/018599.html): writer, monad transformer

    [Revisiting pattern match overlap checks in Haskell ](https://www.reddit.com/r/ProgrammingLanguages/comments/eda7hs/revisiting_pattern_match_overlap_checks_in/): jones, conference, lecture, pattern matching, completeness, exhaustive

    [Escape from the ivory tower: the Haskell journey](https://www.youtube.com/watch?v=re96UgMk6GQ): jones, conference, lecture, history

    [Can Programming Be Liberated from the von Neumann Style? A Functional Style and Its Algebra of Programs](http://www.csc.villanova.edu/~beck/csc8310/BackusFP.pdf): backus, turing award, paradigms, algebra

    [Semigroup Resonance FizzBuzz](https://blog.ploeh.dk/2019/12/30/semigroup-resonance-fizzbuzz/): catamorphism, lazyness, stream, fizzbuzz

    [Haskell2010 Language Report](https://www.haskell.org/onlinereport/haskell2010/): language report, documentation

    [Intro to Parsing with Parsec in Haskell](https://jakewheat.github.io/intro_to_parsing/): library, parsing, tutorial

    [Haskell Problems For a New Decade](http://www.stephendiehl.com/posts/decade.html): diehl, problems

    [String Types](https://tech.fpcomplete.com/haskell/tutorial/string-types): text, string, bytestring, lazy, strict, tutorial

    [Covariance and Contravariance](https://tech.fpcomplete.com/blog/2016/11/covariance-contravariance): snoyman, covariance, contravariance, category theory, functors

    [The constraint trick for instances](https://chrisdone.com/posts/haskell-constraint-trick/): constraints, typeclasses, ~

    [Partial Type Constructors - Or, Making Ad Hoc Datatypes Less Ad Hoc](https://www.reddit.com/r/haskell/comments/f0x6mx/partial_type_constructors_or_making_ad_hoc/): datatypes, partial, complete, exhaustive, language

    [Haskell List Syntax and construction](https://www.reddit.com/r/ProgrammerHumor/comments/f6m5fh/haskell/): lists, syntax, constructors, typeclasses, typeclass recursion

    [Primitive Haskell](https://tech.fpcomplete.com/haskell/tutorial/primitive-haskell): primitives, lowlevel, implementation

    [Evaluation order and state tokens](https://wiki.haskell.org/Evaluation_order_and_state_tokens): evaluation, monads, state, io

    [Applied Haskell Syllabus](https://tech.fpcomplete.com/haskell/syllabus): commertial, tutorial

    [Type Safety Back and Forth](https://www.parsonsmatt.org/2017/10/11/type_safety_back_and_forth.html): types, safe

    [The Design and Use of QuickCheck](https://begriffs.com/posts/2017-01-14-design-use-quickcheck.html): quickcheck, testing, tutorial

    [Existential Quantification](https://markkarpov.com/post/existential-quantification.html): quantification, forall, existential, types

    [Plucking Constraints](https://www.parsonsmatt.org/2020/01/03/plucking_constraints.html): constraints, typeclasses, design

    [Lenses, Folds and Traversals: An Introduction to the Lens Library with Edward Kmett](https://vimeo.com/56063074): ekmett, lens, fold, traversal, lecture

    [Haskell's kind system - a primer](https://diogocastro.com/blog/2018/10/17/haskells-kind-system-a-primer/): kinds, types, polymorphism, unboxed, dependent types

    [Linear Haskell: practical linearity in a higher-order polymorphic language](https://www.youtube.com/watch?v=t0mhvd3-60Y): linear types, omega, jones

    [Announcing n-ary-functor-1.0](https://www.reddit.com/r/haskell/comments/ety9hv/announcing_naryfunctor10/): functors, arity

    [Levity Polymorphism](https://www.youtube.com/watch?v=lSJwXZ7vWBw): eisenberg, levity, polymorphism, lifted

    [Categories for the Working Hacker](https://www.youtube.com/watch?v=gui_SE8rJUM): wadler, conference, lecture, category theory

    [A practical Template Haskell tutorial](https://wiki.haskell.org/A_practical_Template_Haskell_Tutorial): template, meta programming, tutorial

    [Template Meta Programming for Haskell](https://www.microsoft.com/en-us/research/publication/template-meta-programming-for-haskell/?from=http://research.microsoft.com/~simonpj/papers/meta-haskell/): jones, template, meta programming

    [Algebraic lenses](https://chrispenner.ca/posts/algebraic): algebra, lenses, penner, category theory

    [Parsers and Builders as Prisms](https://yairchu.github.io/posts/codecs-as-prisms.html): parsing, prisms, category theory

    [Software Design and Architecture in Haskell](https://github.com/graninas/software-design-in-haskell/blob/master/README.md): collection, links, design, commertial

    [Pattern Synonyms Proposal](https://gitlab.haskell.org/ghc/ghc/-/wikis/pattern-synonyms): pattern synonyms, pattern matching

    [Pattern Synonyms](https://www.microsoft.com/en-us/research/wp-content/uploads/2016/08/pattern-synonyms-Haskell16.pdf): jones, eisenberg, pattern synonyms, pattern matching

    [GADTs meet their match: pattern-matching warnings that account for GADTs, guards, and laziness](https://www.microsoft.com/en-us/research/publication/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](http://cl-informatik.uibk.ac.at/users/sgimenez/data/articles/soi.pdf): curry-howard, linear logic, inference, girard

    [Practical Data Processing With Haskell and Putting Cloud Haskell to Work](https://vimeo.com/53906049): data processing, commertial, web, cloud

    [Introduction to Singletons](https://blog.jle.im/entry/introduction-to-singletons-1.html): singleton, tutorial, dependent types, gadts

    [Haskell generics explained](https://markkarpov.com/tutorial/generics.html): generics, tutorial

    [Understanding F-Algebras](https://bartoszmilewski.com/2013/06/10/understanding-f-algebras/): milewski, algebra, category theory, catamorphisms

    [Maybe catamorphism](https://blog.ploeh.dk/2019/05/20/maybe-catamorphism/): catamorphism, maybe

    [Five benefits to using StandaloneKindSignatures](https://ryanglscott.github.io/2020/01/05/five-benefits-to-using-standalonekindsignatures/): kinds, standalone, signature

    [A Type-Safe Approach to Categorized Data](https://epeery.com/typesafe-approach-to-categorized-data/): categorized data, types, safe, design

    [Case study: migrating from lens to optics](https://oleg.fi/gists/posts/2020-01-25-case-study-migration-from-lens-to-optics.html): lens, optics

    [Transformations on Applicative Concurrent Computations](https://tech.fpcomplete.com/blog/transformations-on-applicative-concurrent-computations): transformations, applicative, concurrently

    [The Thoralf Plugin: For Your Fancy Type Needs](https://repository.brynmawr.edu/cgi/viewcontent.cgi?article=1081&context=compsci_pubs): eisenberg, plugin, compiler, fancy types

    [OutsideIn(X) - Modular type inference with local assumptions](https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/jfp-outsidein.pdf): type inference, dependent types, jones, gadts, typeclasses

    [Getting a Quick Fix on Comonads](https://www.youtube.com/watch?v=F7F-BzOB670): comonads, tutorial, lecture

    [GHC Users Guide](https://downloads.haskell.org/~ghc/latest/docs/html/users_guide.html): ghc, users guide, documentation

    [Faking It - Simulating Dependent Types in Haskell](http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.22.2636&rep=rep1&type=pdf): dependent types

    [Preventing memoization in (AI) search problems](http://okmij.org/ftp/Haskell/index.html): memoization, ai

    [Generalised Algebraic Datatypes](https://wiki.haskell.org/Generalised_algebraic_datatype): gadts, wiki

    [Gadt:AlmostDependentTypes](https://akaposi.github.io/away_day/balestrieri.pdf): lecture, slides, gadts, dependent types

    [Dependent Types In Haskell](https://www.schoolofhaskell.com/user/konn/prove-your-haskell-for-great-safety/dependent-types-in-haskell): dependent types, tutorial

    [Programming with Refinement Types - Tutorial](http://ucsd-progsys.github.io/liquidhaskell-tutorial/): refinement types, liquid types, tutorial

    [Programming with Refinement Types](http://ucsd-progsys.github.io/liquidhaskell-tutorial/book.pdf): refinement types, liquid types

    ## Category Theory

    [From Design Patterns to Category Theory](https://blog.ploeh.dk/2017/10/04/from-design-patterns-to-category-theory/): design patterns

    [Do monad transformers, generally speaking, arise out of adjunctions?](https://stackoverflow.com/questions/56726854/do-monad-transformers-generally-speaking-arise-out-of-adjunctions): monad transformers, adjunctions

    [Monads for functional programming](https://homepages.inf.ed.ac.uk/wadler/papers/marktoberdorf/baastad.pdf): wadler, monads

    [Comprehending Monads](https://ncatlab.org/nlab/files/WadlerMonads.pdf): wadler, monads, tutorial

    [Propositions as Types](https://homepages.inf.ed.ac.uk/wadler/papers/propositions-as-types/propositions-as-types.pdf): wadler, propositions, logic, type theory, verification

    [Catamorphisms](https://blog.ploeh.dk/2019/04/29/catamorphisms/): catamorphisms

    [Category Theory for Pogrammers I](https://www.youtube.com/watch?v=I8LbkfSSR58&list=PLbgaMIhjbmEnaH_LTkxLI7FMa2HsnawM_): milewski, lecture

    [Category Theory for Programmers II](https://www.youtube.com/watch?v=3XTQSx1A3x8&list=PLbgaMIhjbmElia1eCEZNvsVscFef9m0dm): milewski, lecture

    [Category Theory for Programmers III](https://www.youtube.com/watch?v=F5uEpKwHqdk&list=PLbgaMIhjbmEn64WVX4B08B4h2rOtueWIL): milewski, lecture

    ## TypeTheory

    [A Unifying Theory of Dependent Types - the schematic approach](https://www.researchgate.net/profile/Zhaohui_Luo/publication/225233240_A_unifying_theory_of_dependent_types_the_schematic_approach/links/0deec52a1025ec6518000000/A-unifying-theory-of-dependent-types-the-schematic-approach.pdf?origin=publication_detail): dependent types

    ### Wikipedia Links

    [Intuitionistic logic](https://en.wikipedia.org/wiki/Intuitionistic_logic): intuitionistic logic, löf, dependent types, lambda cube, fomega

    [Calculus of constructions](https://en.wikipedia.org/wiki/Calculus_of_constructions): coq, inductive constructions, calculus, lambda cube, lambdac

    [Curry-Howard correspondence](https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence): curry-howard, correspondence, isomorphism

    [Homotopy type theory](https://en.wikipedia.org/wiki/Homotopy_type_theory): hott, homotopy, topology, infinite groupoids

    [Typed lambda calculus](https://en.wikipedia.org/wiki/Typed_lambda_calculus): types, lambda calculus, church

    [Hindley-Milner type inference](https://en.wikipedia.org/wiki/Hindley%E2%80%93Milner_type_inference): type inference, types, milner, hindley

    [Simply typed lambda calculus](https://en.wikipedia.org/wiki/Simply_typed_lambda_calculus): church, types, lambda calculus

    [LF (logical framework)](https://en.wikipedia.org/wiki/LF_(logical_framework)): logical, framework, higher order logic

    [Example of type in System F that is not available in Hindley Milner type inference](https://stackoverflow.com/questions/23995736/example-of-type-in-system-f-that-is-not-available-in-hindley-milner-type-inferen): system f, hindley, milner, types, inference

    [Dependent Type theory](https://en.wikipedia.org/wiki/Dependent_type_theory): dependent types

    [Intuitionistic Type Theory](https://en.wikipedia.org/wiki/Intuitionistic_type_theory): löf, intuitionistic type theory

    [Pure Type System](https://en.wikipedia.org/wiki/Pure_type_system): type system, pure, generalised

    [Lambda Cube](https://en.wikipedia.org/wiki/Lambda_cube): higher order, type system, system f, fomega, typed, coq, constructions

    [Second Order Lambda Calculus](https://en.wikipedia.org/wiki/Second_order_lambda_calculus): higher order, calculus, system f, girard, reynolds

    [Girard's paradox](https://en.wikipedia.org/wiki/Girard%27s_paradox): girard, paradox

    [Propositions as Types](https://homepages.inf.ed.ac.uk/wadler/papers/propositions-as-types/propositions-as-types.pdf): wadler, propositions, logic, type theory, category theory, verification

    [The Fun of Programming - Fun with Phantom Types](http://www.cs.ox.ac.uk/ralf.hinze/publications/With.pdf): phantom types

    ## Formal Verification related


    [Developing Bug-Free Machine Learning SystemsWith Formal Mathematics](https://arxiv.org/pdf/1706.08605.pdf): ai

    [Lean](https://leanprover.github.io/theorem_proving_in_lean/tactics.html): proof assistant

    [Verified Programming Based on Univalent Foundations in Agda - Part 0](https://maxbaroi.gitlab.io/posts/2020-04-17-Basics.html): hott, agda, tutorial

    [Arend](https://arend-lang.github.io/about/arend-features): proof assistant

    [Twelf](https://en.wikipedia.org/wiki/Twelf): proof assistant

    [Lecture Series for Software Foundation Series](https://www.youtube.com/watch?v=KKrD4JcfW90&list=PLGCr8P_YncjUT7gXUVJWSoefQ40gTOz89): lecture, pierce, software foundations

    [Agda vs. Coq vs. Idris](https://whatisrt.github.io/dependent-types/2020/02/18/agda-vs-coq-vs-idris.html): agda, coq, idris

    [Propositions as Types](https://homepages.inf.ed.ac.uk/wadler/papers/propositions-as-types/propositions-as-types.pdf): wadler, propositions, logic, type theory, category theory, verification

    [HOL Theorem Prover](https://hol-theorem-prover.org/#where-to-start): proof assistant, theorem proover

    [Isabelle](https://isabelle.in.tum.de/): theorem prover, proof assistant

    [FStar](https://www.fstar-lang.org/tutorial/): programming language

    ## PLT

    [An Intuition for propagators](https://www.reddit.com/r/haskell/comments/dy8joz/george_wilson_an_intuition_for_propagators/): propagators, electrical circuits, simulation, computatoinal model

    [On the Expressive Power of Programming Languages](https://link.springer.com/content/pdf/10.1007/3-540-52592-0_60.pdf): expression, semantics, translation, thinking process

    [What is your favourite academic paper on Programming Language Theory?](https://www.reddit.com/r/ProgrammingLanguages/comments/dwt8xu/what_is_your_favourite_academic_paper_on/): collection, links

    [dex-lang - Research Language for Array Processing in the Haskell/ML family](https://google-research.github.io/dex-lang/regression.html): programming language, google, dex, array, index, list

    [Incorrectness Logic by Example](https://hexgolems.com/2020/04/incorrectness-logic-by-example/): logic, incorrectness

    [What are the major open problems/issues with functional programming or Haskell right now?](https://www.reddit.com/r/haskell/comments/fmthoy/what_are_the_major_open_problemsissues_with/): problems, issues, functional

    [Executable Grammars: Seeking the minimal extensible self-compiling compiler (2009)](https://www.reddit.com/r/ProgrammingLanguages/comments/enr99b/executable_grammars_seeking_the_minimal/): grammar, compiler, plt

    ## Tools and libraries

    [ghcid](https://github.com/ndmitchell/ghcid): Very low feature GHCi based IDE

    [The rio library](https://github.com/commercialhaskell/rio#readme): rio, library, commercial, prelude

    [Grapefruit](https://wiki.haskell.org/Grapefruit): library, reactive

    [tweag/asterius - A Haskell to WebAssembly compiler](https://github.com/tweag/asterius): webassembly, web, transpiler

    [Typable and Data in Haskell](https://chrisdone.com/posts/data-typeable/): library, typeclasses, polymorphism, ad-hoc, tutorial

    [optparse-applicative - Applicative option parser](https://github.com/pcapriotti/optparse-applicative/blob/master/README.md): library, commandline options, parsing

    [A fast, flexible, fused effect system for Haskell](https://github.com/fused-effects/fused-effects): effect system, fused-effects, library, effects, monads

    [polysemy - higher-order, no-boilerplate, zero-cost monads](https://github.com/polysemy-research/polysemy): effect system, effects, library, monads

    [eff - a work in progress effect system for Haskell](https://github.com/hasura/eff): effect system, effects, monads, library

    [ComonadSheet - A library for expressing "spreadsheet-like" computations](https://github.com/kwf/ComonadSheet): library, comonads, spreadsheets, cellular automatons, plt

    [LiquidHaskell - Liquid Types For Haskell](https://github.com/ucsd-progsys/liquidhaskell): library, liquid types

    ### Functional Graphics

    [LambdaCube3D](https://lambdacube3d.wordpress.com/)

    [Futhark](https://futhark-lang.org/)

    [Rumpus](https://github.com/lukexi/rumpus)

    ## Misc

    [The Power of Prolog](https://www.metalevel.at/prolog): prolog

    [Typechecking Uses of the jQuery Language](https://blog.brownplt.org/2014/01/17/typechecking-jquery.html): jquery, web, types

    [Thinking the unthinkable](https://tomasp.net/blog/2016/thinking-unthinkable/): barriers, generations, point of view, science

    [Math is your insurance policy](https://bartoszmilewski.com/2020/02/24/math-is-your-insurance-policy/]): correctness, safe, milewski, meta

    [Why Functional Programming Matters](https://www.cs.kent.ac.uk/people/staff/dat/miranda/whyfp90.pdf): huges, meta, safety

    [Haskell vs. Ada vs. C++ vs. Awk vs. ... - An Experiment in Software Prototyping Productivity](http://www.cs.yale.edu/publications/techreports/tr1049.pdf): hudak, jones, meta

    [HalVM - Galois Inc.](https://galois.com/project/halvm/): virtual machine, architecture, efficiency, galois

    ### Interesting Companies

    [Galois](https://galois.com/)

    [tweag I/O](https://www.tweag.io/join-us)

    [Serokell](https://serokell.io/)

    [FPComplete](https://www.fpcomplete.com/)

    ### Conferences

    [MuniHac](https://munihac.de/2018.html)

    [ZuriHac](https://zfoh.ch/zurihac2020/)

    [Monadic Party](https://monadic.party/)

    [Strageloop](https://www.thestrangeloop.com/)

    [Curry On](https://www.curry-on.org/2018/)

    [Other Conferences](https://purelyfunctional.tv/functional-programming-conferences/)

  6. haskie-lambda revised this gist Apr 18, 2020. 1 changed file with 16 additions and 0 deletions.
    16 changes: 16 additions & 0 deletions bookmarks.md
    View file
    Original file line number Diff line number Diff line change
    @@ -7,21 +7,37 @@ A collection of bookmarks covering the topics of
    - 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
  7. haskie-lambda created this gist Apr 18, 2020.
    242 changes: 242 additions & 0 deletions bookmarks.md
    View file
    Original file line number Diff line number Diff line change
    @@ -0,0 +1,242 @@
    # 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](https://www.microsoft.com/en-us/research/uploads/prod/1987/01/slpj-book-1987-r90.pdf): 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](https://arxiv.org/pdf/1610.07978.pdf)
    [Advanced topics in types and programming languages, Benjamin C. Pierce](https://b-ok.cc/book/490535/9f7156)
    [Optics by example, Chris Penner](https://b-ok.cc/book/5332887/d426b5): An excellent introduction to all things optics related
    [Types and Programming Languages, Benjamin C. Pierce](https://b-ok.cc/book/655939/ecbfc7)
    [Programming in Martin Löfs Type Theory](https://b-ok.cc/book/687341/f5b77b)
    [Homotopy Type Thoery: Univalent Foundations of Mathematics](https://hott.github.io/book/nightly/hott-online-1246-g494c5db.pdf): 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](https://arxiv.org/pdf/1612.09375.pdf): also for the mathemaically inclined, but evertheless very interesting; contains some good excercises.
    [Write Yourself a Scheme in 48 Hours](https://en.wikibooks.org/wiki/Write_Yourself_a_Scheme_in_48_Hours/)
    [Up to date Real World Haskell](https://github.com/tssm/up-to-date-real-world-haskell)
    [Purely Functional Data Structures, Chris Okasaki](https://www.cs.cmu.edu/~rwh/theses/okasaki.pdf): 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](https://www.thelittletyper.com/): a book on dependent types
    [The Logic of Provability, Boolos](https://www.amazon.com/Logic-Provability-George-S-Boolos/dp/0521483255)
    [Verified Functional Programming in Agda, Aaron Stump](https://dl.acm.org/doi/pdf/10.1145/2841316?download=false)
    [Software Foundation Series, Bemjamin C. Pierce](https://softwarefoundations.cis.upenn.edu/current/index.html)

    ## Mastering Haskell
    [Functional Programming with Overloading andHigher-Order Polymorphism, Mark P. Jones](http://web.cecs.pdx.edu/~mpj/pubs/springschool95.pdf): typeclasses, jones
    [Kleisli arrows of outrageous fortune, CONOR McBRIDE](https://personal.cis.strath.ac.uk/conor.mcbride/Kleisli.pdf): monads, category theory, functional pearl
    [Fast Incremental Regular Expression Matcihng](http://blog.sigfpe.com/2009/01/fast-incremental-regular-expression.html): monoids, regex
    [Beyond Regurar Expressions: More incremental String Matching](http://blog.sigfpe.com/2009/01/beyond-regular-expressions-more.html): monoids, regex
    [Word numbers, Part 1: Billion approaches](http://conway.rutgers.edu/~ccshan/wiki/blog/posts/WordNumbers1/): monoids
    [Extensible Effects](http://okmij.org/ftp/Haskell/extensible/exteff.pdf): effect system
    [Arrows and Computation](http://www.staff.city.ac.uk/~ross/papers/fop.html): arrows, category theory
    [Arrow Calculus](http://homepages.inf.ed.ac.uk/wadler/papers/arrows/arrows.pdf): arrows, category theory, functional pearl, wadler
    [Evaluating Cellular Automata is Comonadic](http://blog.sigfpe.com/2006/12/evaluating-cellular-automata-is.html): comonad, automaton, theoretical cs
    [Comonads](https://bartoszmilewski.com/2017/01/02/comonads/): comonad, milewski
    [The Essence of Dataflow Programming](http://cs.ioc.ee/~tarmo/papers/essence.pdf): comonads, stream
    [Catamorphisms](https://wiki.haskell.org/Catamorphisms): catamorphism, wiki, category theory
    [Functional programming with bananas, lenses, envelopes and barbed wire](https://link.springer.com/chapter/10.1007%2F3540543961_7): datatypes, natural transformations, recursion schemes
    [Parametricity for Bifunctor](https://byorgey.wordpress.com/2018/03/30/parametricity-for-bifunctor/): bifunctors, typeclasses
    [Hasochism: The Pleasure and Pain of Dependently Typed Haskell Programming](https://personal.cis.strath.ac.uk/conor.mcbride/pub/hasochism.pdf): dependent types
    [The Yoneda Lemma](http://blog.sigfpe.com/2006/11/yoneda-lemma.html): category theory, yoneda
    [Backwards IxApplicative for IxBackwards](https://www.reddit.com/r/haskell/comments/dtntre/backwards_ixapplicative_for_ixbackwards/): applicatives, typeclasses
    [Can we have infinite sum types?](https://www.reddit.com/r/haskell/comments/e7kon1/can_we_have_infinite_sum_types): datatypes, sum types, category theory

    [The reasonable effectiveness of the continuation monad](https://blog.poisson.chat/posts/2019-10-26-reasonable-continuations.html): continuations, monads
    [Does seq cause mutation?](https://www.reddit.com/r/haskell/comments/e9nbx1/does_seq_cause_mutation/): evaluation, seq, mutation
    [Web Programming and Streaming Data in Haskell](https://www.snoyman.com/reveal/conduit-yesod#/25): slides, conduit, streaming, yesod, web
    [The rio library](https://github.com/commercialhaskell/rio#readme): rio, library, commercial, prelude
    [rio: A standard library](https://tech.fpcomplete.com/haskell/library/rio): rio, library, commercial, prelude
    [Beware of readFile](https://www.snoyman.com/blog/2016/12/beware-of-readfile): snoyman, readFile, file, read, commercial
    [Parse don't validate](https://lexi-lambda.github.io/blog/2019/11/05/parse-don-t-validate/): parsing, validation, input, types
    [The Monad.Reader Mini Issue 24: Predicates, Trees, GADTs](https://themonadreader.files.wordpress.com/2015/08/issue24.pdf): monad reader, predicates, trees, gadts
    [Monoids and Finger Trees](https://apfelmus.nfshost.com/articles/monoid-fingertree.html): monoid, data structues, datatypes, okasaki, finger trees
    [Applicative programming with effects, CONOR MCBRIDE](http://strictlypositive.org/IdiomLite.pdf): applicatives, effects, functional pearl, effect system
    [Parametricity: Money for Nothing and Theorems for Free](https://bartoszmilewski.com/2014/09/22/parametricity-money-for-nothing-and-theorems-for-free/): milewski, theorems for free, category theory, types
    [Parsing context-sensitive languages with Applicative](https://byorgey.wordpress.com/2012/01/05/parsing-context-sensitive-languages-with-applicative/): parsing, applicative, theoretical cs
    [The Mother of all Monads](http://blog.sigfpe.com/2008/12/mother-of-all-monads.html): monads, continuations, category theory
    [Dependently Typed Haskell in Industry (Experience Report)](https://www.reddit.com/r/haskell/comments/e9sjmz/dependently_typed_haskell_in_industry_experience/): galois, commertial, dependent types, verificaion, conference, lecture
    [A Role for Dependent Types in Haskell](https://www.youtube.com/watch?v=0udX2HqFUD8): dependent types, conference, lecture
    [Using the Indexed State Monad and Dependent Types to represent a Game of Texas Hold ‘Em](https://santiagoweight.wordpress.com/2019/10/25/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](http://blog.sigfpe.com/2006/11/from-l-theorem-to-spreadsheet.html): theoretical cs, comonads
    [Monad Transformer State](https://www.youtube.com/watch?v=KZIN9f9rI34): snoyman, monad transformer, conference, lecture
    [A Little Taste of Dependent Types](https://www.youtube.com/watch?v=VxINoKFm-S4): christiansen, dependent types, little typer
    [Asynchronous Exception Handling in Haskell](https://tech.fpcomplete.com/blog/2018/04/async-exception-handling-haskell): exceptions, parallel, async
    [How to Handle Asynchronous Exceptions in Haskell](https://tech.fpcomplete.com/blog/how-to-handle-asynchronous-exceptions-in-haskell): exceptions, parallel, async, lecture
    [How to Script with Stack](https://tech.fpcomplete.com/haskell/tutorial/stack-script): stack, scripting, devenv
    [Lenses](https://tech.fpcomplete.com/haskell/tutorial/lens): lenses, tutorial
    [IO Inside](https://wiki.haskell.org/IO_inside): wiki, io, monads
    [stm: Software Transactional Memory](https://tech.fpcomplete.com/haskell/library/stm): stm, parallel, async
    [The ReaderT Design Pattern](https://tech.fpcomplete.com/blog/2017/06/readert-design-pattern): reader, monad transformer, design
    [Strict WriterT monad transformer](https://mail.haskell.org/pipermail/libraries/2012-October/018599.html): writer, monad transformer
    [Revisiting pattern match overlap checks in Haskell ](https://www.reddit.com/r/ProgrammingLanguages/comments/eda7hs/revisiting_pattern_match_overlap_checks_in/): jones, conference, lecture, pattern matching, completeness, exhaustive
    [Escape from the ivory tower: the Haskell journey](https://www.youtube.com/watch?v=re96UgMk6GQ): jones, conference, lecture, history
    [Can Programming Be Liberated from the von Neumann Style? A Functional Style and Its Algebra of Programs](http://www.csc.villanova.edu/~beck/csc8310/BackusFP.pdf): backus, turing award, paradigms, algebra
    [Semigroup Resonance FizzBuzz](https://blog.ploeh.dk/2019/12/30/semigroup-resonance-fizzbuzz/): catamorphism, lazyness, stream, fizzbuzz
    [Haskell2010 Language Report](https://www.haskell.org/onlinereport/haskell2010/): language report, documentation
    [Intro to Parsing with Parsec in Haskell](https://jakewheat.github.io/intro_to_parsing/): library, parsing, tutorial
    [Haskell Problems For a New Decade](http://www.stephendiehl.com/posts/decade.html): diehl, problems
    [String Types](https://tech.fpcomplete.com/haskell/tutorial/string-types): text, string, bytestring, lazy, strict, tutorial
    [Covariance and Contravariance](https://tech.fpcomplete.com/blog/2016/11/covariance-contravariance): snoyman, covariance, contravariance, category theory, functors
    [The constraint trick for instances](https://chrisdone.com/posts/haskell-constraint-trick/): constraints, typeclasses, ~
    [Partial Type Constructors - Or, Making Ad Hoc Datatypes Less Ad Hoc](https://www.reddit.com/r/haskell/comments/f0x6mx/partial_type_constructors_or_making_ad_hoc/): datatypes, partial, complete, exhaustive, language
    [Haskell List Syntax and construction](https://www.reddit.com/r/ProgrammerHumor/comments/f6m5fh/haskell/): lists, syntax, constructors, typeclasses, typeclass recursion
    [Primitive Haskell](https://tech.fpcomplete.com/haskell/tutorial/primitive-haskell): primitives, lowlevel, implementation
    [Evaluation order and state tokens](https://wiki.haskell.org/Evaluation_order_and_state_tokens): evaluation, monads, state, io
    [Applied Haskell Syllabus](https://tech.fpcomplete.com/haskell/syllabus): commertial, tutorial
    [Type Safety Back and Forth](https://www.parsonsmatt.org/2017/10/11/type_safety_back_and_forth.html): types, safe
    [The Design and Use of QuickCheck](https://begriffs.com/posts/2017-01-14-design-use-quickcheck.html): quickcheck, testing, tutorial
    [Existential Quantification](https://markkarpov.com/post/existential-quantification.html): quantification, forall, existential, types
    [Plucking Constraints](https://www.parsonsmatt.org/2020/01/03/plucking_constraints.html): constraints, typeclasses, design
    [Lenses, Folds and Traversals: An Introduction to the Lens Library with Edward Kmett](https://vimeo.com/56063074): ekmett, lens, fold, traversal, lecture
    [Haskell's kind system - a primer](https://diogocastro.com/blog/2018/10/17/haskells-kind-system-a-primer/): kinds, types, polymorphism, unboxed, dependent types
    [Linear Haskell: practical linearity in a higher-order polymorphic language](https://www.youtube.com/watch?v=t0mhvd3-60Y): linear types, omega, jones
    [Announcing n-ary-functor-1.0](https://www.reddit.com/r/haskell/comments/ety9hv/announcing_naryfunctor10/): functors, arity
    [Levity Polymorphism](https://www.youtube.com/watch?v=lSJwXZ7vWBw): eisenberg, levity, polymorphism, lifted
    [Categories for the Working Hacker](https://www.youtube.com/watch?v=gui_SE8rJUM): wadler, conference, lecture, category theory
    [A practical Template Haskell tutorial](https://wiki.haskell.org/A_practical_Template_Haskell_Tutorial): template, meta programming, tutorial
    [Template Meta Programming for Haskell](https://www.microsoft.com/en-us/research/publication/template-meta-programming-for-haskell/?from=http://research.microsoft.com/~simonpj/papers/meta-haskell/): jones, template, meta programming
    [Algebraic lenses](https://chrispenner.ca/posts/algebraic): algebra, lenses, penner, category theory
    [Parsers and Builders as Prisms](https://yairchu.github.io/posts/codecs-as-prisms.html): parsing, prisms, category theory
    [Software Design and Architecture in Haskell](https://github.com/graninas/software-design-in-haskell/blob/master/README.md): collection, links, design, commertial
    [Pattern Synonyms Proposal](https://gitlab.haskell.org/ghc/ghc/-/wikis/pattern-synonyms): pattern synonyms, pattern matching
    [Pattern Synonyms](https://www.microsoft.com/en-us/research/wp-content/uploads/2016/08/pattern-synonyms-Haskell16.pdf): jones, eisenberg, pattern synonyms, pattern matching
    [GADTs meet their match: pattern-matching warnings that account for GADTs, guards, and laziness](https://www.microsoft.com/en-us/research/publication/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](http://cl-informatik.uibk.ac.at/users/sgimenez/data/articles/soi.pdf): curry-howard, linear logic, inference, girard
    [Practical Data Processing With Haskell and Putting Cloud Haskell to Work](https://vimeo.com/53906049): data processing, commertial, web, cloud
    [Introduction to Singletons](https://blog.jle.im/entry/introduction-to-singletons-1.html): singleton, tutorial, dependent types, gadts
    [Haskell generics explained](https://markkarpov.com/tutorial/generics.html): generics, tutorial
    [Understanding F-Algebras](https://bartoszmilewski.com/2013/06/10/understanding-f-algebras/): milewski, algebra, category theory, catamorphisms
    [Maybe catamorphism](https://blog.ploeh.dk/2019/05/20/maybe-catamorphism/): catamorphism, maybe
    [Five benefits to using StandaloneKindSignatures](https://ryanglscott.github.io/2020/01/05/five-benefits-to-using-standalonekindsignatures/): kinds, standalone, signature
    [A Type-Safe Approach to Categorized Data](https://epeery.com/typesafe-approach-to-categorized-data/): categorized data, types, safe, design
    [Case study: migrating from lens to optics](https://oleg.fi/gists/posts/2020-01-25-case-study-migration-from-lens-to-optics.html): lens, optics
    [Transformations on Applicative Concurrent Computations](https://tech.fpcomplete.com/blog/transformations-on-applicative-concurrent-computations): transformations, applicative, concurrently
    [The Thoralf Plugin: For Your Fancy Type Needs](https://repository.brynmawr.edu/cgi/viewcontent.cgi?article=1081&context=compsci_pubs): eisenberg, plugin, compiler, fancy types
    [OutsideIn(X) - Modular type inference with local assumptions](https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/jfp-outsidein.pdf): type inference, dependent types, jones, gadts, typeclasses
    [Getting a Quick Fix on Comonads](https://www.youtube.com/watch?v=F7F-BzOB670): comonads, tutorial, lecture
    [GHC Users Guide](https://downloads.haskell.org/~ghc/latest/docs/html/users_guide.html): ghc, users guide, documentation
    [Faking It - Simulating Dependent Types in Haskell](http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.22.2636&rep=rep1&type=pdf): dependent types
    [Preventing memoization in (AI) search problems](http://okmij.org/ftp/Haskell/index.html): memoization, ai
    [Generalised Algebraic Datatypes](https://wiki.haskell.org/Generalised_algebraic_datatype): gadts, wiki
    [Gadt:AlmostDependentTypes](https://akaposi.github.io/away_day/balestrieri.pdf): lecture, slides, gadts, dependent types
    [Dependent Types In Haskell](https://www.schoolofhaskell.com/user/konn/prove-your-haskell-for-great-safety/dependent-types-in-haskell): dependent types, tutorial
    [Programming with Refinement Types - Tutorial](http://ucsd-progsys.github.io/liquidhaskell-tutorial/): refinement types, liquid types, tutorial
    [Programming with Refinement Types](http://ucsd-progsys.github.io/liquidhaskell-tutorial/book.pdf): refinement types, liquid types

    ## Category Theory
    [From Design Patterns to Category Theory](https://blog.ploeh.dk/2017/10/04/from-design-patterns-to-category-theory/): design patterns
    [Do monad transformers, generally speaking, arise out of adjunctions?](https://stackoverflow.com/questions/56726854/do-monad-transformers-generally-speaking-arise-out-of-adjunctions): monad transformers, adjunctions
    [Monads for functional programming](https://homepages.inf.ed.ac.uk/wadler/papers/marktoberdorf/baastad.pdf): wadler, monads
    [Comprehending Monads](https://ncatlab.org/nlab/files/WadlerMonads.pdf): wadler, monads, tutorial
    [Propositions as Types](https://homepages.inf.ed.ac.uk/wadler/papers/propositions-as-types/propositions-as-types.pdf): wadler, propositions, logic, type theory, verification
    [Catamorphisms](https://blog.ploeh.dk/2019/04/29/catamorphisms/): catamorphisms
    [Category Theory for Pogrammers I](https://www.youtube.com/watch?v=I8LbkfSSR58&list=PLbgaMIhjbmEnaH_LTkxLI7FMa2HsnawM_): milewski, lecture
    [Category Theory for Programmers II](https://www.youtube.com/watch?v=3XTQSx1A3x8&list=PLbgaMIhjbmElia1eCEZNvsVscFef9m0dm): milewski, lecture
    [Category Theory for Programmers III](https://www.youtube.com/watch?v=F5uEpKwHqdk&list=PLbgaMIhjbmEn64WVX4B08B4h2rOtueWIL): milewski, lecture

    ## TypeTheory
    [A Unifying Theory of Dependent Types - the schematic approach](https://www.researchgate.net/profile/Zhaohui_Luo/publication/225233240_A_unifying_theory_of_dependent_types_the_schematic_approach/links/0deec52a1025ec6518000000/A-unifying-theory-of-dependent-types-the-schematic-approach.pdf?origin=publication_detail): dependent types

    ### Wikipedia Links
    [Intuitionistic logic](https://en.wikipedia.org/wiki/Intuitionistic_logic): intuitionistic logic, löf, dependent types, lambda cube, fomega
    [Calculus of constructions](https://en.wikipedia.org/wiki/Calculus_of_constructions): coq, inductive constructions, calculus, lambda cube, lambdac
    [Curry-Howard correspondence](https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence): curry-howard, correspondence, isomorphism
    [Homotopy type theory](https://en.wikipedia.org/wiki/Homotopy_type_theory): hott, homotopy, topology, infinite groupoids
    [Typed lambda calculus](https://en.wikipedia.org/wiki/Typed_lambda_calculus): types, lambda calculus, church
    [Hindley-Milner type inference](https://en.wikipedia.org/wiki/Hindley%E2%80%93Milner_type_inference): type inference, types, milner, hindley
    [Simply typed lambda calculus](https://en.wikipedia.org/wiki/Simply_typed_lambda_calculus): church, types, lambda calculus
    [LF (logical framework)](https://en.wikipedia.org/wiki/LF_(logical_framework)): logical, framework, higher order logic
    [Example of type in System F that is not available in Hindley Milner type inference](https://stackoverflow.com/questions/23995736/example-of-type-in-system-f-that-is-not-available-in-hindley-milner-type-inferen): system f, hindley, milner, types, inference
    [Dependent Type theory](https://en.wikipedia.org/wiki/Dependent_type_theory): dependent types
    [Intuitionistic Type Theory](https://en.wikipedia.org/wiki/Intuitionistic_type_theory): löf, intuitionistic type theory
    [Pure Type System](https://en.wikipedia.org/wiki/Pure_type_system): type system, pure, generalised
    [Lambda Cube](https://en.wikipedia.org/wiki/Lambda_cube): higher order, type system, system f, fomega, typed, coq, constructions
    [Second Order Lambda Calculus](https://en.wikipedia.org/wiki/Second_order_lambda_calculus): higher order, calculus, system f, girard, reynolds
    [Girard's paradox](https://en.wikipedia.org/wiki/Girard%27s_paradox): girard, paradox
    [Propositions as Types](https://homepages.inf.ed.ac.uk/wadler/papers/propositions-as-types/propositions-as-types.pdf): wadler, propositions, logic, type theory, category theory, verification
    [The Fun of Programming - Fun with Phantom Types](http://www.cs.ox.ac.uk/ralf.hinze/publications/With.pdf): phantom types

    ## Formal Verification related

    [Developing Bug-Free Machine Learning SystemsWith Formal Mathematics](https://arxiv.org/pdf/1706.08605.pdf): ai
    [Lean](https://leanprover.github.io/theorem_proving_in_lean/tactics.html): proof assistant
    [Verified Programming Based on Univalent Foundations in Agda - Part 0](https://maxbaroi.gitlab.io/posts/2020-04-17-Basics.html): hott, agda, tutorial
    [Arend](https://arend-lang.github.io/about/arend-features): proof assistant
    [Twelf](https://en.wikipedia.org/wiki/Twelf): proof assistant
    [Lecture Series for Software Foundation Series](https://www.youtube.com/watch?v=KKrD4JcfW90&list=PLGCr8P_YncjUT7gXUVJWSoefQ40gTOz89): lecture, pierce, software foundations
    [Agda vs. Coq vs. Idris](https://whatisrt.github.io/dependent-types/2020/02/18/agda-vs-coq-vs-idris.html): agda, coq, idris
    [Propositions as Types](https://homepages.inf.ed.ac.uk/wadler/papers/propositions-as-types/propositions-as-types.pdf): wadler, propositions, logic, type theory, category theory, verification
    [HOL Theorem Prover](https://hol-theorem-prover.org/#where-to-start): proof assistant, theorem proover
    [Isabelle](https://isabelle.in.tum.de/): theorem prover, proof assistant
    [FStar](https://www.fstar-lang.org/tutorial/): programming language

    ## PLT
    [An Intuition for propagators](https://www.reddit.com/r/haskell/comments/dy8joz/george_wilson_an_intuition_for_propagators/): propagators, electrical circuits, simulation, computatoinal model
    [On the Expressive Power of Programming Languages](https://link.springer.com/content/pdf/10.1007/3-540-52592-0_60.pdf): expression, semantics, translation, thinking process
    [What is your favourite academic paper on Programming Language Theory?](https://www.reddit.com/r/ProgrammingLanguages/comments/dwt8xu/what_is_your_favourite_academic_paper_on/): collection, links
    [dex-lang - Research Language for Array Processing in the Haskell/ML family](https://google-research.github.io/dex-lang/regression.html): programming language, google, dex, array, index, list
    [Incorrectness Logic by Example](https://hexgolems.com/2020/04/incorrectness-logic-by-example/): logic, incorrectness
    [What are the major open problems/issues with functional programming or Haskell right now?](https://www.reddit.com/r/haskell/comments/fmthoy/what_are_the_major_open_problemsissues_with/): problems, issues, functional
    [Executable Grammars: Seeking the minimal extensible self-compiling compiler (2009)](https://www.reddit.com/r/ProgrammingLanguages/comments/enr99b/executable_grammars_seeking_the_minimal/): grammar, compiler, plt

    ## Tools and libraries
    [ghcid](https://github.com/ndmitchell/ghcid): Very low feature GHCi based IDE
    [The rio library](https://github.com/commercialhaskell/rio#readme): rio, library, commercial, prelude
    [Grapefruit](https://wiki.haskell.org/Grapefruit): library, reactive
    [tweag/asterius - A Haskell to WebAssembly compiler](https://github.com/tweag/asterius): webassembly, web, transpiler
    [Typable and Data in Haskell](https://chrisdone.com/posts/data-typeable/): library, typeclasses, polymorphism, ad-hoc, tutorial
    [optparse-applicative - Applicative option parser](https://github.com/pcapriotti/optparse-applicative/blob/master/README.md): library, commandline options, parsing
    [A fast, flexible, fused effect system for Haskell](https://github.com/fused-effects/fused-effects): effect system, fused-effects, library, effects, monads
    [polysemy - higher-order, no-boilerplate, zero-cost monads](https://github.com/polysemy-research/polysemy): effect system, effects, library, monads
    [eff - a work in progress effect system for Haskell](https://github.com/hasura/eff): effect system, effects, monads, library
    [ComonadSheet - A library for expressing "spreadsheet-like" computations](https://github.com/kwf/ComonadSheet): library, comonads, spreadsheets, cellular automatons, plt
    [LiquidHaskell - Liquid Types For Haskell](https://github.com/ucsd-progsys/liquidhaskell): library, liquid types

    ### Functional Graphics
    [LambdaCube3D](https://lambdacube3d.wordpress.com/)
    [Futhark](https://futhark-lang.org/)
    [Rumpus](https://github.com/lukexi/rumpus)

    ## Misc
    [The Power of Prolog](https://www.metalevel.at/prolog): prolog
    [Typechecking Uses of the jQuery Language](https://blog.brownplt.org/2014/01/17/typechecking-jquery.html): jquery, web, types
    [Thinking the unthinkable](https://tomasp.net/blog/2016/thinking-unthinkable/): barriers, generations, point of view, science
    [Math is your insurance policy](https://bartoszmilewski.com/2020/02/24/math-is-your-insurance-policy/]): correctness, safe, milewski, meta
    [Why Functional Programming Matters](https://www.cs.kent.ac.uk/people/staff/dat/miranda/whyfp90.pdf): huges, meta, safety
    [Haskell vs. Ada vs. C++ vs. Awk vs. ... - An Experiment in Software Prototyping Productivity](http://www.cs.yale.edu/publications/techreports/tr1049.pdf): hudak, jones, meta
    [HalVM - Galois Inc.](https://galois.com/project/halvm/): virtual machine, architecture, efficiency, galois

    ### Interesting Companies
    [Galois](https://galois.com/)
    [tweag I/O](https://www.tweag.io/join-us)
    [Serokell](https://serokell.io/)
    [FPComplete](https://www.fpcomplete.com/)

    ### Conferences
    [MuniHac](https://munihac.de/2018.html)
    [ZuriHac](https://zfoh.ch/zurihac2020/)
    [Monadic Party](https://monadic.party/)
    [Strageloop](https://www.thestrangeloop.com/)
    [Curry On](https://www.curry-on.org/2018/)
    [Other Conferences](https://purelyfunctional.tv/functional-programming-conferences/)