-
-
Save xgrommx/5e5b0c3462cdc1fbd29ba5aabe48de29 to your computer and use it in GitHub Desktop.
Lambda Calculus Notation with Nameless Dummies
I am not a Number—I am a Free Variable
Parametric Higher-Order Abstract Syntax for Mechanized Semantics
The Locally Nameless Representation
Lambda calculus cooked four ways
Using Circular Programs for Higher-Order Syntax
Abstract Syntax Graphs for Domain Specific Languages
Separate positive and negative occurrences of PHOAS variables in presence of recursive binders
Using Circular Programs for Higher-Order Syntax
https://pay.reddit.com/r/haskell/comments/4rynuq/directed_acyclic_graphs_and_phoas/
When is one thing equal to some other thing?
All Concepts are Kan Extensions
Kan extensions and nonsensical generalizations
Kan extensions for program optimization
Generic programming with adjunctions
Monads from Comonads, Comonads from Monads
Constructing Applicative Functors has stuff about coends
A Representation Theorem for Second-Order Functionals
BASIC CONCEPTS OF ENRICHED CATEGORY THEORY
Codensity and the ultrafilter monad
What Sequential Games, the Tychonoff Theorem and the Double-Negation Shift have in Common
Selection Functions, Bar Recursion, and Backward Induction
THIS IS THE (CO)END, MY ONLY (CO)FRIEND
NATURAL TRANSFORMATIONS Id −→ Id
Update Monads: Cointerpreting Directed Containers. slides
Combinatorial Species and Labelled Structures. has stuff about coends
String diagrams for free monads
How to Twist Pointers without Breaking Them
Notions of computation as monoids
From monoids to near-semirings: the essence of MonadPlus and Alternative
Parameterised Notions of Computation
Arrows, like Monads, are Monoids
categorical semantics of digital circuits
Calculating monad transformers with category theory
An Introduction to n-Categories
Higher-Dimensional Categories: an illustrated guide book
Natural Transformations as Rewrite Rules and Monad Composition
Building inference algorithms from monad transformers
Differentiating Data Structures
Containers in Homotopy Type Theory (2014)
A Meaning Explanation for HoTT
Codensity and the ultrafilter monad
Category Theroy (Oxford Logic Guides)
Higher operads, higher categories
Higher-Dimensional Categories: an illustrated guide book
Category Theory - A Gentle Introduction
A gentle introduction to Category Theory - the calculational approach
Synthetic topology of data types and classical spaces
An introduction to Category Theory with over 200 exercises and solutions available
Elements of basic category theory
Introduction to categories and categorial logic
Tom Leinster, Basic Category Theory
An introduction to geometric topology
Lecture Notes on Randomized Linear Algebra
Category Theory Foundations, Lecture 1
Categories and String Diagrams
Category theory for programmers by Bartosz Milewski
Where Do Ultrafilters Come From?
Codensity (ReaderT s m a) == StateT s (Codensity m) a
Unnatural Transformations and Quantifiers
Is Mac Lane still the best place to learn category theory?
How do I check if a functor has a (left/right) adjoint?
Good books and lecture notes about category theory
Dinatural Transformations and Coends
Kan Extensions III: As Ends and Coends
The cofree comonad and the expression problem
Comonads and Day Convolution reddit
What Are Some Example Adjunctions from Monads (or vice versa)?
What are Haskell's monad transformers in categorical terms?
Haskell monad transformers at the nForum
http://www.cs.ox.ac.uk/jeremy.gibbons/publications/fp4dsls.pdf Functional Programming for Domain-Specific Languages http://cs448h.stanford.edu/DSEL-Little.pdf hudak https://www.andres-loeh.de/HaskellForDSLs.pdf Loh https://github.com/mchakravarty/hoas-conv https://wiki.haskell.org/Embedded_domain_specific_language https://www.reddit.com/r/haskell/comments/2e8d53/whats_the_best_practice_for_building_a_dsl_in/ https://skillsmatter.com/skillscasts/2872-haskell-for-embedded-domain-specific-languages http://cacm.acm.org/magazines/2011/7/109910-dsl-for-the-uninitiated/fulltext https://www.reddit.com/r/haskell/comments/2dh0sd/denotational_design_from_meanings_to_programs_by/ http://lambda-the-ultimate.org/node/2438 http://okmij.org/ftp/tagless-final/course/lecture.pdf https://gist.github.com/PkmX/182c6c5444b695d9a794 http://homepages.inf.ed.ac.uk/slindley/papers/unembedding.pdf
Two approaches to representing variables in a typed term language implemented as a GADT are (1) to use higher-order abstract syntax (HOAS) or to use de Bruijn indices.. Both approaches are convenient for manipulating terms as they require no explicit alpha conversion and avoid name capture during substitution. Nevertheless, there are trade offs between the two. In particular, the HOAS representation doesn't support comparing variable names and the de Bruijn representation is inconvenient for humans to read and write. For a more detailed discussion, see for example Conor McBride and James McKinna's I am not a number: I am a free variable, where they discuss a mixed representation using de Bruijn indices for bound variables and variables of the meta-language for free variables.
The tension between the HOAS and de Bruijn representation also has relevance for the design and implementation of embedded domain specific languages (EDSLs) — aka internal languages. When an internal includes higher-order functions, it is usually most convenient for the user to use the function abstraction mechanisms of the host language. However, to execute or compile the internal language, de Bruijn notation is often more convenient; at least, if optimisations are performed.
http://www2.hh.se/staff/vero/dsl/printL1.pdf http://www2.hh.se/staff/vero/dsl/printL2.pdf http://www2.hh.se/staff/vero/dsl/printL3.pdf http://www2.hh.se/staff/vero/dsl/printL4.pdf http://www2.hh.se/staff/vero/dsl/printL5.pdf http://www2.hh.se/staff/vero/dsl/printL6.pdf
Typed compilation to tagless-final HOAS The embedded DSL is now higher-order: it is simply-typed lambda-calculus with the fixpoint and constants — essentially, PCF. We no longer use staging. Rather, we compile to tagless-final representation, which can be interpreted by different interpreters. Regardless of the number of interpretations of a term, the type checking happens only once. We build our own Dynamics to encapsulate typed terms and represent their types.
https://www.haskell.org/communities/11-2009/report.pdf https://en.wikipedia.org/wiki/Programming_Computable_Functions
https://mail.haskell.org/pipermail/haskell-cafe/2009-October/067425.html
https://blog.cppcabrera.com/posts/56-writing-a-search-dsl-1.html
http://gallium.inria.fr/~naxu/research/dsel.pdf
Sharing and recursion are common problems when implementing DSLs. Often some kind of observable sharing is requested that requires a deep embedding.
Oleg in Haskell-Cafe about Designing DSL with explicit sharing (was: I love purity, but it's killing me) Koen Classen: Observable Sharing for Functional Circuit Description Andy Gill: Type-Safe Observable Sharing Tom Lokhorst AwesomePrelude presentation (video) Leandro Lisboa Penz Haskell eDSL Tutorial - Shared expenses Bruno Oliveira and William Cook: Functional Programming with Structured Graphs Emil Axelsson and Koen Claessen: Using Circular Programs for Higher-Order Syntax Oleg Kiselyov: Implementing explicit and finding implicit sharing in embedded DSLs
An obvious way to relief the tension between the representations is to use HOAS in the surface representation of the internal language and to convert that to the de Bruijn representation before optimisation and execution. However, the conversion is not entirely straight forward for a strongly typed internal language with typed intermediate representations and type-preserving transformations between those representations.
http://www.iro.umontreal.ca/~monnier/tcm.pdf
Implementing Explicit and Finding Implicit Sharing in Embedded DSLs
I love purity, but it's killing me
Simple and Compositional Reification of Monadic Embedded Languages
https://www.reddit.com/r/haskell/comments/4ck2yh/compilation_as_a_typed_edsltoedsl_transformation/
The Difference Between Shallow and Deep Embedding
Certifying Machine Code Safety: Shallow versus Deep Embedding
Shallow versus Deep Embeddings
Embedded domain specific language (links)
Using Circular Programs for Higher-Order Syntax
Implementing Explicit and Finding Implicit Sharing in Embedded DSLs
Type-Safe Observable Sharing in Haskell
An Image Processing Language: External and Shallow/Deep Embeddings
Fizzbuzz in Haskell by embedding a DSL
Compilation as a Typed EDSL-to-EDSL Transformation
Combining deep and shallow embedding of domain-specific languages
##slides
Combining deep and shallow embeddings: a tutorial
Building Small Native Languages with Haskell
##videos
Type-Safe Observable Sharing in Haskell
https://skillsmatter.com/skillscasts/2872-haskell-for-embedded-domain-specific-languages
Strongly Typed Domain Specific Embedded Languages
Everything Old is New Again: Quoted Domain Specific Languages
Implementing Domain Specific Languages with LLVM
Phil Freeman - Embedded DSLs in Haskell
Finally tagless, partially evaluated
Finally, Safely-extensible and Efficient Language-integrated Query
Reducing boilerplate in finally tagless style
Typed Tagless Interpretations and Typed Compilation
From object algebras to finally tagless interpreters
Tagless Staged Interpreters for Simpler Typed Languages
Push-pull functional reactive programming
Functional Reactive Programming, Continued
Efficient and Compositional Higher-Order Streams
Synchronous Functional Programming: The Lucid Synchrone Experiment
Causal commutative arrows, revisited
Functional Reactive Programming, Refactored
FRP - Dynamic event switching in reactive-banana-0.7
FRP — API redesign for reactive-banana 1.0
How to implement a game loop in reactive banana?
Time delays in reactive banana
Beliefs and the Unimpossibility of Functional Reactive Programming
What's the status of current Functional Reactive Programming implementations?
My thoughts after spending 5 month writing an frp library
basic propositional linear logic
Temporal logic and functional reactive programming
Functional Reactive Programming
Functional Reactive Programming in Java
Making Reactive Programs Function part2
From what I can read here and there, Netwire and reactive-banana have different purposes and goals. Netwire specialises in modelising framed signals, such as a game server, because what a game server typically does is sending its state to client in periodic frames. Reactive-banana would be the better choice for creating a GUI because a GUI is a purely event-driven model and is not tolerant to time leak.
netwire: Useful library, but needs maintenance and has high maintenance cost due to its design. I'll likely replace it by a new abstraction at some point, using a different package name. Currently I recommend using one of the following libraries for FRP:
reactive-banana: My former favourite when it comes to push/pull FRP. Well designed, clean semantics, reasonably efficient.
reflex: My current favourite when it comes to push/pull FRP. Well designed, clean semantics, reasonably efficient.
Yampa: AFRP for games, simulations and other real-time applications (for when a high and predictable framerate is more important than pushed events, same target domain as Netwire).
Evan Czaplicki's talk (https://www.youtube.com/watch?v=Agu6jipKfYw) linked in frp-zoo is great! After watching it I would say that varying is definitely in his Arrowized FRP category. The main type in varying is an instance of Arrow. Signals are not connected to the world, and when a signal is not being run - it's cold. Unlike Netwire, varying doesn't have implicit time or inhibition. A Netwire 'wire' written in varying would be something like Monad m => Var m t (Event b) where t is time and b is the value. Event allows inhibition explicitly. Unlike Auto, varying is small and more focused on tweening and allowing you to build data structures that change in a smooth manner over time (or another domain). Auto has a lot of extra functionality like serialization, etc. I purposefully made the varying API tiny in an effort to make learning it really easy. They're all capable of expressing one another in their own terms though, so they're all worth a visit.
Auto is at least as much "FRP" as elerea. Purists to Elliot's approach, notably including Auto's author, will tell you neither one is FRP at all. Five years ago I'd probably be agreeing with them, but IMO at this point that ship has sailed.
Cheney, Bisimulation and Coinduction for Dummies
Sangiorgi, An Introduction to Bisimulation and Coinduction
A Tutorial on (Co)Algebras and (Co)Induction
Practical Coinduction A property holds by induction if there is good reason for it to hold; whereas a property holds by coinduction if there is no good reason for it not to hold.
On proof and progress in Mathematics
A taste of linear logic / linear thoughts
Proof by Coinduction coinduction is going to rely on the fact that epimorphisms from terminal coalgebras are isomorphisms, i.e., there’s no quotient coalgebra of a terminal coalgebra.
Boltzmann Samplers for the Random Generation of Combinatorial Structures
Generating Constrained Random Data with Uniform Distribution
A Hybrid Convolutional Variational Autoencoder for Text Generation
The Multiplicative Weights Update Method
Relational Lattices: From Databases to Universal Algebra
Dependency grammars as Haskell programs
(The Origins of the Linguistic Conception of Computer Programming)[https://pure.uva.nl/ws/files/2419813/154677_Alberts_Nofre_Priestly_Technol_Culture_55_1_2014.pdf] also hn
DEEP LEARNING WITH DYNAMIC COMPUTATION GRAPHS
Nested monadic loops may cause space leaks
Robert Harper's Homotopy type theory course
proofs as processes OPLSS 2012
software foundations in coq OPLSS 2013
polarization and focalization OPLS 2013
type theory foundations OPLSS 2014
category theory foundation OPLSS 2014
introduction to dependent type theory OPLSS 2015
Basic Category Theory: Semantics of Proof Theory — Ed Morehouse OPLSS 2015
proofs as processes OPLSS 2015
Category Theory Background OPLSS 2016
Patricia Johann Lecture 1, OPLSS 2016 logical relations
Programming Languages Background — Robert Harper and Dan Licata OPLSS 2016 2016
Network Programming — Nate Foster OPLSS 2016
Separation Logic and Concurrency — Aleks Nanevski OPLSS 2016
Principles of Type Refinement — Noam Zeilberger OPLSS 2016
Logical relations/Compiler verification — Amal Ahmed OPLSS 2016
Automated Complexity Analysis — Jan Hoffmann OPLSS 2016
##posts
Call-By-Name, Call-By-Value and the λ-Calculus
the three projections of doctor Futamura
Random access lists, nested data types and numeral systems
Papers We Love: John Reynolds, Definitional Interpreters for Higher-Order Programming Languages video
Fold and unfold for program semantics
#papers
Linear types can change the world
Polarized Data Parallel Data Flow from
About the efficient reduction of lambda terms
#books
Program Calculation Properties of Continuous Algebras
Functional Programming with Bananas, Lenses, Envelopes and Barbed Wire
A tutorial on the universality and expressiveness of fold
Factorising Folds for Faster Functions
When is a function a fold or an unfold?
Constructively Characterizing Fold and Unfold
FUNCTIONAL PROGRAMMING WITH APOMORPHISMS (CORECURSION)
Metamorphisms: Streaming Representation-Changers
Primitive (Co)Recursion and Course-of-Value (Co)Iteration, Categorically
Histo- and Dynamorphisms Revisited
Recursion Schemes for Dynamic Programming
Sorting with Bialgebras and Distributive Laws
Unifying Structured Recursion Schemes
Reasoning about Algebraic Data Types with Abstractions
A Translation from Attribute Grammars to Catamorphisms
Attribute Grammars as Recursion Schemes over Cyclic Representations of Zippers
Calculating Certified Compilers for Non-Deterministic Languages
Designing and Implementing Combinator Languages
The design of a pretty-printing library (Hughes)
Higher-Order Recursion Abstraction
Haskell Programming with Nested Types: A Principled Approach
Recursion schemes for dummies?
Recursion Schemes: A Field Guide
An Introduction to Recursion Schemes
Recursion Schemes, Part 2: A Mob of Morphisms
Grokking recursion-scheme: Part 1
Grokking recursion-scheme: Part 2
Dynamorphisms as chronomorphisms
Histomorphisms, Zygomorphisms and Futumorphisms specialised to lists
Examples of histomorphisms in Haskell
Dependently typed programming with singletons
How to keep your neighbours in order
Dependent Types at Work looks like a good introduction to Agda for people with Haskell experience.
DEPENDENT TYPES IN HASKELL: THEORY AND PRACTICE Richard A. Eisenberg's thesis.
Practical Dependent Types in Haskell: Type-Safe Neural Networks reddit
Defunctionalization for the win
Better Data Types a la Carte -- with injectivity guaranteed by construction
trying fancy type stuff: is it possible to write slice for Fixed-Length vectors?
How to write a Monoid instance for something that depends on parameters
Data families vs Injective type families
Quotient types for programmers
Pattern Matching on Type Constructors? type families allow Prolog-like non-linear matches
How can quotient types help safely expose module internals?
Typesafe Printf with TypeInType
working my way through Data.Type.Equality...my head hurts
Decidable Propositional Equality in Haskell
A Functional Programmer's Guide to Homotopy Type Theory
Applying Type-Level and Generic Programming in Haskell
ZuriHac 2016: Generic (and type-level) Programming with Generics-sop