David Young roboguy13

Monads and delimited control are very closely related, so it isn’t too hard to understand them in terms of one another. From a monadic point of view, the big idea is that if you have the computation m >>= f, then f is m’s continuation. It’s the function that is called with m’s result to continue execution after m returns.

If you have a long chain of binds, the continuation is just the composition of all of them. So, for example, if you have

m >>= f >>= g >>= h

then the continuation of m is f >=> g >=> h. Likewise, the continuation of m >>= f is g >=> h.

Programming as Theory Building

Peter Naur

Peter Naur's classic 1985 essay "Programming as Theory Building" argues that a program is not its source code. A program is a shared mental construct (he uses the word theory) that lives in the minds of the people who work on it. If you lose the people, you lose the program. The code is merely a written representation of the program, and it's lossy, so you can't reconstruct

Anon, a young researcher, sits down with Saunders Mac Lane.

Anon: Please, explain to me in full detail, everything you know about category theory. Indicate where you are uncertain so I may better understand your epistemic state.

-- End Prompt

Saunders: It's the foundation of modern mathematics and computer science. It deals with sets of objects called categories, which can be thought of as collections of things. For example, there is a set called the natural numbers that we use for counting. There is also another set called the real numbers, which are used for computing. The idea behind it is that if two things are in one category, then they must have some relationship to each other. If two things are in two different categories, then they probably don't have any relationship to each other.

Anon: Can you describe how these objects and arrows get used in practice?

Semi-automatic Defunctionalization of Continuations

Tony Garnock-Jones. February 2016.

Abstract

Programmers use continuations to achieve all manner of interesting control effects (e.g. Shivers & Turon 2011). But common representations of continuations cause problems in practice in two ways. On one hand, continuations represented as functions are entirely opaque; the only available operation is to invoke the continuation. On the other hand, continuations represented as reified machine stacks expose too much information; irrelevant detail of the program's information becomes visible. In this paper, we present a design for a middle-ground. Using our new language construct, continuations are represented as censored reified machine stacks. Programmers precisely control the information and behavior associated with each frame in the continuation, allowing them the benefits of automatic continuation reification combined with the benefits of a defunctionalized representation of control as data.

Tactics in Agda

This gist is my attempt to list all projects providing proof automation for Agda.

Glossary

When I say tactic, I mean something that uses Agda's reflection to provide a smooth user experience, such as the solveZ3 tactic from Schmitty:

_ : ∀ (x y : ℤ) → x ≤ y → y ≤ x → x ≡ y
_ = solveZ3

Equality-in-equality-out category theory in cubical Agda

Now that equality has become computationally relevant but composition of equality remains cumbersome, the statement of various equality laws in the cubical library feels "wrong". Here I want to explore an alternative approach.

What I'm not proposing

To avoid confusion, I want to start by emphasizing what I'm not proposing.

Inductive-Recursive Types, Generally

I write about inductive-recursive types here. "Generally" means "higher inductive-inductive-recursive" or "quotient inductive-inductive-recursive". This may sound quite gnarly, but fortunately the specification of signatures can be given with just a few type formers in an appropriate framework.

In particular, we'll have a theory of signatures which includes Mike Shulman's higher IR example.

	-- Automatic derivation of equality for inductive types. Examples.
	-- Inspired by https://github.com/alhassy/gentle-intro-to-reflection.
	-- Tested on: Agda version 2.6.2.1-59c7944, std-lib 1.7

	module _ where

	open import Data.Bool
	open import Data.List
	open import Data.Unit
	open import Relation.Binary.PropositionalEquality

	{- Here is a short demonstration on how to use Agda's solvers that automatically
	prove equations. It seems quite impossible to find complete worked examples
	of how Agda solvers are used.

	Thanks go to @anormalform who helped out with these on Twitter, see
	https://twitter.com/andrejbauer/status/1549693506922364929?s=20&t=7cb1TbB2cspIgktKXU8rng

	I welcome improvements and additions to this file.

	This file works with Agda 2.6.2.2 and standard-library-1.7.1


	{-# OPTIONS --prop --without-K --show-irrelevant --safe #-}

	{-
	Challenge:
	- Define a deeply embedded faithfully represented syntax of a dependently typed
	TT in Agda.
	- Use an Agda fragment which has canonicity. This means that the combination of
	indexed inductive types & cubical equality is not allowed!
	- Prove consistency.