-
-
Save epicallan/8b81cf00182ef4373af7c669f5f60cb4 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.
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.
Unembedding Domain-specific Languages
Devon Stewart - Higher Order Abstract Syntax
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
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.
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.
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
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"
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)
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?
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?
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".
http://www.cs.ox.ac.uk/jeremy.gibbons/publications/fp4dsls.pdf Functional Programming for Domain-Specific Languages http://cs448h.stanford.edu/DSEL-Little.pdf hudak https://www.andres-loeh.de/HaskellForDSLs.pdf Loh https://github.com/mchakravarty/hoas-conv https://wiki.haskell.org/Embedded_domain_specific_language https://www.reddit.com/r/haskell/comments/2e8d53/whats_the_best_practice_for_building_a_dsl_in/ https://skillsmatter.com/skillscasts/2872-haskell-for-embedded-domain-specific-languages http://cacm.acm.org/magazines/2011/7/109910-dsl-for-the-uninitiated/fulltext https://www.reddit.com/r/haskell/comments/2dh0sd/denotational_design_from_meanings_to_programs_by/ http://lambda-the-ultimate.org/node/2438 http://okmij.org/ftp/tagless-final/course/lecture.pdf https://gist.github.com/PkmX/182c6c5444b695d9a794 http://homepages.inf.ed.ac.uk/slindley/papers/unembedding.pdf
Two approaches to representing variables in a typed term language implemented as a GADT are (1) to use higher-order abstract syntax (HOAS) or to use de Bruijn indices.. Both approaches are convenient for manipulating terms as they require no explicit alpha conversion and avoid name capture during substitution. Nevertheless, there are trade offs between the two. In particular, the HOAS representation doesn't support comparing variable names and the de Bruijn representation is inconvenient for humans to read and write. For a more detailed discussion, see for example Conor McBride and James McKinna's I am not a number: I am a free variable, where they discuss a mixed representation using de Bruijn indices for bound variables and variables of the meta-language for free variables.
The tension between the HOAS and de Bruijn representation also has relevance for the design and implementation of embedded domain specific languages (EDSLs) — aka internal languages. When an internal includes higher-order functions, it is usually most convenient for the user to use the function abstraction mechanisms of the host language. However, to execute or compile the internal language, de Bruijn notation is often more convenient; at least, if optimisations are performed.
http://www2.hh.se/staff/vero/dsl/printL1.pdf http://www2.hh.se/staff/vero/dsl/printL2.pdf http://www2.hh.se/staff/vero/dsl/printL3.pdf http://www2.hh.se/staff/vero/dsl/printL4.pdf http://www2.hh.se/staff/vero/dsl/printL5.pdf http://www2.hh.se/staff/vero/dsl/printL6.pdf
Typed compilation to tagless-final HOAS The embedded DSL is now higher-order: it is simply-typed lambda-calculus with the fixpoint and constants — essentially, PCF. We no longer use staging. Rather, we compile to tagless-final representation, which can be interpreted by different interpreters. Regardless of the number of interpretations of a term, the type checking happens only once. We build our own Dynamics to encapsulate typed terms and represent their types.
https://www.haskell.org/communities/11-2009/report.pdf https://en.wikipedia.org/wiki/Programming_Computable_Functions
https://mail.haskell.org/pipermail/haskell-cafe/2009-October/067425.html
https://blog.cppcabrera.com/posts/56-writing-a-search-dsl-1.html
http://gallium.inria.fr/~naxu/research/dsel.pdf
Sharing and recursion are common problems when implementing DSLs. Often some kind of observable sharing is requested that requires a deep embedding.
Oleg in Haskell-Cafe about Designing DSL with explicit sharing (was: I love purity, but it's killing me) Koen Classen: Observable Sharing for Functional Circuit Description Andy Gill: Type-Safe Observable Sharing Tom Lokhorst AwesomePrelude presentation (video) Leandro Lisboa Penz Haskell eDSL Tutorial - Shared expenses Bruno Oliveira and William Cook: Functional Programming with Structured Graphs Emil Axelsson and Koen Claessen: Using Circular Programs for Higher-Order Syntax Oleg Kiselyov: Implementing explicit and finding implicit sharing in embedded DSLs
An obvious way to relief the tension between the representations is to use HOAS in the surface representation of the internal language and to convert that to the de Bruijn representation before optimisation and execution. However, the conversion is not entirely straight forward for a strongly typed internal language with typed intermediate representations and type-preserving transformations between those representations.
http://www.iro.umontreal.ca/~monnier/tcm.pdf
Implementing Explicit and Finding Implicit Sharing in Embedded DSLs
I love purity, but it's killing me
Simple and Compositional Reification of Monadic Embedded Languages
https://www.reddit.com/r/haskell/comments/4ck2yh/compilation_as_a_typed_edsltoedsl_transformation/
The Difference Between Shallow and Deep Embedding
Certifying Machine Code Safety: Shallow versus Deep Embedding
Shallow versus Deep Embeddings
Embedded domain specific language (links)
Using Circular Programs for Higher-Order Syntax
Implementing Explicit and Finding Implicit Sharing in Embedded DSLs
Type-Safe Observable Sharing in Haskell
An Image Processing Language: External and Shallow/Deep Embeddings
Fizzbuzz in Haskell by embedding a DSL
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
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
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.
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.\
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.
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
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
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 .
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.
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.
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)[https://www.youtube.com/playlist?list=PLvPsfYrGz3wspkm6LVEjndvQqK6SkcXaT]
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
Cheney, Bisimulation and Coinduction for Dummies
Sangiorgi, An Introduction to Bisimulation and Coinduction
A Tutorial on (Co)Algebras and (Co)Induction
Practical Coinduction A property holds by induction if there is good reason for it to hold; whereas a property holds by coinduction if there is no good reason for it not to hold.
On proof and progress in Mathematics
A taste of linear logic / linear thoughts
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.
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
2017 04 28 - Andreas Lochbihler - Functional Programming and Proving in Isabelle/HOL
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.
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
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
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
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!
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
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
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.
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
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
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.
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
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.
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.
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.
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.
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
Unifying Structured Recursion Schemes
London Haskell 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
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?
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
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.
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.
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
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
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
Practical Dependent Types in Haskell: Type-Safe Neural Networks reddit
Defunctionalization for the win
Better Data Types a la Carte -- with injectivity guaranteed by construction
trying fancy type stuff: is it possible to write slice for Fixed-Length vectors?
How to write a Monoid instance for something that depends on parameters
Data families vs Injective type families
Quotient types for programmers
Pattern Matching on Type Constructors? type families allow Prolog-like non-linear matches
How can quotient types help safely expose module internals?
Typesafe Printf with TypeInType
working my way through Data.Type.Equality...my head hurts
Decidable Propositional Equality in Haskell
A Functional Programmer's Guide to Homotopy Type Theory
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
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.