| {- 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 |
| -- 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 |
This gist is my attempt to list all projects providing proof automation for Agda.
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
Tony Garnock-Jones. February 2016.
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.
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?
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
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 >>= hthen the continuation of m is f >=> g >=> h. Likewise, the continuation of m >>= f is g >=> h.
(draft; work in progress)
See also:
This is a compiled list of falsehoods programmers tend to believe about working with time.
Don't re-invent a date time library yourself. If you think you understand everything about time, you're probably doing it wrong.
This is a term that performs modulo 32 addition on two 32-bit binary numbers efficiently on the abstract algorithm.
On this example, I compute 279739872 + 496122620 = 775862492.
binSize= 32
binZero= (binSize r.a.b.c.(a r) a.b.c.c)
binSucc= (binSize r.x.a.b.c.(x b x.(a (r x)) c) a.a)
binFold= x.a.b.c.(binSize r.x.(x x.f.(a (f x)) x.f.(b (f x)) f.c r) a.c x)
binToNat= (binSize r.n.x.(x x.f.(f x) x.f.(add n (f x)) f.0 (r (mul 2 n))) n.x.0 1)