-
-
Save danidiaz/36f5647c0968361eedd677ad3870715f 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
Revisiting catamorphisms over datatypes with embedded functions
Fortunately, a year later Leonidas Fegaras and Tim Sheard realized that the main use of the 'unfold step' above was to just undo the damage caused by the fold step and that a full inverse wasn't needed
The problem the reduces to the question of how to define place. Fegaras and Sheard were willing (and able) to change every functor to include an extra member name Place and then define as part of each catamorphism that cata f (Place x) = x. They then ensured that Place wasn't abused by the programmer by a complicated type system that we really don't have access to in Haskell.
We revisit the work of Paterson and of Meijer & Hutton, which describes how to construct catamorphisms for recursive datatype definitions that embed contravariant occurrences of the type being defined. Their construction requires, for each catamorphism, the definition of an anamorphism that has an inverse-like relationship to that catamorphism. We present an alternative construction, which replaces the stringent requirement that an inverse anamorphism be defined for each catamorphism with a more lenient restriction. The resulting construction has a more efficient implementation than that of Paterson, Meijer, and Hutton and the relevant restriction can be enforced by a Hindley-Milner type inference algorithm. We provide numerous examples illustrating our method.
Boxes Go Bananas slides extended version
One fix, as noted by Washburn and Weirich is to quantify over the a with an explicit forall when working with the Fegaras/Sheard catamorphism. This has the nice side effect that it prevents illegal uses of 'Place'. Moreover, that explicit quantifier allows you to use different catamorphisms over the term.
Weirich and Washburn's encoding as an elimination form protect the user from bad case analysis by denying you the ability to inspect terms with case at all.
In other words, the only thing you can do to a term is apply a catamorphism to it. They even say as much somewhere in the paper.
No sweat, we can go rederive all of the other stuff thats defined in terms of catamorphism, right? paramorphisms, zygomorphisms, histomorphisms, generalized catamorphisms, and then we can do anything we want, right? Unfortunately, here is where we run out of steam.
A catamorphism isn't strong enough to encode general recursion without fmap. In order to rederive general recursion from a catamorphism you need at least a paramorphism. Normally we can define a paramorphism in terms of our catamorphism with the use of fmap, but as we are working over merely an exponential functor we do not have fmap!
Depending on how bad we want to be, we can get out of the Washburn/Weirich or Fegaras/Sheard sandboxes and into one of the others. Though curiously we can't get back out of the Meijer/Hutton-style unless we have a full Functor.
We do not claim that this encoding will solve all of the problems with programming using higher-order abstract syntax. In particular, algorithms that require the explicit manipulation of the names of bound variables remain outside the scope of this implementation technique.
Using cata to implement operations such as eval is convenient because the pattern of recursion is already specified. None of eval, evalAux or unevalAux are recursively defined.
Parametric Higher-Order Abstract Syntax for Mechanized Semantics slides
The Locally Nameless Representation
Lambda calculus cooked four ways
Using Circular Programs for Higher-Order Syntax
Abstract Syntax Graphs for Domain Specific Languages explains PHOAS reddit
Type-and-Scope Safe Programs and Their Proofs
A programmer implementing an embedded language with bindings has a wealth of possibilities. However, should she want to be able to inspect the terms produced by her users in order to optimise or even compile them, she will have to work with a deep embedding.
A Locally Nameless Theory of Objects
Locally Nameless Permutation Types
Functional Programming with Structured Graphs
To provide a convenient and expressive programming interface, structured graphs use a binding representation based on parametric higherorder abstract syntax (PHOAS)
Parametric Compositional Data Types
A Parallel Intermediate Representation for Embedded Languages
The HOAS allows Nikola to express let-sharing and λ-sharing, two kinds of optimisations for minimising recomputation of common subexpressions and for reducing the final code-size.
Atoms are often taken to be strings, but any countably infinite set with decidable equality will do.
Stephanie Weirich, Tim Sheard and I recently submitted a paper to ICFP entitled Binders Unbound. (You can read a draft here.) It’s about our kick-ass, I mean, expressive and flexible library, unbound (note: GHC 7 required), for generically dealing with names and binding structure when writing programs (compilers, interpreters, refactorers, proof assistants…) that work with syntax. Let’s look at a small example of representing untyped lambda calculus terms. This post is working Literate Haskell, feel free to save it to a .lhs file and play around with it yourself!
Monadic presentations of lambda terms using generic inductive types twitter
A Type Theory for Defining Logics and Proofs. Talks about HOAS.
Everybody’s Got To Be Somewhere. twitter. repo. pdf.
Secrets of the Glasgow Haskell Compiler inliner. question.
Another well-known approach to the name-capture problem to use de Bruijn numbers [dB80]. Apart from being entirely unreadable, this approach suffers from the disad- vantage that when pushing a substitution inside a lambda, the entire range of the substitution must have its de Bruijn numbers adjusted. That operation can be carried out lazily, to avoid a complexity explosion when pushing a substitution inside multiple lambdas, but that means yet more administration.
Using Circular Programs for Higher-Order Syntax. A simple alternative to De Bruijn indexing, from ICFP 2013. A simple alternative to De Bruijn indexing, from ICFP 2013.
Bound strongly-typed bound video more even more
In other words, to use the Meijer/Hutton catamorphism to write a pretty printer, you have to write a parser as well; to use it to eval, you must also be able to reify values back into programs.
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/
A Scope Safe Universe of Syntaxes with Binding, Their Semantics and Proofs
Let Idris Take Care Of You: Variable Binding
Dependable Types 2: Correctness by Construction
Is nameless representation worth the trouble?
The main goal of pretty much any story for binders isn't about saving memory, it's primarily about ensuring that we don't write unhygienic programs or program transformations, often with a secondary goal of providing fast/easy alpha-equivalence.
Using explicit names it's all too easy to break hygiene: allowing a variable to be used outside the scope in which it's bound, allowing binders to capture things they shouldn't, etc. As a particular example, correctly implementing capture-avoiding substitution is far trickier than expected. So the primary goal of any variable binding story (de Bruijn levels, de Bruijn indices, locally nameless, HOAS,...) is to get rid of these problems.
Type 'Int' does not match type 'Int'
Compiler engineering is full of traps of representation.
Differences between HOAS and FOAS
Why GADTs are awesome: implementing System F using HOAS
Separate positive and negative occurrences of PHOAS variables in presence of recursive binders
Two representations for lambda calculus terms are the Church representation, due to Thierry Coquand (left) and Gerard Huet (middle), let's call it CH, and PHOAS, due to Adam Chlipala (right), let's call it PH. Here is a Haskell program giving both encodings, and showing they are interconvertible. The CH representation is called finally tagless by Carette, Kiselyov, and Shan, which is not the most perspicuous name; Atkey, Lindley, and Yallop point out the idea goes back to Coquand and Huet; PH was introduced by Chlipala.
Converting a HOAS term GADT into a de Bruijn term GADT
Atkey, Sam Lindley & Jeremy Yallop had independently developed the same method and were about to publish it in a paper entitled Unembedding Domain-Specific Languages
I'll show how to convert between a named, a de-Bruijn, and a PHOAS representation of lambda terms. It's relatively easy to fuse that into the parser if you absolutely want to, but it's probably better to parse a named representation first and then convert.
Phoas in scala - Boxes go bananas for less
Since all the machinery is wrapped up inside of Haskell's implementation even simple operations like pretty printing and writing transformation passes can be more difficult. This form is a good form for evaluation, but not for transformation.
In the context of Haskell, Washburn and Weirich introduced a technique called parametric HOAS, or PHOAS. By making a slight alteration in the spirit of weak HOAS, we arrive at an encoding that addresses all three of the complaints above: the encoding is legal in Coq, exotic terms are impossible, and it is possible to write any syntax-deconstructing function that we can write with first-order encodings. The last of these advantages is not even present with HOAS in Twelf. In a sense, we receive it in exchange for giving up a free implementation of capture-avoiding substitution.
It is nice for languages where it is a first-class concept (e.g. Twelf, which is a logic/theorem language), but it gets complicated very quickly if you want to do AST transformations.
HOAS is a form of embedding a language L with binders into a language L-Base also with binders and functions, but such that L-binders are handled by functions in L-Base and the problem of defining capture-avoiding substitution for L-terms is reduced to reusing L-Base's capture-avoiding substitution. (NB L = L-Base is possible but not required.)
HOAS is neat, but (simplifying a bit) prevents you from making inductive definitions on L terms. There are various ways of getting around this shortcoming, the most principled one is probably the nominal approach of A. Pitts et al. Another problem with HOAS is that the representation may contain 'junk'. That means there are L-Base terms that do not represent L-programs.
It's quite ingenious but it's not as convenient as locally nameless representation for working underneath binders.
How I learned to stop worrying and love de Bruijn indices
Turning bottom-up into top-down with Reverse State
Is it possible to normalize affine λ-calculus terms using PHOAS in Agda?
A well-typed suspension calculus
Sometimes when I feel sad I implement a dependently typed lambda calculus.
unbound-generics in case expressions
I am not a number, I am a classy hack
In this post, I’ll discuss some of the issues which have driven us to a de Bruijn indexed representation of values, where once we used Haskell functions to model Epigram functions.
Remark. Whilst this is a higher-order representation of values, it is not and should not be described as ‘higher-order abstract syntax’: on the one hand, free variables have a concrete first-order representation; on the other hand, the functions in Can are permitted to analyse and compute with their arguments by pattern matching on canonical value forms. Repeat. It is not HOAS. It is an untyped approximation to a Kripke-model construction, which morally goes by structural recursion on types.
Semantics for de Bruijn levels
hoas and traversable tweet. another HOAS tweet
A Generic Abstract Syntax Model for Embedded Languages
Is it possible to convert a HOAS function to continuation passing style?
monadic presentations of lambda terms using generalized inductive types. tweet.
Syntaxes with binding form a monad indexed by the variable representation: 4.4
What are the performance characteristics of HOAS/tagless final?
What representations but de Bruijn are there to avoid the ill-defined capture-avoiding substitution?
Writing efficient free variable traversals. more.
a HOAS encoding of a subset of the XLA core ops with completely statically tracked shape information
context contains patterns, not variables
No real-world implementation of a functional language uses term substitution for beta reduction! Instead, the standard practice is to have environment machines, closures, and a separation of immutable code from value environments CEK, SECD & STG machines
Nominal: An efficient and easy-to-use library for defining datatypes with binders, and automatically handling bound variables and alpha-equivalence. A New Approach to Abstract Syntax with Variable Binding.
the implementation of (dependent) type systems. a bibliography of publications that discuss implementation of dependent type systems.
data structures that represent only closed terms
Skipping the binder bureaucracy with mixed embeddings in a semantics course (Functional Pearl)
Unembedding Domain-specific Languages
Devon Stewart - Higher Order Abstract Syntax
Phil Freeman - Embedded DSLs in Haskell slides
Type theory elaboration implementation. Playlist related to elaboration-zoo
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. Coproducts and ultrafilters. tweet. ncatlab. notes on ultrafilters.
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 evolved into the book "Coend calculus".
NATURAL TRANSFORMATIONS Id −→ Id Prove that a transformation of the identity functor of a Group G (seen as a category) into itself is just an element of the center of G
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. Selective Applicative Functors.
a sort of 'type-indexed' generalisation of Monoid, where the monoid structure is reflected at the level of types by the unit and product types (which themselves form a typelevel monoid structure up to isomorphism)
Notions of computation as monoids ext
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
AN INTRODUCTION TO ∞-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
A Type-Theoretical Definition of Weak ω-Categories
Revisiting the Futamura Projections: A Visual Tutorial
Profunctor optics - modular data accessors
Algorithmic Homological Algebra uses term "pre-inverse"
Notes on categories incomplete and never to be finished uses term "pre-cancellable"
A Prehistory of n-Categorical Physics
NOTES ON ADJUNCTIONS, MONADS AND LAWVERE THEORIES
Monads for behaviour (mentions ideal monads)
Equivalent and Inequivalent Formulations of Classical Mechanics∗ - how different equivalent categories can be?
Equivalent categories are identical except that they might have different numbers of isomorphic "copies" of the same objects.
Enriched Lawvere Theories for Operational Semantics
Backtracking with cut via a distributive law and left-zero monoids
An Investigation of the Laws of Traversals SO question
Kleisli arrows of outrageous fortune video reddit
Comprehending Ringads On ringads and foldables
Equational reasoning with lollipops‚ forks‚ cups‚ caps‚ snakes‚ and speedometers
The type constructors Cont, ContT, Yoneda, Codensity, and Ran
As a quick reminder of the usefulness of those obscurely-named constructs, a Cont computation can capture the current continuation, ContT is the monad transformer variant of Cont, Yoneda is useful for fmap fusion, Codensity computations can defer cleanup actions, and Ran computations can change the inner monad for the remainder of the computation.
Futamura Projections in Haskell
In particular, our constructions cannot be used to compose the List monad with itself.
An Abstract View of Programming Languages
This is a monad in the category of monads. Moggi discusses them in "An Abstract View of Programming Languages", including which transformers have joinT.
Applicative Bidirectional Programming tweet
What You Needa Know about Yoneda tweet tweet blog slides
Categories of Optics. twitter. reddit
coends as diagrams with holes
Relating idioms, arrows and monads from monoidal adjunctions continues the "Notions of computations as monoids" paper.
In case the reader is not familiar with them, coends might be (informally) seen as existential or Σ types.
Backward Induction for Repeated Games An use of the Select monad transformer.
Relational Algebra by Way of Adjunctions slides
Parametric polymorphism and operational improvement
A Meaning Explanation for HoTT
Exceptionally Monadic Error Handling. reddit.
Yoneda Intuition from Humble Beginnings. reddit.
UNIFIED NOTIONS OF GENERALISED MONADS AND APPLICATIVE FUNCTORS
string & wiring diagrams are fabulous for software and system design survey of diagrams for monoidal categories 7 sketches
Enriched Lawvere Theories for Operational Semantics.
Free monads of free monads. reddit.
Generalized Lens Categories via functors Cop→Cat
Profunctor optics, a categorical update. paper. Intro to Kaleidoscopes.
Unifying graded and parameterised monads. more.
Reason Isomorphically!. twitter.
Logic of computational semi-effects and categorical gluing for equivariant functors
Basic Bicategories. A Brief Introduction to Bicategories. bicategories and higher categories (data + axioms). A 2-categories companion.
A 1-cell a • f✲b • in a bicategory B is called an equivalence if there exists a 1-cell b • g✲a • such that g◦f ∼= 1a and f ◦g ∼= 1b
In a sense, coherence axioms are a price to be paid for the increased expressive power originated by weakening the defining structural properties. Think, for example, of the coherence diagram for associativity in definition §6. It identifies the basic ways in which the composition of 4 arrows can be parenthesised and relates them through a. To ensure that all such ways are unique is precisely the reason to enforce the commutativity of the diagram. By such a coherence axiom one knows that, in a bicategory, any two natural isomorphisms built out of a, r and l, by the composition and unit operations, actually coincide. That is to say, weakening has caused no special (calculational) damage.
This is the broader context of n-categories [Bae97], whose basic claim is that equations should hold on the nose (i.e., up to equality) only at the top level, i.e., between n-cells. . Therefore laws concerning k-cells, for k < n, should always be expressed as (k + 1)-equivalences. In this context an equivalence between (n − 1)-cells is an invertible n-cell whereas an equivalence between k-cells, for k < n, is just a (k + 1)-cell invertible up to equivalence.
The pentagon axiom is the ‘associahedron’ K4, whose vertices are each possible parenthesised word on four letters such that the letters appear in the same order, and edges are an application of associativity. Its commutativity asserts that there is no ambiguity between the two possible ways to transform an expression involving four horizontally composed 1-cells bracketed to the left to one bracketed to the right, while the triangle axiom asserts that there is no ambiguity between the two ways to collapse the unit if it appears in the middle of an expression involving horizontally composed 1-cells.
A category is called skeletal if it has no non-identity isomorphisms. With the axiom of choice, one can show that every small category is equivalent to its skeleton.
An enriched category is a category in which the hom-functors take their values not in Set, but in some other category V . The theory of enriched categories is now very well developed, and Cat-category theory is the special case where V = Cat. In Cat-category theory one deals with higher-dimensional versions of the usual notions of functor, limit, monad, and so on, without any “weakening”. The passage from category theory to Cat-category theory is well understood; unfortunately Catcategory theory is generally not what one wants to do — it is too strict, and fails to deal with the notions that arise in practice. In bicategory theory all of these notions are weakened. One never says that arrows are equal, only isomorphic, or even sometimes only that there is a comparison 2-cell between them. If one wishes to generalize a result about categories to bicategories, it is generally clear in principle what should be done, but the details can be technically very difficult.
Andrzej Filinksi’s master’s thesis, Declarative Continuations and Categorical Duality. pdf
Codensity and the ultrafilter monad
Homotopy type theory: the logic of space
lectures in the theory of Weighted Automata and Transducers 2 3 more
DIAGONAL ARGUMENTS AND CARTESIAN CLOSED CATEGORIES
A survey of constructive models of univalence tweet
proof theory, rules and meaning — an introduction
As you work with operations on structures, it may be necessary to coherently manipulate isomorphism (or more generally homomorphism) witnesses for various properties of these operations, e.g. associativity, commutativity and distributivity. A working mathematician, to use Mac Lane’s term, is well advised to be aware of the coherent witness-manipulation problem
the double category of open Petri nets
retrofitting purity with comonads
From Probability Monads to Commutative Effectuses
Just do It: Simple Monadic Equational Reasoning.
Understanding Idiomatic Traversals Backwards and Forwards. reddit
While this paper doesn't deal with "infinite" traversables, it gives a good intuition for a representation theorem for traversables in the finite case
Coends, graphically Coend Calculus and Open Diagrams
Category Theory as An Excuse to Learn Type Theory
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
Abstract Algebra Theory and Applications
Should I use a monad or a comonad?
Lecture notes on Category Theory concepts and Haskell GitHub repo
Program design by calculation reddit
The Rising Sea: Foundations of Algebraic Geometry
Do not be seduced by the lotus-eaters into infatuation with untethered abstraction
three different simultaneous generalizations, which can be interpreted as three large themes in mathematics
Practical foundations of mathematics (Fictive) story of a time where people reasonned only up to isomorphism
Seven Sketches in Compositionality: An Invitation to Applied Category Theory course
opetopes Opetope The category of opetopes and the category of opetopic sets opetopes as trees The calculus of opetopes - video
What is Applied Category Theory?
A Convenient Category for Higher-Order Probability Theory.
The Yoneda Lemma without category theory. tweet. Categories of Structures in Haskell.
Partial Functions and Recursion in Univalent Type Theory.
Composing Bidirectional Programs Monadically
Constructing Quotient Inductive-Inductive Types
WHAT IS ALGEBRAIC ABOUT ALGEBRAIC EFFECTS AND HANDLERS?
A categorical view of computational effects - Emily Riehl
Initial Algebras, Terminal Coalgebras, and the Theory of Fixed Points of Functors - draft
the nucleus of a profunctor At the Interface of Algebra and Statistics The nucleus: Mining concepts from adjunctions
Category Theory Foundations, Lecture 1
Categories and String Diagrams
Category theory for programmers by Bartosz Milewski
Categorification of Fourier Theory
choose Your Own Derivative reddit
They usually only make use of rudimentary mathematical tools that were already known in the XIXth century and miss completely the strength and depth of the constant evolution of our mathematical concepts and tools.
Monoidal Functors, Species and Hopf Algebras.
Extensibly Free Arrows - λC 2018 slides.
All of my company's business logic for our backend is written using arrows. I gave a talk at LC last year on it if you want to learn about the design pattern. "Extensibly free arrows"
selective applicative functors
Polynomial functors II: Seven wonders of the composition product
Emily Rieh - A Categorical View of Computational Effects slides
Universal algebra of higher kinded algebras. Monadicity.
Univalence from a computer science point-of-view. The synthetic theory of ∞-categories vs the synthetic theory of ∞-categories - Emily Riehl.
Memento - A natural transformation is an End (IV)
Combining Effects and Coeffects via Grading
internal lenses as functors and cofunctors
Initial Algebra as Directed Colimit
Synthetic topology in Homotopy Type Theory for probabilistic programming
Categorical Probability and Statistics: De Finetti's construction as a categorical limit
David Spivak: Mode-dependent dynamical systems and polynomial functors
the wiring pattern of the whole system is depending on state... operadic means that you can nest these guys
symmetric monoidal categories : a rosetta stone
Michael Shulman: Two-dimensional semantics of homotopy type theory
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
Building free arrows from components reddit
Profunctors, Arrows, & Static Analysis
Applicative Sorting original and a further improvement.
Category Theory, Syntactically
The Yoneda Lemma Without Category Theory
What is the advantage of monad transformers over monad coproducts?
The advantage that monad transformers has is that monad coproducts don't exist in general! Monad products always exist, but you can't define monad coproducts once and for all.
programming with universal properties link
Split epimorphisms and split monomorphisms - Annoying Precision
Monomorphisms and epimorphisms - Annoying Precision
Profunctor Optics: The Categorical View
CPS vs codensity vs reflection without remorse
Radix Sort, Trie Trees, And Maps From Representable Functors
A formalization of category theory in Coq
Closure Conversion as CoYoneda
Functor Oriented Programming reddit
Higher-order Abstract Syntax for Cartesian Closed Categories reddit
Counterexamples of Type Classes reddit
Monads are monoid objects for Compose, and applicatives are monoid objects for Day. So in Hask, I think we have a natural transformation Day f f ~> Compose f f which corresponds to ap essentially. This turns any Compose-monoid into a Day-monoid, but I'm not sure if this mapping can be expressed in any category, so maybe that's the issue there?
Also, Day convolution does not really work in a general CCC. Even in Set, Day convolution of arbitrary functors does not exist in general, but at least you can restrict yourself to accessible functors (which you can approximate in haskell as "strictly positive functors").
Also I don't know what you mean by saying day convolution doesn't work in general. Definitionally its just a kan extension making use of a category with suitable monoidal structure, which Set most certainly has!?
As for Day convolution, yes, it is a left Kan extension of something involving the monoidal structure, but that doesn't mean that it always exists, just like Kan extensions don't always exist. If you take the formula for a pointwise Kan extension as a coend, the domain of the coend is large (Set itself), so even though Set is cocomplete, you can't conclude that it exists.
On Day convolution I think see your point -- the coend formula works if you're in a sufficiently (co)complete setting, not universally.
Final Algebra Semantics is Observational Equivalence
Help with understanding monoid algebra
Computational Quadrinitarianism (Curious Correspondences go Cubical)
the slings and arrows of outrageous fortune Arrow is more than Strong and Category reddit
Kan Extensions III: As Ends and Coends
From free algebras to free monads
Lenses for philosophers reddit
Categories with Monadic Effects and State Machines
The Free Functor is Coyoneda, while the Cofree Functor is Yoneda.
from free algebras to free monads
Idempotence parametricity puzzle
Is the Yoneda Lemma only useful from a theoretical point of view?
toposes back in fashion?. The uses and abuses of the history of topos theory. Suitable introdcution?. Johnstone's book
The view that toposes originated as generalized set theory is a figment of set theoretically educated common sense. This false history obstructs understanding of category theory and especially of categorical foundations for mathematics.
needa know about Yoneda - video
Can skeleta simplify category theory?. Equivalence versus Isomorphism of Categories. What structure do natural isomorphisms preserve?
The first, and perhaps most important, point is that hardly any categories that occur in nature are skeletal. The axiom of choice implies that every category is equivalent to a skeletal one, but such a skeleton is usually artifical and non-canonical. Thus, even if using skeletal categories simplified category theory, it would not mean that the subtleties were artifical, but rather that the naturally occurring subtleties could be removed by an artificial construction (the skeleton).
Conway's Game Of Life Using Representable And Comonads performance the State comonad comonad to monad
In a much older post, I showed how to use the Co comonad-to-monad-transformer to convert Store s into State s, but this is a different beast, it is a monad directly on Store s.
Is there is a similar construction that lets you build a comonad out of a monad?
Sadly, it seems the answer in Haskell is no.
Surmounting the intuitionistic impossibility of this, then given any such adjunction, there would be a nice coend we could take, letting us sandwich any Monad in the middle as we did above.
Homotopy Type Theory and Higher Inductive Types
Free Monad and Free Applicative using single Free type reddit
They are related, but there are some coeffects there that I’m less sure about Implicits can be modeled with Env, and you can model custom coeffects with Cofree
Comonad Transformers in the Wild
Getting all the contexts of an arbitrarily-shaped Traversable container lazily so
the Plan applicative transformer
MonadFix and the Lazy and Strict State Monad reddit
Difference between free monads and fixpoints of functors? reddit
The deepness stops at another "coincidence" though. In Hask, the final object of F-coalgebras just happens to coincide with the initial object of F-algebgras. Is there deep reason for that coincidence?
I found prerequisites for the two fixed points to coincide including being an algebraically compact category (Theory and Practice of Fusion, section 3), maybe there is a deeper connection
scheduling effects. Part 4 of 4 of breadth-first traversals
Selective applicative functors reddit
What are the different approaches to formalizing type theory in the usual model-theoretic context?
Do you see the import here? The set of natural transformations hom could be m-a-s-s-i-v-e, a dense forest of unknowable, untamable, and frankly unhelpful weeds. "Except," the Yoneda lemma tells us, "it's not!" The only natural transformations that exist are those which can be cooked up from elements in the set obtained by evaluating F at the object of interest, X.
Category Theory in PL research
Basic laws of arithmetic, like a×(b+c) = a×b+a×c, are secretly laws of set theory. categorifying cardinal arithmetic HN
Backprop as Functor: A compositional perspective on supervised learning . reddit. neurocat.
finition 2.1 for a supervised learning algorithm is exactly the same as a lens.
Applied Category Theory Course: Collaborative Design
commutative monoids. tweet. talk. tweet.
Graphs are to categories as lists are to monoids.
Limits and Colimits Part 3 (Examples).
Applicative Bidirectional Programming and Automatic Differentiation. paper. reddit.
selective applicative functors
capability. van Laarhoven Free Monad.
Another solution to many of the same problems has been known for a while: free monads and extensible effects. As it happens, capability and free monads can be formally compared. In this paper, Mauro Jaskelioff and Russell O'Connor, prove that free monads are a special case of capabilities (it's not phrased in these terms, of course, but that's what the paper amounts to).
Swierstra notes that by summing together functors representing primitive I/O actions and taking the free monad of that sum, we can produce values use multiple I/O feature sets. Values defined on a subset of features can be lifted into the free monad generated by the sum. The equivalent process can be performed with the van Laarhoven free monad by taking the product of records of the primitive operations. Values defined on a subset of features can be lifted by composing the van Laarhoven free monad with suitable projection functions that pick out the requisite primitive operations. No doubt someone will develop a library implementing a type class(y) hierarchy to make this process transparent, which may or may not be a good idea.
the graphical calculus for Proarrow Equipments
Do monad transformers, generally speaking, arise out of adjunctions?
A concrete use for the right-adjoint of Day. eliminate a monad transformer stack in an Applicative style
Notes on Category Theory with examples from basic mathematics
adjunctions in the wild - foldl
blog post on weighted colimits, forshadowning the one on Freyd's adjoint functor theorem. Freyd's theorem
Eliminating Binders for Easier Operational Semantics
The free monoid on any set is finite lists over that set, and then the free group on that is… what? .
the nucleus of a profunctor. hyperfunctions.
Data.Functor.Contravariant.Rep.Representable
Applied Category Theory course intro Seven Sketches in Compositionality An Invitation to Applied Category Theory course book. new
Lecture 59 - Chapter 4: Cost-Enriched Profunctors (whole course)[https://forum.azimuthproject.org/categories/applied-category-theory-course]
Lecture 50 - Chapter 3: Left Kan Extensions
We'll create new databases from old using Kan extensions. You can see Fong and Spivak doing this in Section 3.4 of Seven Sketches, but I'll warn you that they don't say "Kan extension".
applied functional type theory
Applied Category Theory (@ MIT 2019)
Programming with categories - Lecture 0
squares: The double category of Hask functors and profunctors
Computing an integer using a Grothendieck topos. notes on toposes
High-assurance data integration with mathematical rigor
bicategory. A Survey of Definitions of (weak) n-Category
A monoidal category M may be regarded as a bicategory BM with a single object ∙. The objects A of M become 1-cells [A]:∙→∙ of BM; these are composed across the 0-cell ∙ using the definition [A]∘0[B]=[A⊗B], using the monoidal product ⊗ of M. The identity 1-cell ∙→∙ is [I], where I is the monoidal unit of M. The morphisms f:A→B become 2-cells [f]:[A]→[B] of BM. The associativity and unit constraints of the monoidal category M transfer straightforwardly to associativity and unit data of the bicategory BM. The construction is a special case of delooping (see there).
the natural number n denotes the maximal dimension of non-trivial cells in the model,
while the natural number r denotes the maximal dimension of the directed cells.
Up to equivalence [seems important!] you may assume that all equivalent pairs of j-morphisms for j>n are in fact equal, and many authorities include this as a requirement. On the other hand, you can also write down a definition of n-category from scratch (without passing through ∞-categories), and then this question never comes up. The point is that you don't talk about j-morphisms for j>n; you stop at n-morphisms.
So in an (∞,0)-category every morphism is an equivalence. Such ∞-categories are usually called ∞-groupoids.
This is directly analogous to how a 0-category is equivalent to a set, a (1,0)-category is equivalent to a groupoid, and so on. (In general, an (n,0)-category is equivalent to an n-groupoid.)
A 0-category (or (0,0)-category) is, up to equivalence, the same as a set (or class).
Remark 1.2. Interpreted literally, 0-category or (0,0)-category would be an ∞-category such that every j-cell for j>0 is an equivalence, and any two such j-cells that are parallel are equivalent. The picture that apparently emerges from this description might suggest a set equipped with an equivalence relation, or a what is sometimes called a setoid, or something even more complicated than that. One could thus say that a 0-category is a “setoid”, when considered just up to isomorphism. But it is more appropriate in higher category theory to consider these things up to equivalence rather than up to isomorphism [seems important!] when we do this, a 0-category is equivalent to a set again.
thin categories: up to isomorphism Vs up to equivalence
(It is really a question of whether you're working with strict categories, which are classified up to isomorphism, or categories as such, which are classified up to equivalence.)
Nonetheless, "unique up to unique isomorphism" is not a very useful notion. It just means the structure specified is unique up to isomorphism and has no non-trivial automorphism (in other words an isomorphism X→X has to be the identity homomorphism); if X had a non-trivial automorphism, then that automorphism would defeat the requirement of a unique isomorphism. Many properties used to specify structures up to isomorphism say nothing about the existence of automorphisms, so they will usually not specify anything up to unique isomorphism. What is very useful however is specifying something up to canonical automorphism: if X and Y are structures satisfying the specification, then there is an isomorphism X→Y, and in case there should be more than one such isomorphism, there is a way to single out one of them by a special property. In practice this special property is usually directly related to the specification that X,Y have to satisfy, and the existence of a canonical isomorphism an immediate consequence of it.
equivalence between two categories is a pair of functors between them which are inverse to each other up to natural isomorphism of functors (inverse functors).
This is like an isomorphism, but weakened [seems important!] such as to accomodate for the fact that the correct ambient context for categories is not iself a 1-category, but is the 2-category Cat of all categories. Hence abstractly an equivalence of categories is just the special case of an equivalence in a 2-category specialized to Cat.
We discuss some possible variants of the definition of equivalence of categories, each of which comes naturally from a different view of Cat.
The first, isomorphism, comes from viewing Cat as a mere 1-category; it is too strong and is really only of interest for strict categories. The next, strong equivalence, comes from viewing Cat as a strict 2-category; it is the most common definition given and is correct if and only if the axiom of choice holds. The next definition, weak equivalence, comes from viewing Cat as a model category; it is correct with or without choice and is about as simple to define as strong equivalence. The last, anaequivalence, comes from viewing Cat as a bicategory that is not (without the axiom of choice) equivalent (as a bicategory!) to the strict 2-category that defines strong equivalence; it is also always correct.
What does it mean for something to hold “up to isomorphism”?
up to. more. What does 'unique up to isomorphism' really mean?
"The property holds up to isomorphism" is a phrase which means "we might say an object has property , but that's an abuse of notation. When we say that, we really mean that there is an object isomorphic to which has property ". Essentially, it means "the property might not hold as stated, but if we replace the idea of equality by the idea of isomorphism, then the property holds".
A fundamental use of the concept of isomorphic functors is the usual definition of equivalent categories which involves functors isomorphic to identity functors.
More generally, one may think of a monoidal category as a bicategory with a single object (so that the monoidal product becomes horizontal composition) and this way regard enrichment in a monoidal category as the special case of enrichment in a bicategory . This is discussed in the section
Monoidal category. ncatlab. um.
A rather different application, of which monoidal categories can be considered an abstraction, is that of a system of data types closed under a type constructor that takes two types and builds an aggregate type; the types are the objects and {\displaystyle \otimes }\otimes is the aggregate constructor. The associativity up to isomorphism is then a way of expressing that different ways of aggregating the same data—such as {\displaystyle ((a,b),c)}{\displaystyle ((a,b),c)} and {\displaystyle (a,(b,c))}{\displaystyle (a,(b,c))}—store the same information even though the aggregate values need not be the same. Identity objects are analogous to algebraic operations addition (type sum) and multiplication (type product). For type product - identity object is the unit {\displaystyle ()}(), it trivially fully inhabits its type, so there is only one inhabitant of the type, and that is why a product with it is always isomorphic to the other operand. For type sum, the identity object is the void type, which stores no information and its inhabitants impossible to address. The concept of monoidal category does not presume that values of such aggregate types can be taken apart; on the contrary, it provides a framework that unifies classical and quantum information theory.[1]
Unfortunately, we’re not quite done with revising our definition yet. We’ll be taking our tensor products and identity objects and stringing them together to make new functors, and similarly we’ll be using these natural isomorphisms to relate these functors, but we need to make sure that the relationship doesn’t depend on how we build it from the basic natural isomorphisms. An example should help make this clearer.
What’s happened is we’ve replaced equations at the level of sets with (natural) isomorphisms at the level of the category, but these isomorphisms are now subject to new equations. We’ve seen two examples of these new equations, and it turns out that all the others follow from these two. I’ll defer the justification of this “coherence theorem” until later.
Poly is the category of polinomial functors and natural transformations between them.
selection functions are functorial in the category of lenses
who invented 'internalization'
associativity & multicategories
derived functor. just that you can make so many noncanonical choices and have it all piece together in the end.
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 an opaque/abstract data type to remove power from a monadic interface
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
Strongly Typed Term Representations in Coq
Finally, Safely-Extensible and Efficient Language-Integrated Query
A Self-Hosting Evaluator using HOAS
Breaking Through the Normalization Barrier: A Self-Interpreter for F-omega
Church and Curry: Combining Intrinsic and Extrinsic Typing
Church Encoding of Data Types Considered Harmful for Implementations linked from this interesting reddit discussion.
(P)HOAS and its ilk are a tool to simplify the representation of variable binders and the operation of term substitution. (bound, a great library, has an altogether different approach to solving this problem.) Phenomenally useful if variable binding and term substitution are important in your DSL - ie, your DSL looks something like lambda calculus - but quite useless for imperative languages where variables are declared and then written and read.
Tagless Staged Interpreters for Typed Languages
Abstracting Definitional Interpreters. video. tweet.
Sound and Reusable Components for Abstract Interpretation
Type Soundness Proofs with Definitional Interpreters
Engineering Definitional Interpreters
Tagging, Encoding, and Jones Optimality
The Structure and Performance of Efficient Interpreters apparently obsolete?
Compiling to categories "The general technique appears to provide a compelling alternative to deeply embedded domain-specific languages."
Type-safe observable sharing in Haskell
Observable Sharing for Functional Circuit Description
Stream Processing for Embedded Domain Specific Languages
Abstracting Definitional Interpreters github
Compositional Soundness Proofs of Abstract Interpreters
Collapsing Towers of Interpreters HN lobsters
Writing CEK-style interpreters (or semantics) in Haskell reddit
Functional EDSLs for Web Applications reddit
Haste, Selda
(Re-)Creating sharing in Agda’s GHC backend
Strongly Typed Term Representations in Coq
There are two approaches to formalizing the syntax of typed object languages in a proof assistant or programming language. The extrinsic approach is to first define a type that encodes untyped object expressions and then make a separate definition of typing judgements over the untyped terms. The intrinsic approach is to make a single definition that captures well-typed object expressions, so ill-typed expressions cannot even be expressed. Intrinsic encodings are attractive and naturally enforce the requirement that metalanguage operations on object expressions, such as substitution, respect object types. The price is that the metalanguage types of intrinsic encodings and operations involve non-trivial dependency, adding significant complexity. This paper describes intrinsic-style formalizations of both simply-typed and polymorphic languages, and basic syntactic operations thereon, in the Coq proof assistant. The Coq types encoding object-level variables (de Bruijn indices) and terms are indexed by both type and typing environment. One key construction is the boot-strapping of definitions and lemmas about the action of substitutions in terms of similar ones for a simpler notion of renamings. In the simply-typed case, this yields definitions that are free of any use of type equality coercions. In the polymorphic case, some substitution operations do still require type coercions, which we at least partially tame by uniform use of heterogeneous equality.
intrinsically-typed definitional interpreters for imperative languages
A definitional interpreter defines the semantics of an object language in terms of the (well-known) semantics of a host language, enabling understanding and validation of the semantics through execution. Combining a definitional interpreter with a separate type system requires a separate type safety proof. An alternative approach, at least for pure object languages, is to use a dependently-typed language to encode the object language type system in the definition of the abstract syntax. Using such intrinsically-typed abstract syntax definitions allows the host language type checker to verify automatically that the interpreter satisfies type safety. Does this approach scale to larger and more realistic object languages, and in particular to languages with mutable state and objects?
In this paper, we describe and demonstrate techniques and libraries in Agda that successfully scale up intrinsically-typed definitional interpreters to handle rich object languages with non-trivial binding structures and mutable state. While the resulting interpreters are certainly more complex than the simply-typed λ-calculus interpreter we start with, we claim that they still meet the goals of being concise, comprehensible, and executable, while guaranteeing type safety for more elaborate object languages.
Folding Domain−Specific Languages: Deep and Shallow Embeddings - Gibbons
Abstracting Definitional Interpreters
A Generic Abstract Syntax Model for Embedded Languages
But the real insight of this story is a replaying of an insight from Reynold's landmark paper, Definitional Interpreters for Higher-Order Programming Languages, in which he observes definitional interpreters enable the defined-language to inherit properties of the defining-language. We show the same holds true for definitional abstract interpreters. Remarkably, we observe that abstract definitional interpreters can inherit the so-called "pushdown control flow" property, wherein function calls and returns are precisely matched in the abstract semantics, simply by virtue of the function call mechanism of the defining-language.
Embedding F tweet gist type-level lambdas
This millennium has seen a great deal of research into embedded domain-specific languages. Primarily, such languages are simplytyped. Focusing on System F, we demonstrate how to embed polymorphic domain specific languages in Haskell and OCaml. We exploit recent language extensions including kind polymorphism and first-class modules
Lightweight Modular Staging: A Pragmatic Approach to Runtime Code Generation and Compiled DSLs Haskell example
Alchemy: A Language and Compiler for Homomorphic Encryption Made easY look at the appendix
The difficulty of using HOAS with effectful generators has long been recognized in the literature as a thorny problem,
Intrinsically-Typed Definitional Interpreters for Imperative Languages. Intrinsically Typed Definitional Interpreters: The Good, The Bad, and The Ugly. video.
Generic Monadic Constructs for Embedded Languages. Feldspar?
Lambda: the Ultimate Sublanguage. tweet
Scoping Monadic Relational Database Queries
From Definitional Interpreter to Symbolic Executor
Towards Secure IoT Programming in Haskell
Haski is designed after the synchronous programming language Lustre
our design does not require any modifications to GHC or the use of compiler plug-ins. Instead, Haski uses embedding techniques by leveraging advanced type-level features of GHC such as GADTs [Peyton Jones et al. 2006], data kinds [Yorgey et al. 2012], existential types, and pattern synonyms [Pickering et al. 2016].
Compilation as a Typed EDSL-to-EDSL Transformation
Combining deep and shallow embedding of domain-specific languages
Yet another explanation of intrinsic encoding
The parsing/typechecking problem for intrinsic encodings (?) and another take.
De-serialization and type-checking
Typed Tagless-Final Linear Lambda Calculus great resource! tagless final + HOAS (?)
Domain-specific Languages and Code Synthesis Using Haskell
Lessons learned building a toy compiler
A small (<500 LOC) programming language capable of proving theorems about its own terms
Backpack for initial and final encodings reddit
Duplicator Interpreter with HOAS
Writing A GraphQL DSL In Kotlin
It's well-known™ that this sort of 'intrinsically-typed' AST (where the AST is indexed by types/contexts) does not scale to dependently-typed object languages. As soon as your type contexts are telescopes instead of lists (i.e., types in the context can refer to other types in the context), you need induction-recursion and it gets unpleasant.
A completely valid point; I still think a indexed AST is preferred for correctness, particularly between phases. They definitely quite more time/dedication to complete though -- telescopes are much harder to deal with than lists.
Building a Friendly and Safe EDSL with IxState and TypeLits
Combining Deep and Shallow Embedding of Domain-Specific Languages. reddit.
Combining deep and shallow embeddings: a tutorial
Building Small Native Languages with Haskell
compiling a fifty year journey material
DSLs for non-programmers are a hoax. reddit. hn.
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
Building a language, in Haskell, with an LLVM backend
Philip Wadler on Reynolds’s ‘Definitional Interpreters for Higher-Order Programming Languages’
Creating an approachable Haskell-like DSL
Zeldspar - The Road to Epiphany
07 The Highs and Lows of Opimising DSLs
Statically Typed Interpreters - λC 2017 assets
An EDSL for KDB/Q: Rationale, Techniques and Lessons Learned
Ryan Newton - DSL Embedding in Haskell 1/2
Ryan Newton - DSL Embedding in Haskell 2/2
ICFP 2014: Folding Domain-Specific Languages: Deep and Shallow Embeddings - Jeremy Gibbons
UoY CS - Folding Domain-Specific Languages - Prof. Jeremy Gibbons
Stitch: The Sound Type-Indexed Type Checker reddit
Chris Laffra - Little Languages
Refunctionalization of Abstract Abstract Machines. paper.\
[Lorentz: Implementing Smart Contract eDSL in Haskell(https://www.reddit.com/r/haskell/comments/f098r7/lorentz_implementing_smart_contract_edsl_in/)
PaSe: An Extensible and Inspectable DSL for Micro-Animations
A DSL for fluorescence microscopy
A Generic Abstract Syntax Model for Embedded Languages (slides)
BinderAnn: Automated reification of source annotations for monadic EDSLs
Techniques for Implementation of Symbolically Interpretable Haskell EDSLs
strongly typed system F in ghc
On Adding Pattern Matching to Haskell-based Deeply Embedded Domain Specific Languages. reddit.
Choosing is Losing: How to combine the benefits of shallow and deep embeddings through reflection. tweet.
Data-reify for observable sharing
hnix is essentially a catamorphic lambda calculus interpreter. Using a functor fixed point to encode expression trees yields some very useful flexibility.
Finally tagless, partially evaluated
Finally, Safely-extensible and Efficient Language-integrated Query
De Bruijn-index, finally tagless
What makes partial evaluation of De Bruijn-indexed terms P repr h a so difficult is that their type includes the environment h with the types of the free variables that may occur in the term. The two key operations of partial evaluation, substitution for free variables and weakening, do change the environment h. (The type a of the embedded expression of course stays the same.) Furthermore, these operations have to adjust the De Bruijn indices in a complex way.
Effects Without Monads: Non-determinism -- Back to the Meta Language
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
Mutual Recursion in Final Encoding.
A very simple technique for making DSLs extensible
Simple lambda calculus DSL using GADTs in OCaml
Beam uses a finally tagless style which abstracts away the AST representation. The AST in the core module is used for testing. That’s it. The individual backends co opt the typeclasses in the core module to provide a custom representation.
Introduction to Tagless Final. Great article! reddit.
Final tagless encodings have little to do with typeclasses. more.
pragmatic object oriented tagless final
The Death of Final Tagless. Beautiful, Simple, Testable Functional Effects for Scala. tweet. zio thread. Interview. more zio. final tagless seen alive. not dead yet. tweet. tweet. stuff. laws.
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 and Their Optimization
Causal commutative arrows, revisited
Functional Reactive Programming, Refactored
There's a few of approaches to dealing with this that work together. Many of us hope to package them up into nicer abstractions now that we've started recognizing them. There are two very important ones to know. The first is to push dynamicity into the leaves of your data structure. Instead of rendering a Dynamic [a], you can work with a Dynamic [Dynamic a]. This let's you model changes to the leaves of the list separately from changes to the spine of the list. The nuclear weapon of this approach is traverseDMapWithKeyWithAdjust and the MonadAdjust class in general. It's quite rough in the currently unreleased Reflex 0.5 (which is what should be used since 0.4 is very old and doesn't have any lessons from industrial use incorporated).
The second major technique is to use patches instead of naive update Events. There is a variant of Dynamic called Incremental whose update value is a type that represents changes to the value the Incremental holds. You can write your own patch types and specify the value type they act on. Combined with the previous technique this lets you incrementally update the spine of a data structure instead of all at once. You can specify arbitrary changes which is less user friendly but more powerful.
Fault tolerant functional reactive programming
Fault Tolerant Functional Reactive Programming (Functional Pearl)
A Fitch-style Modal Calculus for Reactive Programming Without Space Leaks
Rhine: FRP with Type-Level Clocks
Modal FRP For All related to Rattus.
Reactive Probabilistic Programming
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
Haskell with Reactive Banana and GTK3
Does functional reactive programming in haskell scale well in GUI programs?
An introduction to reflex more
What is the current status of functional reactive programming (FRP) in Haskell?.
How can I best learn functional reactive programming?.
Your Easy Guide to Functional Reactive Programming
FRP in CodeWorld. reddit. Building and Debugging FRP with CodeWorld and Reflex
Instead of the state being the big deal, and components interact via shared state, the dependency graph becomes the big deal, and components interact by being passed their dependencies as arguments, and producing their results. That's made workable by correctly modeling the nature of these dependencies and results, and keeping state local .
reflex-vty: A library for building functional reactive terminal applications
FRP implementation details in Rust
the roots of frp nice diagrams hn objections
An IDE implemented using reflex
The Misunderstood Roots of FRP. Explicitly Comprehensible Functional Reactive Programming.
An efficient normalisation procedure for linear temporal logic
Rattus 0.1: An embedded FRP language with modal types.
What are different flavors of functional reactive programming?
you describe sequential circuits as functions operating over infinite streams, where memory/state is 'inferred' when you prepend an element in front of a stream: by doing that you move the present to the future, thus requiring memory.
basic propositional linear logic
Temporal logic and functional reactive programming
Functional Reactive Programming
Functional Reactive Programming in Java
Making Reactive Programs Function part2
Doug Beardsley: Real World Reflex
Do-It-Yourself Functional Reactive Programming
Sampling is pull
Purely Functional User Interfaces that Scale.
Principled Testing of Functional Reactive Systems
Synthesis of Functional Reactive Programs via a Reduction of Asynchronous Inputs to Lists
A Fresh Look at Linear Temporal Logic
alpaca-netcode: Rollback/replay NetCode for realtime, deterministic, multiplayer games
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.
Building a reactive calculator in Haskell (1/5) Reactive Web Apps in Haskell (all posts + live demo)
Rattus 0.1: An embedded FRP language with modal types
Explicitly Comprehensible Functional Reactive Programming. zulip.
One thing I encountered while playing with Specular (basically Reflex port to PS) is that you can code yourself into a corner if you don't push Dynamic s low enough, ending up not being able to avoid unnecessary updates
Reimplementing graphmod as a source plugin: graphmod-plugin reddit
Specifying how a plugin affects recompilation reddit
Comprehensive overview of using the Build System
hlint as a source plugin reddit
an index of different resources about GHC plugins
The Thoralf plugin: for your fancy type needs
write your own GHC typechecker plugins.
Type Theory Behind Glasgow Haskell Compiler Internals
Stage 1 does not support interactive execution (GHCi) and Template Haskell. The reason being that when running byte code we must dynamically link the packages, and only in stage 2 and later can we guarantee that the packages we dynamically link are compatible with those that GHC was built against (because they are the very same packages).
Contributing to GHC 2: Basic Hacking and Organization
So why did we need to build the compiler twice, wouldn’t the stage 1 compiler and the stage 1 package database have been enough? That’s a good question! We need to build the stage 2 compiler with the stage 1 compiler using the stage 1 package database (the one we will ship with the stage 2 compiler). As such, the compiler is built with the identical libraries that it ships with. When running / interpreting byte code, we need to dynamically link packages and this way we can guarantee that the packages we link are identical to the ones the compiler was built with. This it is also the reason why we don’t have GHCi or Template Haskell support in the stage 1 compiler.
Writing Custom Optimization Passes. faking fundeps
ghc hacking using Nix. another tweet.
Build GHC with stack and hadrian.
Writing efficient free variable traversals. reddit
"Eventful GHC" (debugging / profiling Haskell via the GHC eventlog)
Gazing into the Void: Understanding Space (Leaks)
https://ghc-compiler-notes.readthedocs.io/en/latest/
Embracing a mechanized formalization gap
In GHC, scopes are represented by VarSets. These VarSets are implemented by finite maps from uniques to Vars. Querying whether a variable is contained within this set is done by checking whether the unique of the variable is in the domain of the map. However, that query doesn’t ensure that the same variable is stored in the set, only one with the same unique. Thus, we require a stronger property: not only should the variable stored in the set have the same unique, but it should also be the “same” variable in the sense of almostEqual, shown below. In that way, all of the occurrences of that variable in the expression will be forced to have the same meta-information
Developing GHC for a Living. GHC dev.
I put together https://ghc.dev/, a cheatsheet to help anyone get started with contributing to GHC.
Simon Hafner- Up to Your Elbows in GHC- λC 2019
haskell / GHC symbol cheat sheet
GHC Dev getting started material
Write a GHC extension in 30 minutes by Richard Eisenberg
On "simple" constraints for typechecker plugins by Nicolas Frisby
Function Calls. whole-program specialization. effects for less - known vs unkown calls
A known call is a call of a function whose binding site is statically visible: The function is bound at top level in this module; or, The function is bound at top level in another module, and optimisation is on, so we can see the details (notably arity) of the function in the module's interface file; or, The function is bound by a let binding that encloses the call.
higher order functions make unknown calls (?)
Haskell to Core: Understanding Haskell Features Through Their Desugaring. post
What do ghc's FUN_1_0, FUN_0_1, etc closure types mean?
That's how the STG machine works, except thinnings can only appear at functions and thunks.
Creating new backends for GHC?
Introduction to Haskell execution and garbage collection internals
Debugging an assertion failure in GHC
The obvious point to connect to GHC codegen is STG, because Core is too restricted by its specific (and weak) type system, and Cmm is too low-level to be convenient. For example, Agda can compile to Haskell, but because the Haskell type system is weak in comparison, the code output is a horrid mess where almost everything is wrapped in unsafeCoerce, and this can be very poorly optimized by GHC. STG in contrast has a type system which only represents memory layouts and basic operational features, so it's a lot more flexible.
bracket has interrumptible cleanup
reworking of GHC's errors nice architectural choice to avoid cyclic dependencies
GHC activities report: December–January 2020/2021
Hacking on GHC - First Steps (2021)
Understanding Memory Usage with eventlog2html and ghc-debug
Cheney, Bisimulation and Coinduction for Dummies
Sangiorgi, An Introduction to Bisimulation and Coinduction
bunch of tweets about costuff https://twitter.com/DiazCarrete/status/1359097297834016773 https://twitter.com/DiazCarrete/status/775299151923974144 https://twitter.com/DiazCarrete/status/722587839444230146 https://twitter.com/DiazCarrete/status/904454953351163906 https://twitter.com/DiazCarrete/status/904007261521149952 https://twitter.com/DiazCarrete/status/1359098561376489472 https://twitter.com/DiazCarrete/status/1274268812855164928 https://twitter.com/DiazCarrete/status/1348956772820779011 https://twitter.com/DiazCarrete/status/1274268812855164928
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
Using Coq to Write Fast and Correct Haskell
Teach Yourself Logic 2017: A Study Guide HN
Corecursion and coinduction: what they are and how they relate to recursion and induction
Forms of recursion and induction What is the difference between total recursive and primitive recursive functions How does primitive recursion differ from “normal” recursion?
THE ESSENCE OF CODATA AND ITS IMPLEMENTATION
Copatterns Programming Infinite Structures by Observations. tweet
Mathematical Logic in Computer Science.
Setoids in type theory. Relationships between Constructive, Predicative and Classical Systems of Analysis. BISH. nlab.
In Praise of Sequence (Co-)Algebra.
The Power of Interoperability: Why Objects Are Inevitable. paper.
We argue that abstract datatypes — with public interfaces hiding private implementations — represent a form of codata rather than ordinary data
Explaining Non-Bisimilarity in a Coalgebraic Approach: Games and Distinguishing Formulas
Corecursion and coinduction: what they are and how they relate to recursion and induction. hn.
Flexible coinduction in Agda. reddit.
Classical (Co)Recursion: Programming
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.
Robert Harper on proofs by contradiction
Proof of negation and proof by contradiction
How is coinduction the dual of induction?
Natural deduction with Liquid Haskell
The Blind Spot and the cut rule
What is the easiest way to extend Morte to enable pattern-matching, induction and similar?
Something you may want to look at is Cedille/CDLE, which is (for the most part) CoC extended with dependent intersection types, implicit products, and a heterogeneous equality type. In it, you can get dependent eliminators, including induction. You can also prove parametricity and a few other interesting things.
The theory is barely more complicated than the CoC, it doesn't require termination or positivity checking, doesn't require an implementation of unification, etc.
Linear logic and deep learning video more more more
Suffice to day that Ehrhard and Regnier discovered something quite profound in differential lambda calculus, the implications of which are still being explored; this discovery should have significant bearing on what people refer to as differentiable programming, I think.
The third link above is the master’s thesis of my talented student James Clift. We have subsequently extended that work and are finishing a paper which explains the computational content of derivatives of Turing machines, according to differential linear logic. This might be of interest to people here. I will post a link when we put it online.
Pearlmutter and Siskind's basic idea is to use Reynolds defunctionalization transformation to turn higher-order programs into first-order programs, and then apply automatic differentiation to the resulting first-order program.
Classical Logic in Haskell. adventures in classical-land.
Induction-recursion. tweet. tweet.
induction-induction, induction-recursion. Induction-induction. What is induction-induction?.
Automatic Refunctionalization to a Language with Copattern Matching
Free is a kind of universal PL for unquotiented terms, Cofree for automata of a certain sort.
2017 04 28 - Andreas Lochbihler - Functional Programming and Proving in Isabelle/HOL
linear-base makes writing Linear Haskell easy and fun
@rae: Avoid losing money via -XLinearTypes
@rae: Connecting linearity and relevance in Dependent Haskell
Controlled Array Fusion using Linear Types. Josef Svenningsson (can't find the paper)
controlling fusion in haskell. Composable Efficient Array Computations Using Linear Types. Deforestation: transforming programs to eliminate trees.
linear types for circuit desing in clash
uniqueness types vs. linearity
Evaluating Linear Functions to Symmetric Monoidal Categories. programming without function (related video, but no linear types).
With linear types and the right notion of an arrow, we can build full intuitionistic linear logic
Deadlock-Free Session Types in Linear Haskell
A Brouwerian viewpoint on proof is that it is about transforming proofs into proofs, and then only later did folks start thinking about how to transform disproof.
A Fresh Look at Linear Temporal Logic
Extending Homotopy Type Theory with Linear Type Formers
types for programming and reasoning
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
On the Design of Distributed Programming Models "we show that concurrent programming models are necessary, but not sufficient, in the construction of large-scale distributed systems because of the problem of failure and network partitions: languages need to be able to capture and encode the tradeoffs between consistency and availability"
Initial algebra semantics is enough!
Polarized Data Parallel Data Flow avoiding explicit recurison, mentioned here
Empirical Study of the Anatomy of Modern Sat Solvers
Linkers - Ian Lance Taylor, Gold, A New ELF Linker
A Poor Man's Concurrency Monad. more.
Visualizing the Evolution of SAT Formula Structure in Solvers Why SAT solvers are practical
A Technique for Drawing Directed Graphs
Fast Deterministic Selection Selection Algorithm The related problem of k-highest elements
Algebraic Graphs with Class - A functional pearl
Fast and Loose Reasoning is Morally Correct
Calculating the Fundamental Group of the Circle in Homotopy Type Theory
Static Analysis of Programs using Semirings
A unified approach to solving seven programming problems (functional pearl)
Hygienic Source-Code Generation Using Functors
Somewhat Practical, Pretty Much Declarative Verifiable Computing in Haskell
Compiler Construction The Art of Niklaus Wirth
Batch Normalization (BN) is a milestone technique in the development of deep learning, enabling various networks to train.
The Algorithmic Foundations of Differential Privacy
The simple essence of automatic differentiation
Building a Bw-Tree Takes More Than Just Buzz Words
Formal Language Recognition with the Java Type Checker
Calculational Verification of Reactive Programs with Reactive Relations and Kleene Algebra
Semi-Indexing Semi-Structured Data in Tiny Space hw-json
What’s the Difference? Substracting bijections blog
On the Complexity and Performance of Parsing with Derivatives
a paper came out in 2016 that cleared up a number of the performance issues. So, most implementations (except Racket) are still terrible, but should “just” need to apply the findings from that newer paper to be fixed.
Invertible syntax descriptions: Unifying parsing and pretty printing.
From Fast Exponentiation to Square Matrices: An Adventure in Types
How to Architect a Query Compiler, Revisited links to related papers in HN video1 on collapsing towers of interpreters video2
Future Directions for Optimizing Compilers.
Partially-Static Data as Free Extension of Algebras.
Music as Language Putting Probabilistic Temporal Graph Grammars to Good Use
Coroutining Folds with Hyperfunctions tweet
everybody's got to be somewhere
On understanding data abstraction, revisited
one might arge encapsulation is somewhat overrated
Dependent Type Systems as Macros
Quantitative Information Flow with Monads in Haskell
Monad Transformers and Modular Algebraic Effects
Flipping Fold, Reformulating Reduction
Algebraic Property Graphs. video. reddit. Fast Left-Kan Extensions Using The Chase. Financial Reporting Data Warehousing with CQL.
seeking stability by being lazy and shallow
Ever wondered how fusion works?
Nested monadic loops may cause space leaks
A Comonad of Graph Decompositions
winterkoninkje's columbicubiculomania binary operations ring theory modal logic
Selda: a monadic database EDSL
Dynamic Programming exercises exercises lecture notes
A program that accepts exactly any desired finite set, in the right universe
[ANN: Prettyprinter 1.0 – ending the Wadler/Leijen zoo dilemma (https://pay.reddit.com/r/haskell/comments/6e62i5/ann_prettyprinter_10_ending_the_wadlerleijen_zoo/)
Getting introspection on a monadic computation by restricting what you can see of the result of earlier computations is basically the same approach Atze uses in his key monad and cage stuff here: http://people.seas.harvard.edu/~pbuiras/publications/KeyMonadHaskell2016.pdf There he embeds arrow computations into a monad simply by forbidding you to see the contents of the "cage" by the way it is encoded.
A (computational) linguistic farce in three acts hacker news
An Adversarial Review of “Adversarial Generation of Natural Language” more drama
word embeddings medium hackernews
Using free monads in a real-life large application?
The important thing is that mtl style is vastly more optimizable for GHC.
Whatever effect interpreter you would write for that effect type, you can implement a transformer that does the same thing for this class.
With mtl style, if you want to treat a class as an effect, and a transformer as an interpreter, then you end up needing n2 type class instances for n effects, if you want to have total coverage.
A typed expression quotation is written as [|| ... ||], or [e|| ... ||], where the ”...” is an expression; if the ”...” expression has type a, then the quotation has type Q (TExp a).
Values of type TExp a may be converted to values of type Exp using the function unType :: TExp a -> Exp.
Top-level declaration splices break up a source file into declaration groups. A declaration group is the group of declarations created by a top-level declaration splice, plus those following it, down to but not including the next top-level declaration splice. N.B. only top-level splices delimit declaration groups, not expression splices. The first declaration group in a module includes all top-level definitions down to but not including the first top-level declaration splice.
A typed expression splice is written
$$x, where x is an identifier, or $$ (...), where the ”...” is an arbitrary expression.
A typed expression splice can occur in place of an expression; the spliced expression must have type Q (TExp a)
A typed expression quotation is written as [|| ... ||], or [e|| ... ||], where the ”...” is an expression; if the ”...” expression has type a, then the quotation has type Q (TExp a).
Values of type TExp a may be converted to values of type Exp using the function unType :: TExp a -> Exp.
The problem with typed TH splice is that it doesn’t really make sense at the top-level and it should be treated as an implicit splice.
Typed Template Haskell is still not quite sound
Typed Template Haskell is quite similar to the lambda-circle calculus or MetaOCaml, but restricted to two levels.
Implementing Algebraic Effects in C
Notes on design of webscrapers in Haskell
In the second half of compilation, linguistic complexity falls.
Typically, the first drop is a desugaring phase which removes complex language features by transforming them into core language features.
OverlappingInstance workarounds Avoid overlapping instances with closed type families
Writing Performant Haskell (1 of 6): Intro
Abstract structure for substraction? torsors
15-251 Great Theoretical Ideas in Computer Science
Lessons I Wish I Had Learned Before Teaching Differential Equations Earlier thread Great explanation of integrating factors
Moshe Vardi on P versus NP SAT Solvers: Is SAT Hard or Easy? Theoretical explanations for practical success of SAT solvers?
It could also be that the use of SAT solvers is entirely spurious, driven by the availability of technology, rather than by an intrinsic need. Maybe the problems that need to be solved for verification purposes can be reduced to SAT, but it does not mean that they have to be reduced to SAT. The solvers may “work” exactly because they’re asked to solve problems that admit polynomial-time solutions, given a bit more ingenuity and effort. In fact, the claim that “practical instances” are easily solvable can be taken as evidence that the problems to be solved are not really SAT problems after all (ie, they don’t cover the space of SAT problems).
A type checker plugin for row types
Order theory for computer scientists
IMMUTABILITY AND UNBOXING IN ARRAY PROGRAMMING
Debugging C with Haskell's Divisible
- Contravariant generalizes Modus Tollens.
- Divisible generalizes Conjunction Introduction.
- Decidable generalizes Disjunction Elimination.
A Comparison of Four Algorithms Textbooks
Monoidal Parsing another video reddit
Computational Geometry: Set Operations on Polytopes reddit
Thoughts on "explicit passing" style as an alternative to MTL for managing effects?
Dynamic Programming: First Principles Dynamic Programming and the Calculus of Variations HN HN HN HN
One important takeaway is that dynamic programming in the Bellman formulation is a discrete analogue of Hamilton-Jacobi theory in how it writes down an equation for the optimal value as a function of a given endpoint rather than writing down an equation for the path as with the Euler-Lagrange equations. (You can reconstruct the path from the value function after the fact by gradient descent.) The relationship between Hamilton-Jacobi and Euler-Lagrange is the classical version of wave-particle duality. A concrete example in geometrical optics is the eikonal equation, a Hamilton-Jacobi type PDE, versus the geodesic equation, an Euler-Lagrange type ODE. Not coincidentally, one common numerical method for the eikonal equation called the fast marching method is a dynamic programming algorithm, very similar to Dijkstra's algorithm for shortest paths.
It should be mentioned that any "local" equation like a PDE or ODE cannot describe a globally optimal solution without strong assumptions such as convexity. In fact, satisfying the Euler-Lagrange equation isn't even sufficient for local optimality without further qualifications (Weierstrass conditions). But the Bellman dynamic programming equation, being recursive, can describe globally optimal solutions.
AlphaGo Zero - How and Why it Works HN
Everything you didn’t want to know about monad transformer state reddit
MonadTransTunnel, which allows transfer of transformer from one monad to another
Functional pearl: Nested Datacubes reddit
Session types in Cloud Haskell Session Types with Linearity in Haskell
LSEQ: an Adaptive Structure for Sequences in Distributed Collaborative Editing
deep learning & fp Deep Learning with Dynamic Computation Graphs Backprop as Functor: A compositional perspective on supervised learning
Hacking GHC's Stack for Fun and Profit
Why (and how) I wrote my own Entity Component System
Entities, now instead of being explicitly modeled by a GameObject are implicitly defined by an Int corresponding to their index in all of the arrays.
Modern Compiler Implementation in ML (Tiger Book) - Typechecker Question HaskTiger
The Handle Pattern / Object Oriented Programming in Haskell / Modularization of Algorithms on Complex Data Structures
About using existentials instead: "Hiding the state in the manner that you describe also hides it from "subclasses"; try to define the mkCounter/ticktock constructors and you'll see what I mean."
C++ core guidelines HN best way to learn c++
I strongly disagree with you. I think too few people use exceptions. They're great for making code more expressive, and it's only through exceptions that you can avoid two-phase initialization of classes and make constructors actually useful. It's only through exceptions that you can have meaningful copy-constructable resource-holding value types. Avoiding these constructs severely restricts the language. And for what? The arguments against exceptions appear to mostly arise from misunderstanding or some kind of weird aesthetic sense that I don't have.
Error codes also generally discard context and encourage a "just abort" mentality, especially with respect to memory exhaustion. That, or they become so general, mechanized, and macro-ized that they might as well be exceptions, but worse in almost every way.
GC-less Haskell: a trivial SDL2 demo
Lessons from Building Static Analysis Tools at Google HN
Authenticated data structures, generically paper HN
Evolutionary Generative Adversarial Networks GANs actor-critic Generative Adversarial Text to Image Synthesis
Breadth-First Traversals in Far Too Much Detail
What is the "correct" Haskell nix workflow? deploying Haskell to the cloud
Contributing to GHC 2: Basic Hacking and Organization
An Old Conjecture on Stream Transducers hn
Loading a Cabal module in the GHC API
Bit-manipulation operations for high-performance succinct data-structures and CSV parsing reddit
Forking and ContT ContT, withLifted and resetContIO
Programming Z3 nice tutorial.
Scrap Your Boilerplate with Object Algebras. original. Who's Afraid of Object Algebras?.
A naive—and wrong—way to shuffle a list is to assign each element in the list a random number, and then sort it. It might not be immediately obvious why
Applicative Regular Expressions using the Free Alternative. Parsing context-sensitive languages with Applicative. Free Monad and Free Applicative using single Free type. slides
Syntax-Guided Rewrite Rule Enumeration for SMT Solvers.
Generating Good Generators for Inductive Relations. What is the best practice to generate data which satisfy specific property in QuickCheck?
LoCal: A Language for Programs Operating on Serialized Data. reddit. hn.
The Best Refactoring You’ve Never Heard Of
Practical deforestation for fixed-point structures -- introducing tungsten
Faster Coroutine Pipelines Faster Coroutine Pipelines - a reconstruction. so question.
the decidability of EPR (a fragment of first-order logic)
a new metalanguage for theorem provers
Does this newtype exist in some library?
Ever wondered how fusion works?.
Computational semantics course
In the second lecture, we look at the extension of dynamic predicate logic to type theory. This gives rise to a system that is very much like modern compositional versions of discourse representation theory. We present an implementation and comment on its failings.
A Purely Functional Typed Approach to Trainable Models (Part 1) reddit
It is essentially the same as the wengert mode implementation, except it works heterogeneously. the ad library only works if your input, intermediate and output values all have the same type.
Contributing to GHC 4: Real Issues
A Monadic Framework for Delimited Continuations.
term rewriting combinators in Haskell
Entity Component Systems & Data Oriented Design slides. hn
What’s the Difference? video and slides.
What is AABB - Collision detection?
implicit corecursive queues. Difference Lists, Applicatives, And Codensity. From monoids to near-semirings: the essence of MonadPlus and Alternative
Proof of negation and proof by contradiction se. tweet.
Recovering Purity with Comonads and Capabilities tweet
why ML-like module systems are powerful. lists of papers about modules systems
mathematics for computer science on hn
algorithms lecture notes and assignments CSCI-280
Programmin in Z3. SMT by example.
Syntactic metaprogramming I in meta-cedille. reddit.
automatic differentiation for dummies
A Functional Reboot for Deep Learning
coroutining folds with hyperfunctions
Harper’s Regular-Expression Matcher in Cedille
Seeking Stability by being Lazy and Shallow
MIT 6.046J Design and Analysis of Algorithms, Spring 2015
Advanced Algorithms (COMPSCI 224), Lecture 1
APLicative Programming with Naperian Functors
CS50 2017 - Lecture 7 - Dynamic Programming
Differential Topology | Lecture 1 by John W. Milnor
MIT Calculus Revisited: Single Variable Calculus
MIT Calculus Revisited: Multivariable Calculus
MIT Calculus Revisited: Complex Variable Calculus
MIT 18.01 Single Variable Calculus
Fast and Parallel State Machines Data-Parallel Finite-State Machines paper
Efficiently coding for modern CPUs
MuniHac 2018 Keynote: Beautiful Template Haskell
Generative Art. Day!
Haskell SDL2 on Windows. more.
automatic differentiation for dummies
MuniHac 2019: The many faces of isOrderedTree
a functional reboot for deep learning
Parser Parser Combinators for Program Transformation
Good design and type safety in Yahtzee
Stacked Borrows - An Aliasing Model for Rust
Technical Talk: Michele Pagani on automatic differentiation
10-part series on breadth-first traversals
The Dawn of Computational Complexity Theory
Functions of type A → B can be translated into corresponding functions of type ¬B → ¬A in continuation-passng style (CPS), where ¬A is logically negation but computationally a continuation from A.
This widens the view of functions as value transformers, taking values of type A to values of type B, to include an alternative perspective of them as continuation transformers
using graded coeffects to work with multiple versions of a package within a single program
List of linguistics open courses at MIT. tweet.
CS224U: Natural Language Understanding. tweet. plan.
Grammatical Framework: Formalizing the Grammars of the World spotted at HN
The GF model of translation: application and resource grammars
Aarne Ranta: Automatic Translation for Consumers and Producers
Fantastic Features We Don't Have In The English Language reddit
The Ling Space. Lambda calculus. Type theory.
Intuition & Use-Cases of Embeddings in NLP
Modern NLP for Pre-Modern Practitioners
Genie: A Generator of Natural Language Semantic Parsers for Virtual Assistant Commands
Of Lambdas and Linguists Montague Semantics. slides handout
Grammatical Framework: Programming with Multilingual Grammars lobsters
Computational Semantics with Functional Programming
Combinatorial Species and Tree-Like Structures
The Vauquois triangle (Vauquois, 1968)
Developing a Stemmer for German Based on a Comparative Analysis of Publicly Available Stemmers
books read to make a gaming engine
Getting started in Natural Language Processing (NLP)
Multitask Question Answering Network (MQAN)
NLP's ImageNet moment has arrived hn
NLP's generalization problem, and how researchers are tackling it
The State of Transfer Learning in NLP
As an NLP person who had to work on some object detection stuff recently for an unrelated matter, it's amazing what a difference transfer learning makes. Whole task becomes brainless.
What problem does BERT hope to solve for search?
tracing bidirectional type checking
DisCoCat and language change. tweet.
http://aclweb.org/anthology/C82-1022 https://pdfs.semanticscholar.org/0b5d/ab9d1718d6ca0c7211c0d81c9a65e4a03759.pdf https://m.tau.ac.il/~landman/files/advanced-semantics/6%20Montague%20Grammar%20and%20Type%20Shifting.pdf https://www.researchgate.net/publication/228525117_Compositionality_in_Montague_Grammar https://plato.stanford.edu/entries/montague-semantics/ https://web.stanford.edu/~cgpotts/talks/potts-symsys100-2012-04-26-montague.pdf http://people.umass.edu/scable/LING720-FA13/Handouts/Partee-Presentation.pdf https://www.persee.fr/doc/hel_0750-8069_1983_num_5_2_1164 http://www.u.tsukuba.ac.jp/~kubota.yusuke.fn/lsa/bach79.pdf https://idus.us.es/xmlui/bitstream/handle/11441/50570/MONTAGUE%20GRAMMAR%2C%20CATEGORIES.pdf?sequence=1&isAllowed=y MONTAGUE GRAMMAR, CATEGORIES AND TYPES: A PRESENTATION OF ACTUAL THEORIES IN SEMANTICS AND DISCOURSE INTERPRETATION From Montague Grammar to Database Semantics http://lagrammar.net/papers/fmg2dbs-li.pdf https://pdfs.semanticscholar.org/0b5d/ab9d1718d6ca0c7211c0d81c9a65e4a03759.pdf
DBS was designed to answer the central theoretical question for building a talking robot
Given the opportunity to use the computers at CSLI Stanford (1984-86), we attempted to computationally verify the SCG fragment of English with an implementation in Lisp. This seemed possible for the following reasons
Montague Grammar has inspired several generations of formal semanticists. It has paved the way to a precise formulation of semantic problems and solutions. Montague has shown that it is possible to do highly rigorous work and yet make substantial progress at the same time. What it certainly is not, however, is the last word on matters. Especially when it comes to compositionality there is no consensus whether Montague has supplied a fully compositional approach. This has nothing to do with a lack of precision; it has more to do with the question whether the abstract formulation is a good rendering of our initial intuitions. In many ways, Montague looks more like a technician than a theoretician; he prefers something that works over something that has intrinsic virtues. Forty years on, the ideas have been substantially modified. We seem to have a much more profound notion of what is a compositional semantics.
https://pdfs.semanticscholar.org/0b5d/ab9d1718d6ca0c7211c0d81c9a65e4a03759.pdf
But, despite of the importance of the role played by the logical grammars in the “semantic controversies” during the decade 1955-1965, they didn’t influence substantially in the later developments, fundamentally in those that were carried out in the generative frame. It is in this sense in which it is necessary to interpret Gerald Gazdar’s and Geoffrey Pullum’s following statement:
“Categorial grammars [...] have always had a somewhat marginal status in linguistics. There has always been someone ready to champion them, but never enough people actually using them to turn them into a paradigm. The currency they have [...] is due in large measure to Montague, who based his semantic work on a modified categorial grammar”
https://en.wikipedia.org/wiki/Categorial_grammar
https://en.wikipedia.org/wiki/Dependency_grammar#Dependency_vs._constituency
From Logic to Montague Grammar: Some Formal and Conceptual Foundations of Semantic Theory Course Handouts and Problem Sets Seth Cable University of Massachusetts Amherst January 13, 2014
http://ling.auf.net/lingbuzz/001989/current.pdf
http://www.coli.uni-saarland.de/courses/underspecification-06/slides/01-mg.pdf
Unfortunately, however, the SCG fragment turned out to be seriously unsuitable for a computational implementation.
Cooper Storage and Type-Level Haskell. CONTINUATIONS AND THE NATURE OF QUANTIFICATION. The Cooper Storage Idiom. CS224U Introduction to semantic parsing. The Shrdlite project in Typescript.
From Frequency to Meaning: Vector Space Models of Semantics.
Linguistics Using Category Theory (distributional semantics). hn
Types in Natural Language. tweet
In Stockholm, when I first discussed the project with Per Martin-Löf, he said that he had designed type theory for mathematics, and than natural language is something else. I said that similar work had been done within predicate calculus, which is just a part of type theory, to which he replied that he found it equally problematic. But his general attitude was far from discouraging: it was more that he was so serious about natural language and saw the problems of my enterprise more clearly than I, who had already assumed the point of view of logical semantics. His criticism was penetrating but patient, and he was generous in telling me about his own ideas. So we gradually developed a view that satisfied both of us, that formal grammar begins with what is well understood formally, and then tries to see how this formal structure is manifested in natural language, instead of starting with natural language in all it unlimitedness and trying to force it into some given formalism.
You could even encode generic conjugation forms and the generate the combinatorial species for each.
Abstracting definitional interpreters
First, the interpreter is written in an open recursive style; the evaluator does not call itself recursively, instead it takes as an argument a function ev—shadowing the name of the function ev being defined—and ev (the argument) is called instead of self-recursion. This is a standard encoding for recursive functions in a setting without recursive binding. It is up to an external function, such as the Y-combinator, to close the recursive loop. This open recursive form is crucial because it allows intercepting recursive calls to perform “deep” instrumentation of the interpreter
Program reduction: a win for recursion schemes reddit
Backpack for initial and final encodings
We’re going to use open recursion and a dash of laziness to write our evaluator.
Explicit memoization can be elegant; a response to "DP in Haskell"
compositional zooming. reddit.
We present a novel but remarkably simple formulation of formal language grammars in Haskell as functions mapping a record of production parsers to itself
Hyperfunctions. hypertypes. hyperfunctions as games. tweet. Algebras for Weighted Search. Hyperfunctions have sort of stacklike behavior.
On the other hand, BFS player 1's behavior looks extremely complex, and involves dreaming up some entirely new hypothetical other player, and thinking about what that other player would have done, as well.
Functional Pearl: The Decorator Pattern in Haskell
An arity-generic decorator needs to solve two problems: intercept recursive calls and handle functions of any arity uniformly
a well-typed call-tracing decorator
Robert Harper's Homotopy type theory course at CMU
Computational (Higher) Type Theory tutorial - POPL 2018 slides
15-816 Linear Logic at CMU reddit reddit2
15-816 Substructural Logics at CMU
Lecturas del Grupo de Lógica Computacional
6.851: Advanced Data Structures (Fall'17)
Programming Language Theory in Agda
Robert Harper - Computational Type Theory
Simon Peyton Jones - Compiling without continuations
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
OPLSS 2018 - Algebraic Effects and Handlers - Andrej Bauer
Capturing the Future by Replaying the Past
Actually the authors of this paper show that mutable state + exceptions is all that is required to implement delimited continuations (except in C, read the paper for the details). There is a performance hit if we compare their implementation with a direct support from languages which support delimited continuations but this is not that bad.
Versatile Event Correlation with Algebraic Effects
The paper shows that with a limited set of effects, like push but also trigger to trigger the materialization of a tuple or get/set to temporarily store events, we can reproduce most of the behaviours exposed by so-called “complex event processing” (CEP) libraries: windowing, linear/affine consumption, zipping, and so on.
Relational Algebra by Way of Adjunctions
https://popl19.sigplan.org/track/POPL-2019-Research-Papers#event-overview
write yourself a typed functional language.
at 30:30 interesting dependent programming trick
at 39:30, thoughts about the particularities of dependent types in #haskell
Proceedings of the ACM on Programming Languages Volume 3 Issue ICFP, August 2019
Twice per year, JFP publishes the abstracts of recently completed PhD theses in the area of functional programming. Type-Safe Generic Differencing of Mutually Recursive Families.
the list of accepted papers for ICFP '21.
list of lectures. RH talks about laziness in some of them.
formal reasoning about programs 2018
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
type inference in stack based languages
[recursion continuation trampolines](On Recursion, Continuations and Trampolines)
What are the differences between logical relations and simulations?
Hackett - type systems as macros
Search-based compiler code generation
A Tutorial on Implementing Higher-Order Unification in Haskell Follow-up
What are the differences between logical relations and simulations?
Logical Frameworks and Meta-Languages: Theory and Practice
Workshop on Homotopy Type Theory/ Univalent Foundations
Resources for writing a type checker? mpre
Algorithmically Scrapping Your Typeclasses
infer is implemented as a catamorphism, which generates a fresh type variable for every node in the expression tree, looks up free variables in the SymTable and attempts to unify as it goes.
Is there any reason to compile pure lambda calculus with CPS?
The alternative to cps from the "compiling without continuous" paper is "administrative normal form". There's an explication in the paper "the essence of continuations passing style", but the paper is pretty dense.
Appel’s CPS implementation for ML is all the things he mentions: It’s rather large, it’s quite rigid, and it’s a pain to debug. An answer to this is Join Points, another is a Sea of Nodes. There, let-floating is a function of the scheduler and subsequent dead argument elimination passes. Additionally, the graph is naturally scheduled in data-dependence order but that is strictly not a requirement.
A Graph-Based Higher-Order Intermediate Representation (Sea of nodes)
The Left Hand of Equals HN pdf
An Adequacy Theorem for Dependent Type Theory
Old neglected theorems are still theorems HN tweet idris forum
the abstract algorithm more Optimality and inefficiency: what isn't a cost model of the lambda calculus?
Unfortunately, the bookkeeping to maintain the redex sharing takes exponential time
how to implement system F-omega?
It is indeed quite common during compilation to repeatedly traverse an AST doing operations only on some of its nodes (distinguished by a type or a particular data constructor). That's why compiler construction has been not only the biggest consumer for generic programming libraries but also a notable producer.
Why I no longer believe in computational classical type theory. A formulae-as-type notion of control. reddit.
Survey on Bidirectional Typechecking
What constitutes denotational semantics? Denotational semantics. tweet.
In a parallel (concurrent) language, it is possible to short-circuit both sides: they are evaluated in parallel, and if one terminates with value true, the other is interrupted. This operator is thus called the parallel or.
The problem of full abstraction for the sequential programming language PCF was, for a long time, a big open question in denotational semantics. The difficulty with PCF is that it is a very sequential language. For example, there is no way to define the parallel-or function in PCF. It is for this reason that the approach using domains, as introduced above, yields a denotational semantics that is not fully abstract.
However, compositional semantic definitions have been losing their edge over the years. Robin Milner and Andy Pitts have developed a number of "operational reasoning" techniques, which work purely on the syntax but using the operational semantics wherever needed for talking about behaviour. These operational reasoning techniques are low-tech. No fancy mathematics. No infinite objects. We can teach them to undergraduates and anybody can use them. So, many people ask the question why we need denotational semantics at all.
Operational approaches also score brilliantly when the programming languages get very fancy, with all kinds of loopy higher-order types. We may have no idea how to model such things mathematically. Or, the standard mathematical models might turn out to be inconsistent under the stress of loopiness. (For example, see "Polymorphism is not set-theoretic" by Reynolds.) Operational approaches that work purely on syntax can neatly side step all these mathematical problems.
Another word about "operational semantics". In the early days, the term "operational" was used to refer to any semantic definition that referred to detailed evaluation steps. Both denotational semanticists and axiomatic proponents looked down upon "operational" semantics, regarding it as being low-level and machine-oriented. I think this was really based on their belief that higher level descriptions were possible. These beliefs were shattered as soon as they considered concurrency.
Here we see the authors struggling with the two notions of "operational", one the technical notion - behaviour expressed using syntactic manipulations, and the other, the conceptual notion - being low-level and detailed. The credit largely goes to Plotkin and Milner for rehabilitating "operational" semantics, making it as high-level as possible and showing that it could be elegant and insightful.
Despite all this, the operational notion of process is still quite different from the denotational notion of process, the latter of which was developed by both de Bakker and Hoare and their teams. And, I think there is a lot that is mysterious and beautiful about the denotational process concept which is still to be understood.
Don’t Think, Just Defunctionalize.
elaborate Reddit comment about evaluation strategies induction laziness and other stuff
Linear types can change the world
Polarized Data Parallel Data Flow from
About the efficient reduction of lambda terms
OutsideIn(X) Modular type inference with local assumptions reddit
LCF considered as a programming language
reddit comment mentioning On the unity of duality and Least and Greatest Fixed Points in Linear Logic.
Type systems for programming languages
Light Affine Lambda Calculus and Polynomial Time Strong Normalization
Linear types and non-size-increasing polynomial time computation
A Syntactical Analysis of Non-Size-Increasing Polynomial Time Computation
Higher Inductive Types in Programming
On Understanding Types,Data Abstraction, and Polymorphism
Practical type inference for arbitrary-rank types also unification-fd and typing haskell in slightly more modern haskell and this tweet
Logic Programming and Type Inference with the Calculus of Constructions - Matthew Mirman
Logical Bisimulations and functional languages?
A Logical Relation for Monadic Encapsulation of State
Incremental Parametric Syntax for Multi-Language Transformation
Sound and Complete Bidirectional Typechecking for Higher-Rank Polymorphism with Existentials and Indexed Types reddit
The Calculus of Dependent Lambda Eliminations so
Lambda encodings were abandoned as a basis for constructive type theory almost thirty years ago
Induction principles are not derivable for lambda encodings (Geuvers, 2001)
Induction Is Not Derivable in Second Order Dependent Type Theory reddit
We give counter-models in which the induction principle over natural numbers is not valid.
Compiling with Continuations, Continued
The essence of compiling with continuations
Compiling without continuations
The case-of-case transformation, including the idea of using let bindings to avoid duplication, is very old
Declarative semantics for functional languages: compositional, extensional, and elementary reddit
An Introduction to Logical Relations
Complete and Easy Bidirectional Typechecking for Higher-Rank Polymorphism apparently v good slides
A Short Introduction to Systems F and Fω
Practical type inference for arbitrary-rank types
Boxy type inference for higher-rank types and impredicativity watch out, impredicativity!
Formalized Unification Algorithms
Overlapping and Order-Independent Patterns
Compilation as a Typed EDSL-to-EDSL Transformation reddit
Stitch: The Sound Type-Indexed Type Checker
all this shifting can slow the interpreter down. A variable shift requires a full traversal and rebuild of the AST, costing precious time and allocations. Though I have not done it in my implementation, it would be possible to add a Shift constructor to the AST type to allow these shifts to be lazily evaluated; the design and implementation of other opportunities for optimization is left as future work.
How to Architect a Query Compiler pdf
Abstract Interpretation, Logical Relations, and Kan Extensions
TLA+ in Practice and Theory Part 4: Order in TLA+
Galois connections serve as the basis for abstract interpretation, a central concept in the theory of program analysis, developed by Patrick and Radhia Cousot in the 1970s. In TLA terms, abstract interpretation is a process by which the more abstract specification, G , is automatically generated from the more concrete one, F. Abstract interpretation places different kinds of programs semantics on a spectrum of abstraction, from behaviors to functional denotational semantics. Many ideas in program analysis, including type checking, model checking and deductive proofs can all be viewed as forms of abstract interpretation. In TLA+ this idea is made explicit and formally manipulable, though less general.
Logical Full Abstraction and PCF
Definability and Full Abstraction
Abstract Interpretation - a semantics-based tool for program analysis
Traits: Composable Units of Behaviour
Literature Review of GHC Core reddit
10 papers that all PhD students in programming languages ought to know, for some value of 10
Light Affine Set Theory: A Naive Set Theory of Polynomial Time twitter
Elaborating Dependent (Co)pattern Matching
A Metalanguage for Guarded Iteration
Coherent Explicit Dictionary Application for Haskell: Formalisation and Coherence Proof
Partially-Static Data as Free Extension of Algebras
From algebra to abstract machine: a verified generic construction
Connot McBride on total languages - Turing-Completeness Totally Free Datatypes of Datatypes tweet tweet tweet tweet tweet hasochistic containers event
When we put that "Delay" in the type, or write a fuel-driven approximant, we're often accused of somehow cheating, but we're only telling the truth: we can't show this is finite but we can run it as long as you want.
basics of bidirectionalism lobsters. a quick look at impredicativity. video
Freer monads, more extensible effects video. Free and Freer Monads: Putting Monads Back into Closet. slides. What is your opinion on Eff vs. mtl-style design?. How do I compose 'freer' effects in haskell?. One Monad to Prove Them All. see also the algebraic effects and handlers videos from OPLSS 2018.
Writing Monad (and now, Applicative and Functor) instances and making sure the monad laws hold are a big part of defining a monad and even a bigger part in exponentially procreating monad tutorials. We argue that all these instances are boilerplate -- avoidable boilerplate. Perhaps because of the Latin-sounding names and the evocation of the highest Math, the petty boilerplate, trivial laws, plain old plumbing have usurped an extraordinary amount of attention. Wouldn't it be refreshing if we could directly think on what an effect does rather than on how the plumbing works.
The Calculus of Dependent Lambda Eliminations
Modern constructive type theory is based on pure dependently typed lambda calculus, augmented with user-defined datatypes. This paper presents an alternative called the Calculus of Dependent Lambda Eliminations, based on pure lambda encodings with no auxiliary datatype system.
Lambda encodings were abandoned as a basis for constructive type theory almost thirty years ago, due to the following problems
Univalent Foundations and the UniMath Library
the idea of higher inductive types being that unlike ordinary inductive types we allow in their definitions not only constructors that generate elements of the type being defined, but also constructors that generate paths (i.e. elements of identity types) or even higher homotopies.
Theory and practice of demand analysis in Haskell.
cubical Agda. On Higher Inductive Types in Cubical Type Theory.
A Verified Compiler for a Linear Imperative/Functional Intermediate Language
Signatures and Induction Principles for Higher Inductive-Inductive Types.
Stochastic Lambda Calculus and Monads of Probability Distributions
A Probabilistic Language based upon Sampling Functions
Effect Handlers via Generalised Continuations.
Definitional Proof-Irrelevance without K. video.
Definitional equality—or conversion—for a type theory with a decidable type checking is the simplest tool to prove that two objects are the same, letting the system decide just using computation. Therefore, the more things are equal by conversion, the simpler it is to use a language based on type theory.
Infinite Types, Infinite Data, Infinite Interaction.
From Parametricity to Conservation Laws, via Noether's Theorem
Higher-order Type-level Programming in Haskell.
Partial Type Constructors (extended version).
System Fω and Parameterization. reddit.
Symbolic Execution is a case of Abstract Interpretation?. HN. Meta-circular Abstract Interpretation in Prolog.
Call-By-Need is Clairvoyant Call-By-Value.
Quantitative Program Reasoning with Graded Modal Types. Granule.
Recovering Purity with Comonads and Capabilities
Julia’s Efficient Algorithm for Subtyping Unions and Covariant Tuples
A Predicate Transformer Semantics for Effects
Checking Dependent Types with ormalization by Evaluation: A Tutorial (Haskell Version). tweet.
A tiny implementation of GHC's OutsideIn(X) algorithm.
A Modular Inference of Linear Types for Multiplicity-Annotated Arrows
runners in action. post. repo. Interacting with external resources using runners (aka comodels)
We shall address these kinds of issues indirectly (!), by not introducing a linear typing discipline‚ but instead we make it convenient to hide external resources
Dependently typed lambda calculus with a lifting operator. tweet.
Defunctionalization: Everybody Does It, Nobody Talks About It. Defunctionalisation: An underappreciated tool for writing good software. hn.
on recursion continuations and trampolines
LoCal: A Language for Programs Operating on Serialized Data
Generalized Monoidal Effects And Handlers
Elaborating dependent (co)pattern matching
Programming Languages as Objects in Nature. tweet. The Next 700 Semantics
Lambda encodings were abandoned as a basis for constructive type theory almost thirty years ago, due to the following problems. Induction Is Not Derivable in Second Order Dependent Type Theory. Something is lost when we encode data or codata impredicatively. Lambda is not the Ultimate.. in type theory this definition of the recursion scheme suffers from same inefficiency as plagues the predecessor for Church-encoded naturals
tweets about Facet https://twitter.com/rob_rix/status/1320544724864872453 https://twitter.com/rob_rix/status/1318518708059492353 telescopes https://twitter.com/rob_rix/status/1320381469769011202 https://twitter.com/rob_rix/status/1320695095268675584
Dijkstra Monads Forever: Termination-Sensitive Specifications for Interaction Trees
We model such programs using interaction trees, a coinductive datatype for representing programs with algebraic effects
A graded dependent type system with a usage-aware semantics . video.
Design and Implementation of Effect Handlers for Object-Oriented Programming Languages
Our design employs explicit capability-passing style. That is, instead of dynamically searching for a handler at runtime, we pass instances of handlers as additional arguments to methods.
Handling Local State with Global State
Programming, Logic and Semantics Lab. tweet.
closure conversion is safe for space
Cheap interpreter, part 7: register machines
Functional programming languages Part I: interpreters and operational semantics whole
CS-XXX: Graduate Programming Languages Lecture 14 — Efficient Lambda Interpreters
A biased history of equality in type theory
write yourself a typed functional language. slides. examples. pi.
https://arxiv.org/pdf/1905.13706v1.pdf
Cubical Syntax for Extensional Equality
On bidirectional type checking. tweet. video. notes.
I love bidirectional, but it's not the best if your goal is inference in the absence of any type annotations.
An infinitary rewriting interpretation of coinductive types
Calculating Correct Compilers II
Elaborating dependent (co)pattern matching: No pattern left behind
Effect Handlers via Generalised Continuations. tweet
An Algebraic Approach to Typechecking and Elaboration. talk. slides.
a “nanopass style” tutorial on how to implement refinement type checkers
we show how to implement a refinement type checker via a progression of languages that incrementally add features to the language or type system.
elaboration-zoo. tweet. tweet.
What makes dependent type theory more suitable than set theory for proof assistants?
Calculating Programs (MGS 2019)
Reasoning about the garden of forking paths
An Existential Crisis Resolved
elaboration. bidirectional evaluation.
Calculating Dependently-Typed Compilers
Counterexamples in Type Systems
how undefined values arise In programming languages.
Making uniqueness types less unique post
Programs and Proofs Mechanizing Mathematics with Dependent Types
Abstraction and Computation Type Theory, Algebraic Structures, and Recursive Functions
Metaprogramming Lecture Notes.
A Denotational Engineering of Programming Languages
Introduction to homotopy type theory Egbert Rijke. github
J.N. OLIVEIRA PROGRAM DESIGN BY CALCULATION. post
Curry On Talk: The Practice and Theory of TLA+
Dana Scott & Jeremy Siek - Theory & Models of Lambda Calculus: Typed and Untyped (Part 1) - λC 2018 1. 2. 6/6.
A New Language for Constant-Time Programming.
Implementing a Dependently Typed Language 1 2 3 4 5 6
Game Semantics and Session Types
Big Step Normalisation for Type Theory
Generalized Church is the Curry-Howard of Knaster-Tarski
Type Inference needs Revolution (2015)
Epigram 2 - Autopsy, Obituary, Apology
The Hitchhiker’s Guide to Logical Verification
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
the banana-split law, an important program optimisation that replaces a double tree traversal by a single one
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
Trees that grow Trees that shrink
Generalised folds for nested datatypes
Disciplined, efficient, generalised folds for nested datatypes
Compiling Tree Transforms to Operate on Packed Representations
Histo- and Dynamorphisms Revisited
I don’t know about “principled way to choose”; I think that’s largely a matter of taste. Try it both ways, and see which you prefer! More concretely, consider which properties you might like to prove of such functions; maybe those properties are more easily proved using coinduction than induction, in which case you should probably look for a coinductive program (an unfold) over an inductive one (a fold).
Catamorphism-Based Program Transformations for Non-Strict Functional Languages
Dependently Typed Folds for Nested Data Types
Coroutining Folds with Hyperfunctions. folding two things at once.
General recursion via coinductive types, by Capretta (2005). Turing-completeness totally free, by McBride (2015?). reddit.
Sometimes this is called a combinator for iteration as opposed to recursion, ie., loop corresponds to the imperative intuition of "do this, repeat"
Categories with a combinator of that very type are called iteration theories
iteration and recursion are closely related. The way I like to informally relate the two is that iteration is "just" tail recursion, and conversely, recursion can often be encoded iteratively in a stack machine. But depending on how you phrase the concepts they could be literally the same thing. That's actually what happens with iteration theories: they are models for both "iterative" languages (with loop-like constructs) and "recursive" languages (with fix-like constructs). More precisely, an iteration theory is a category with coproducts (sums of types) and a function on morphisms from a -> b + a to a -> b satisfying a bunch of equations.
In Haskell-speak, loop and fix correspond to two instances of the same class of iterative theories.
Another place where loop comes up is in representing non-terminating computations in total languages, because tail recursion is closely related to the guardedness condition for coinductive definitions. That's the starting point of the paper General recursion via coinductive types, by Capretta (2005). In contrast, it's less obvious how to encode something like fix, where you're morally allowed to make recursive calls anywhere. The aforementioned paper discusses one solution in its later sections. Another one is to use a free monad, delaying the recursive calls with an effect; that's the topic of Turing-completeness totally free, by McBride (2015?).
CATEGORICAL PROGRAMMING WITH INDUCTIVE AND COINDUCTIVE TYPES. tweet. The Nax Language: Unifying Functional Programming and Logical Reasoning in a Language based on Mendler-style Recursion Schemes and Term-indexed Types
tail recursive only fix point combinator. book
Sometimes this is called a combinator for iteration as opposed to recursion, ie., loop corresponds to the imperative intuition of "do this, repeat" (this is equivalent to forever :: m () -> m Void in the monad m = StateT t (Either p)), whereas fix corresponds to the declarative intuition of "definitions where the right-hand side mentions the left-hand side" (with "tail-recursion" adding constraints on where those mentions may occur).
Categories with a combinator of that very type are called iteration theories, there's even a whole book on the topic: Iteration Theories: The Equational Logic of Iterative Processes, by Bloom & Esik (1993).
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
catamorphism = iterator, paramorphism = recursor
Mixing Supercompilers and Recursion Using Elgot Algebras reddit
Histomorphisms, Zygomorphisms and Futumorphisms specialised to lists
Examples of histomorphisms in Haskell
Recursion Schemes, Part IV: Time is of the Essence reddit
Recursion schemes using Fix on a data-type that's already a Functor?
the digits of py - metamorphism example
A catamorphic lambda-calculus interpreter reddit
A Simple Hylomorphism Example reddit
How to make catamorphisms work with parameterized/indexed types?
Recursion Schemes, Part V: Hello, Hylomorphisms
Program Reduction: A Win for Recursion Schemes reddit
Annotating an AST with type information using recursion-schemes?
Recursion Schemes for Higher Algebras
The idea is that free constructions arise as fixed points of higher order functors, and therefore can be approached with the same algebraic machinery as recursive data structures, only at a higher level.
Feval: F-Algebras for expression evaluation
What is the difference between Fix, Mu and Nu in Ed Kmett's recursion scheme package
Recursion Schemes, Part VI: Comonads, Composition, and Generality. reddit. also an interesting discussion in a github issue.
A natural way to fold over the history involved in a histomorphism?
Compdata Trees and Catamorphisms.
over nested datatypes: still hard
Stream Fusion From Lists to Streams to Nothing at All mentioned here. and here. on hackage
there are at least two ways to turn a Haskell list into functions, and they are related in an interesting way: Representing the list inductively (a.k.a. build/foldr fusion system): Representing the list coinductively (a.k.a. stream fusion)
A Hierarchy of Mendler style iteration/recursion combinators. tweet.
the standard catamorphism [...] can specialize to a monadic carrier type
Combining folds using semigroups
recursion schemes in the GRIN compiler
Composing non-distributive monads in recursion-schemes
co-functions (aka coexponentials, coimplicatives, subtractions).
repository of recursion schemes applied to practical algorithms.
Unifying Structured Recursion Schemes
London Haskell Recursion Schemes
Lazily Diffing Merkle Trees with Recursion Schemes
recursion-schemes. recursion-schemes-5.1.
transverse is a version of hoist with side-effects. This time we cannot specialize hoist, we really do need a dedicated function
Dependently typed programming with singletons
How to keep your neighbours in order
Self Types for Dependently Typed Lambda Encodings and the SO question
A tutorial implementation of a dependently typed lambda calculus
Higher-Order Dynamic Pattern Unification for Dependent Types and Records
A Unification Algorithm for COQ Featuring Universe Polymorphism and Overloading
Contrained type families - preprint
Programming Examples Needing Polymorphic Recursion
Staged Generic Programming - in metaocaml
Quantified class constraints Reddit Another very good exposition Reddit
Safe API Design with Ghosts of Departed Proofs reddit. who authorized these ghosts?.
Writing APIs with enforced preconditions, that give the user plenty of flexibility in constructing arguments to prove that the preconditions are met.
Keep Your Laziness in Check reddit the appendix describes a way to implement variadic currying.
LiquidHaskell: Experience with Refinement Types in the Real World twitter
Interactive Programs and Weakly Final Coalgebras in Dependent Type Theory
agdarsec - Total Parser Combinators. more.
Proving tree algorithms for succinct data structures
Saint: an API-generic Type-safe Interpreter. source.
Implementing Modal Dependent Type Theory
Dependently Typed Haskell in Industry (Experience Report)
Intrinsically-Typed Definitional Interpreters for Linear, Session-Typed Languages. for imperative languages
FUNCTIONAL PEARLS Heterogeneous binary random-access lists tweet
Generic Programming of all Kinds
type your matrices for great good
A Specification for Typed Template Haskell tweet. slides
Multi-stage Programs in Context
Staged Sums of Products. video
Staged Selective Parser Combinators. video at 28:00
Eliminating Bugs with Dependent Haskell (Experience Report)
Dependent Types at Work looks like a good introduction to Agda for people with Haskell experience.
G¨odel system T is very important in the history of ideas that led to the CurryHoward isomorphism and Martin-L¨of type theory. Roughly speaking, G¨odel system T is the simply typed kernel of Martin-L¨of’s constructive type theory, and Martin-L¨of type theory is the foundational system out of which the Agda language grew. The relationship between Agda and Martin-L¨of type theory is much like the relationship between Haskell and the simply typed lambda calculus. Or perhaps it is better to compare it with the relationship between Haskell and Plotkin’s PCF [30]. Like G¨odel system T, PCF is based on the simply typed lambda calculus with truth values and natural numbers. However, an important difference is that PCF has a fixed point combinator which can be used for encoding arbitrary general recursive definitions. As a consequence we can define non-terminating functions in PCF.
DEPENDENT TYPES IN HASKELL: THEORY AND PRACTICE Richard A. Eisenberg's thesis.
Programs and Proofs Mechanizing Mathematics with Dependent Types
A specification for dependent types in Haskell
On dependent types and intuitionism in programming mathematics
Singleton types here Singleton types there Singleton types everywhere
Formal Verification of Spacecraft Control Programs Using a Metalanguage for State Transformers
Handling Recursion in Generic Programming Using Closed Type Families
Equivalences for free: univalent parametricity for effective transport
Ornamental Algebras, Algebraic Ornaments. The Essence of Ornaments. so question.
Dependent types thus provide not only a new ‘axis of diversity’ — indexing — for data structures, but also new abstractions to manage and exploit that diversity. I
Generic programming of all kinds
sums of products for mutually recursive families. tweet. slides.
Generic Deriving of Generic Traversals. slides.
All source material for Thinking with Types.
C O M P I L I N G W I T H D E P E N D E N T T Y P E S - Bowman.
Sums of Products for Mutually Recursive Datatypes
Game Semantics of Martin-Lof Type Theory
Extensible Type-Directed Editing
What is type theory, precisely?. A general definition of dependent type theories
Practical Dependent Types in Haskell: Type-Safe Neural Networks reddit
Defunctionalization for the win. Defunctionalizing Arithmetic to an Abstract Machine.
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
Dependent type checking without substitution see also this minimal implementation of the calculus of constructions
dependent regexes talk by Stephanie Weirich code (Reddit)[https://pay.reddit.com/r/haskell/comments/66p7s7/the_influence_of_dependent_types_stephanie_weirich/]
Type inference for polymorphic recursion is undecidable
Is it possible to declare FromJSON instance for my weird enum-like type?
Idiomatic boolean equality usage (singletons)
Don't use Booleans! I seem to keep repeating myself on this point: Booleans are of extremely limited usefulness in dependently-typed programming and the sooner you un-learn the habit the better. An Elem s ss ~ True context promises to you that s is in ss somewhere, but it doesn't say where. This leaves you in the lurch when you need to produce an s-value from your list of ss. One bit is not enough information for your purposes.
Is there any connection between a :~: b and (a :== b) :~: True?
Checking if one type-level list contains another
There seems to be an obsession with Boolean type families that's endemic to the Haskell community. Don't use them! You're making more work for yourself than necessary when it comes to using the result of such a test.
Dependent types in Haskell: Progress Report
Decidable Propositional Equality in Haskell
Tradeoffs of dependent types food for thought
There are two different notions of equality applicable to singletons: Boolean equality and propositional equality.
-
Boolean equality is implemented in the type family (:==) (which is actually a synonym for the type family (==) from Data.Type.Equality) and the class SEq. See the Data.Singletons.Prelude.Eq module for more information.
-
Propositional equality is implemented through the constraint (
), the type (::), and the class SDecide. See modules Data.Type.Equality and Data.Singletons.Decide for more information.
The unification-fd package by wren gayle romano is the de-facto standard way to do unification in Haskell. You’d use it if you need to implement type inference for your DSL, for example.
music composition meets dependent types
generic-lens - Generically derive lenses for accessing fields of data types (with no Template Haskell) does records-sop allow something like this as well?
Encode state transitions in types using linear types
Fixed-Length Vector Types in Haskell (an Update for 2017)
Type Level Merge Sort (Haskell)
Uses of row polymorphism in Purescript
Coinduction in Coq and Isabelle reddit
A hands-on introduction to cubicaltt
Dependent Pairs in Haskell - λC 2017 slides
Structures of Arrays, Functors, and Continuations reddit
Better Data Types a la Carte reddit earlier
Eliminating overlapping instances with type families is a known trick. In this case, we need a type family to compute a Nat index of the occurrence of a type in a lifted list, then dispatch the class instances on the computed index. This is used in freer and monad-classes, plus there's a version of this in compdata with paths to tree nodes instead of indices.
Finite-State Machines, Part 2: Explicit Typed State Transitions
Finding bugs in Haskell code by proving it and a compiler reddit
Deriving Bifunctor with Generics reddit
Haskell and dependent pairs reddit
GADTs are weak approximations of inductive families from dependently typed languages
Free Lenses for Higher-Kinded Data reddit reddit another post reddit
Haskell-cafe Selda, type operators and heterogeneous lists
Heterogeneous lists with dependent types in Haskell reddit twitter
Proving commutativity of type level addition of natural numbers
Smart constructors that cannot fail reddit
Functional Typelevel Programming in Scala HN
A recurring method in dependently typed programming is to program with data structures that enforce coherence of their indices, even though they contain no bits themselves...leaving said data-bearing indices entirely implicit.
matching on types. The universe pattern
I think it is fairly common in Haskell for a developer to play around with different ways of representing a certain thing until you converge on an elegant representation. This is many, many times more important when we are dealing with dependently-typed Haskell.
Inelegant and awkward data representations can make term-level programming clunky. Inelegant and awkward type representations can make type-level programming downright infeasible due to the sheer amount of lemmas that need to be proven.
It took me a good amount of time to put the different pieces together in my head. It is not only a matter of proving the lemma: restructuring the code in childrenToForest_go leads to different lemmas you can attempt to prove, and figuring out which ones are feasible is a big part of writing code like this.
Checking Dependent Types with Normalization by Evaluation: A Tutorial
Singletons of singletons (emulating complex pi types in Haskell).
Variable-arity zipWith in terms of Applicative ZipList. reddit.
particularities of type families
Interpreter for System T Combinator Language
(Typeable — A long journey to type-safe dynamic type representation)[https://medium.com/@hgiasac/typeable-a-long-journey-to-type-safe-dynamic-type-representation-9070eac2cf8b]
a minimal singe-file example of dependently typed elaboration with holes and pattern unification
Proving m + (1 + n) == 1+ (m + n) in Dependent Haskell.
Hide one of the type params of a multi-param typeclass in a function signature.
Proving Addition is Commutative in Haskell using Singletons.
How to think about types: Insights from a personal journey
I'm not sure in which context this usage arose (Coq? Twelf? LF? Earlier? Anyone know?), but I tend to think of the terms parameter and index as having a slight difference in meaning.
Singletons of Singletons for embedding System F-omega in Haskell
authenticated data structures, generically. tweet
making ghosts of departed proofs easier to use
Four ways to partially apply constraint tuples
Ghost Hunting the Perfect API ( with departed proofs )
Guarded Computational Type Theory
Describing Microservices using Modern Haskell (Experience Report)
Functional Pearl: Witness me - Constructive arguments must be guided with concrete witness. Interesting CS trend: evidence. Linear Logic for Constructive Mathematics.
pipelining in a session type framework
Classless GHC.Generic with Type.Reflection
Applying Type-Level and Generic Programming in Haskell Updated version reddit
ZuriHac 2016: Generic (and type-level) Programming with Generics-sop
Coding for Types: The Universe Patern in Idris
SuperRecord: Practical Anonymous Records for Haskell
Type-Safe GraphQL Servers with GADTs
A Little Taste of Dependent Types
Why are type-families (over-)used in Haskell bindings to REST APIs?.
"one of the few good uses of Boolean type families". Avoid overlapping instances with closed type families. Avoiding Overlapping Instances with Closed Type Families (GHC/AdvancedOverlap).
n. variable arity. more.
visible kind application example
Typed Protocols, Session Type Framework for Applications
BOB Summer 2019 - Peter Thiemann, Types for Protocols
Whatever happened to "open data types and open functions"?
System F in Agda, for fun and profit
Datatype-Generic Programming by Andres Löh - Advanced Track @ ZuriHac 2020
GHC curiosities: Equality constraints in kinds
CBPV doesn't distinguish data/code using kinds [...] the kind-based approach is a good one. Unboxed types in GHC.
Type rule. How to read typing rules?. Introduction to type theory for a beginner?. Type Systems introductory paper. Judgment (mathematical logic). ON THE MEANINGS OF THE LOGICAL CONSTANTS AND THE JUSTIFICATIONS OF THE LOGICAL LAWS.
From Set Theory to Type Theory. Axiomatic Set Theory in Type Theory slides.
The Trouble with Typing Type as Type. 3 Shocking Ways to Break Mathematics. An overview of type theories.
Type theories are not set theories — they do not have a separate logical formula language, like that of Frege, to serve as a basis for the theory. So, one cannot achieve consistency in type theory by restricting how a set may be constructed from a logical formula. Instead, type theory places restrictions on the kinds of formulae that can be expressed. Rather that rule out paradoxical sets representing self-referential propositions, type theory rules out the propositions themselves. In such a theory, it is not even well-formed to ask if a set contains itself4.
Why colon to denote that a value belongs to a type?
type theory book recommendations
Native Type Theory. HN. categorical logic. interesting HN comment
universe levels & induction-recursion
We are living in a new world now, if "add a bunch of universes" barely fazes our tools.
Strongly normalizing type theory beyond induction-recursion
type theory for all - gradual types
How did 'judgement' come to be a term of #logic ?
implication vs. entailment in #logic
Questions as information types. slides
A CUBICAL LANGUAGE FOR BISHOP SETS. tweet. updated version.
The collection of automated equations in a given type theory is called definitional equality; the more equations are definitional, the less time users must spend providing coercions.
To account for higher-order concepts, rather than admit higher-order judgments, we usually internalize judgmental notions as types: dependent sums internalize context extension, dependent products internalize entailment, and propositional equality should in some sense internalize judgmental equality
the structure of programs corresponds to the structure of proof search tweet.
Logical Relations As Types. video
Cubical Agda, the new extensions bringing univalence and higher inductive types to Agda. video.
Canonicity and normalization for Dependent Type Theory. Canonicity for Cubical Type Theory.
Why is regularity a problem in cubical type theory?
What technique is used to implement type checking for CoC?
The essential part of NbE is the separation of syntax and values
formalization of various type theories in Agda
controlling program extraction
Normalization for Cubical Type Theory LICS ‘21 Video.
A metalanguage for multi-phase modularity—and printf debugging!. video.
lecture notes on HoTT/UF with Agda
"It is the simplest semantics that only models two things: extensional input output behaviour and nontermination. [...] but people wanted to model more stuff [...] doesn’t tend to mix cleanly with the kinds of computational effects people want to study"
Isn't any type system about enforcing abstraction layers?
Type-theoretic constructions of the final coalgebra of the finite powerset functor
here are some objects/fams that are defined by an induction principle but are not the natural numbers. an induction principle says how to prove a property of every inhabitant of a type, or, alternatively, how to build a dependent function out of that type..
Type Theory Forall Podcast Episode #10 - Classical Logic vs Intuitionistic Logic.
Unlike in ZF, functions in type theory are a primitive notion, not defined as functional relations.
Quadratic type checking for objective type theory
we eliminate definitional equality and replace all computation rules by propositional equalities
“My personal disenchantment with dependent type theories coincides with the decision to shift from extensional to intensional equality. This meant for example that 0 + n = n and n + 0 = n would henceforth be regarded as fundamentally different assertions, one an identity holding by definition and the other a mere equality proved by induction. Of course I was personally upset to see several years of work, along with Constable’s Nuprl project, suddenly put beyond the pale. But I also had the feeling that this decision had been imposed on the community rather than arising from rational discussion. And I see the entire homotopy type theory effort as an attempt to make equality reasonable again.”
discussing judgmental equality
the hardest problem in type theory (video)
How should a “working mathematician” think about sets?. In what respect are univalent foundations “better” than set theory?. ZFC Set Theory and the Category of Sets. Axiom of infinity. Is there any set theory without something like the Axiom Schema of Separation?. Why is the powerset axiom more acceptable than the axiom of choice?. Is the axiom of universes 'harmless'?. WHAT IS THE THEORY ZFC WITHOUT POWER SET?. Reasons to believe Vopenka's principle interesting answer. Are there any large cardinals that are inconsistent with ZF?. Ultrafilters VII: Large Cardinals.
Because of Goedel's Incompleteness Theorems, we know that we cannot describe a complete axiomatization of mathematics. Any proposed axiomatization T, if consistent, will be unable to prove the principle Con(T) asserting that T itself is consistent, although we have reason to desire this principle once we have committed ourselves to T. Adding the consistency principle Con(T) simply puts off the question to Con(T+Con(T)), and so on, in a process that proceeds into the transfinite.
Thus, the large cardinal hierarchy provides exactly the tower of theories, whose levels transcend consistency strength, that we knew should exist. And it does so in a way that is mathematically robust and interesting, with its foundations arising, not in some syntactic diagonalization, but in mathematically fulfilling and meaningful questions in infinite combinatorics.
In a striking turn of events, soon thereafter, Kunen proved that Reinhardt cardinals are inconsistent with ZFC! Since then, we have been edging closer and closer to this chasm of inconsistency, defining stronger and stronger large cardinal axioms that stop just short of falling prey to Kunen’s proof.
And then you have the "Jack-in-the-box" axioms - that just give you a set ex nihilo, that you otherwise couldn't build using the toolbox. In ZFC, there's only one - Infinity. But we often consider other similar axioms - we call them "strong axioms of infinity," or large cardinals.
The reason Infinity has to be a jack-in-the-box is that, if we start with the emptyset, then all our toolbox axioms just keep spitting out finite sets. So we have a "gap" between the finite and the infinite.
We do know that ZFC cannot prove that there is even one inaccessible cardinal. And we know we cannot prove in ZFC that the existence of an inaccessible is consistent, because of limitations coming from the incompleteness theorems. So any argument that inaccessibles are consistent will have to use methods that cannot be formalized in ZFC.
There is a rough convention that results provable from ZFC alone may be stated without hypotheses, but that if the proof requires other assumptions (such as the existence of large cardinals), these should be stated. Whether this is simply a linguistic convention, or something more, is a controversial point among distinct philosophical schools (see Motivations and epistemic status below).
Why did mathematicians choose ZFC set theory over Russell's type theory?.
type theory isn't an alternative to set theory, it's an alternative to first-order logic (FOL). A type theory is another kind of logic; it's not a theory within first-order logic like set theory. In other words, type theory (as a foundation) is a logical basis for mathematical constructions while set theory could be called, for lack of a better word1, a "mathematical" basis for mathematical constructions.
Type theory, though, wasn't meant to be used like FOL. FOL is like a specification language. A first-order theory is like a specification, and we're primarily interested in models of the theory, i.e. things that fit the specification.
Arguments against large cardinals. Intersting responses.
If you doubt the consistency of large cardinals, why not start earlier and question the existence of the set of natural numbers?
What “forces” us to accept large cardinal axioms?. philosophy of set theory.
What are large cardinals for?.
The relationship between large cardinals and program termination.
What are large cardinals and large cardinal axioms?.
An introduction to Georg Cantor’s transfinite paradise
when doing homotopy theory constructively, the homotopy category of homotopy 0-types is not equivalent to the category of sets (as it is classically). In one approach it's equivalent to the category of setoids!
Models of ZFC Set Theory. blog post.
Roughly, a “model of {\mathsf{ZFC}}” is a set with a binary relation that satisfies the {\mathsf{ZFC}} axioms, just as a group is a set with a binary operation that satisfies the group axioms.
Is there a model of Set Theory which thinks it is the Standard Model.
[What do countable transitive models of ZFC look like?](https://math.stackexchange.com/questions/438035/what-do-countable-transitive-models-of-zfc-look-like.
Clearing misconceptions: Defining “is a model of ZFC” in ZFC.
Every model of ZFC has an element that is a model of ZFC.
How can there be genuine models of set theory?.
There are several reasons why model theory texts only look at models that are sets. These reasons are all related to the fact that model theory is itself studied using some (usually informal) set theory.
One benefit of sticking with set-sized models is this makes it possible to perform algebraic operations on models, such as taking products and ultrapowers, without any set-theoretic worries.
Standard model of ZFC and existence of model of ZFC.
Uncountable sets in countable models of ZFC.
Crash course on higher-order logic and type theory
Course: Higher-Dimensional Type Theory. ~ Favonia#TypeTheory #ITP #Agda. syllabus tweet
Why is the Axiom of Choice not needed when the collection of sets is finite?. Intuition behind the Axiom of Choice. Axiom of choice confusion: what does it mean an element to have no distinguishing features?. Axiom of Choice and finite sets.
The ability to give a name to some arbitrary element of a nonempty set is known as "existential instantiation". This is an inference rule of the underlying logic, not part of the theory, and so it is included not only in ZFC, but also in ZF, and in appropriate forms it is also included in PA and every other first-order theory.
Making one choice is simple, if a set A is not empty, then ∃a(a∈A), and therefore we can pick such a. This is called existential instantiation. But this choice is completely arbitrary.
However making infinitely many arbitrary choices is something we cannot prove to be possible1.
Remember that arbitrary sets have absolutely no structure. We only have ∈ in our language, and we have sets and their elements. Sometimes we are lucky and the elements of the set are nice enough to allow for a definable way of choosing from them. For example if the empty set is a member or something.
A common misconception is that countable choice has an inductive nature and is therefore provable as a theorem (in ZF, or similar, or even weaker systems) by induction. However, this is not the case; this misconception is the result of confusing countable choice with finite choice for a finite set of size n (for arbitrary n), and it is this latter result (which is an elementary theorem in combinatorics) that is provable by induction.
Why is the axiom of choice required for infinite, but not finite, sets?.
Why can't proofs have infinitely many steps?.
One could view the axiom of choice as a sort of finitary (and therefore usable) surrogate for the infinitely long axioms and proofs that would come up in your approach.
Do we need Axiom of Choice to make infinite choices from a set?.
If all the sets you choose from are the same, then constant choices are choices that you can always make. If all the sets you choose from have a particular structure on all of them (e.g. they are all finite sets of real numbers), then you can choose from them all (e.g. they are all finite sets of real numbers, take the minimal element).
small infinitary epistemic logics.
We develop a series of small infinitary epistemic logics to study deductive inference involving intra/inter-personal beliefs/knowledge in social situations. In these situations, people’s beliefs may include infinitary components such as common knowledge, common beliefs, and infinite regress of beliefs.
IN PRAISE OF REPLACEMENT AKIHIRO KANAMORI.
nonstandard models of arithmetic
Type theory, Category theory and Philosophy. events and temporal types
hilosophy, computer science and linguistics have much to say to one another,
what is an explicit bijection? slides
implementing modal type theory
Setoid type theory - a syntactic translation
Definable Quotients in Type Theory. reddit
Algebraic models of dependent type theory
Induction-Recursion – 20 years later warning! might have a mistake at slide 21.
A STUDY OF SELF-REFERENTIAL GÖDEL NUMBERINGS